Implementations for checking bisimulation of LTS

Bisimilarity is one of the most studied relations between behavioral equivalences proposed in the concurrency theory. Algorithms for checking bisimulation in finite state system are very useful for both theoretical aspects and practical applications. In order to give a detailed comparison on different implementation techniques for bisimilarity of LTS, this paper studies and implements two different algorithms: on-the-fly algorithm and quasi-local algorithm, by adopting both depth-first-search and width-first-search. The experimental results and discussions of the applicabilities and advantages of these algorithms are also performed, which show the usage of two algorithms. The research gives insights on further implementation of model-specific process calculi.