A Local Algorithm for Checking Probabilistic Bisimilarity
Yuxin Deng and Wenjie Du
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; 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.