The Study Of Fuzzy Bisimulation Verification Algorithm

With the development of the times,the complexity of computer's hardware and software systems has improved,the application of formal verification in computer science is more and more widely.As an important part of formal verification,bisimulation has perfect mathematical properties and is used to describe the equivalences of system's behavior.The transition system which satisfies the bisimulation can imitate each other's behavior.Algorithm for bisimulaion are usually classified into two kinds: global algorithm and local algorithm.Global algorithm is mainly used to verify that any states in systems satisfy the bisimulation but need to store all the transition systems.Local algorithm is mainly used to verify the given states whether satisfy the bisimulation.The local algorithm only need to traverse the states which belong to the given states succeed set.It has better efficiency when verify the states which do not satisfy the bisimulation.Classical system models limited to qualitative analysis and can no longer meet the actual needs.As an important part for quantitative analysis of systems,fuzzy theory has got a lot of attention by computer scientists.Since 1970s,computer scientists have applied fuzzy theory to the transition systems and have depth research on the bisimulation equivalence under the fuzzy transition system.In order to verify the states which between fuzzy transition systems satisfy the fuzzy bisimulation quickly,the algorithm for checking fuzzy bisimulation is particularly important.The main contributions of this paper are follows:1.An equivalence class partition algorithm for fuzzy bisimulation is proposed.The equivalence class partition algorithm for fuzzy bisimulation is a kind of global algorithm,which based on the idea of partition refinement.The algorithm uses transition to divide the state into equivalence classes,and also uses the state to divide the equivalence classes of transition until the following conditions are met:(1)All states that meet the fuzzy bisimulation are in an equivalence class;(2)Any state in the equivalence class of states satisfies the fuzzy bisimulation.2.A local algorithm for checking fuzzy bisimulation is proposed.The algorithm takes the method which is depth-first traversal.While traversing the current states and it's succeed states,the algorithm also need to be verified that its successor states whether satisfies the fuzzy bisimulation.In the worst case,that is,when all subsequent states are traversed,the algorithm gives the final result.3.Use Java to implement the algorithm of fuzzy bisimulation equivalence class partition and fuzzy bisimulation equivalence verification.Through the combination of theoretical analysis and experimental comparison,the equivalence class partition algorithm for fuzzy bisimulation,the local algorithm for checking fuzzy bisimulation and the existing global algorithm are compared with each other,the advantages and disadvantages applicability of the two algorithms are discussed and explained.