Design And Implementation Of Algorithms For Checking Bisimilarity

With the rapid development of computer networks and telecommunication tech-nologies, innovations of multi-core CPU systems and cloud computing, and the popu-larization of distributed computing, modeling and analysis of concurrent systems havebecome one of the most important computer technologies. Since 1980s, widely re-searches have been done on concurrent systems. Various formal models of concurrentsystems are proposed. An ideal concurrent model should have the characteristics ofconcurrency, distribution, real-time, heterogeneous, and interaction. Due to the intrin-sic complexities, compared to sequential computations of traditional models, there areso many unclear ?elds on concurrent models.Process algebra describes concurrent computing through algebraic models. Theyare able to depict concurrent phenomena that many processes are activated concurrent-ly, completing their expected work through exchanging information. It becomes themost representative model due to its perfect algebraic properties, standard grammars,and concise semantics. One of the important research approaches on process algebraand concurrent theory is the equivalence relations, which are able to judge whether andwhen two processes have similar behaviors. There have been various kinds of equiv-alences and preorder relations proposed in recent 30 years, among which, bisimilarityis the most standard one. Bisimilarity is the basis of organizing processes, and de?n-ing other equivalences. It has perfect mathematical properties, and is used to depictrelationship between processes naturally.However, duetotheundecidabilityofbisimulations, therearelackoftechnologiesfor automatic checking bisimulation, which need restriction and approximation. Mostalgorithms for checking bisimilarity including global and local algorithms are based on ?nite state labeled transition systems. Although global algorithms are e?cient ,they are not very practical, since they should memorize the transfer relation of wholesystem states. Local algorithms lean on better practicality by considering only currentand relative states.This thesis introduces and implements two algorithms for automatic checkingbisimulation on ?nite state labeled transition systems. One is a local algorithm andthe other is a quasi-local algorithm with both local and global algorithm merits.Local algorithm: We analyze the pair of target states on LTSs, combine thechecking of the bisimulation with generation of the system's state space. Todetermine whether the initial states are bisimilarity, the algorithm attempts toconstruct a relation relating the states of the LTSs incrementally starting withthe pair of initial states. This algorithm generates the product dynamically soit is also called"On-the-Fly"veri?cation algorithm. In fact, the procedure ofsearching may have to execute several times to get the answer.Quasi-LocalAlgorithm: WestartwithconstructingtheproductoftwoLTSswithstates relating to the initial pair of states. The synchronous product obtained iscalled DLTS. We label states (s∥t) in the DLTS with 0 if s and t have di?erentinitial actions. Otherwise we label state 1. Then we propagate label 0 step bystep to all pairs of states those are not bisimilar, until all the labels of statesin the DLTS are not changed. Although this algorithm needs to generate thesynchronous product (L1∥L2) by a preprocessing step, it quickly terminatesand gives the right result in most cases.The two algorithms have their own advantages when checking the bisimulationunder different processes. We experiment several test cases after implementing them.We also investigate what kind of condition, one may act more e?cient than the other.Furthermore, we give the analysis on their respective applicabilities, merits and draw-backs. The result turns out the bisimilarity in ?nite state systems can be determined.The quasi-local algorithm have a lower theoritical time complexity, and runs faster inmost cases. We believe this article could serve as a good introductory work for futureresearches on bisimilarity in in?nite state system.