A local algorithm for checking probabilistic bisimilarity

Bisimilarity is one of the most important relations for comparing the behaviour of formal systems in concurrency theory. Decision algorithms for bisimilarity in finite state systems are usually classified into two kinds: global algorithms are generally efficient but require to generate the whole state spaces in advance, and local algorithms combine the verification of a system's behaviour with the generation of the system's state space, which is often more effective to determine that one system fails to be related to another. Although local algorithms are well established in the classical concurrency theory, the study of local algorithms in probabilistic concurrency theory is not mature. In this paper we propose a polynomial time local algorithm for checking probabilistic bisimilarity. With mild modification, the algorithm can be easily adapted to decide probabilistic similarity with the same time complexity.