Comparison And Application Of Bisimulation Verification Algorithm

Bisimulation equivalence plays a central role in the verification of concurrent systems based on equivalence relations between labeled transition systems.Decision algorithms for bisimilarity in finite state systems are usually classified into two kinds: global algorithms and local algorithms.Our main contributions are as follows:(1)Introduce the local algorithm,including on-the-fly algorithm and quasi-local algorithm,and compare the running time of the two algorithms.(2)Discuss the main ideas of global algorithm and implement Valmari's algorithm,which is of the best comprehensive performance.Then we compare the Valmari's algorithm with CADP tools.(3)Bisimulation reduction of states in RDF(Resource Description Framework)graphs,which can be called a bisimulation minimization problem.To solve the bisimulation minimization problem,Antti Valmari proposed an algorithm based on Hopcroft,Paige and Tarjan's ideas.Later,Alexander Sch?tzle and other people proposed an algorithm using external memory to solve the large-scale RDF bisimulation reduction.In fact,the Antti Valmari's algorithm can also deal with large systems with an in-memory implementation.We try to use Antti Valmari's algorithm in this paper to solve the RDF bisimulation reduction problem and make a comparison between the Java implementation of Antti Valmari's algorithm and the SQL implementation of Alexander Sch?tzle's algorithm.