Decision Algorithms for Probabilistic Bisimulation

Appears: Proceedings of the 13th International Conference on Concurrency Theory (CONCUR '02), Brno, Czech Republic, LNCS 2421, pages 371--385, August 2002.

Abstract: We propose decision algorithms for bisimulation relations defined on probabilistic automata, a model for concurrent nondeterministic systems with randomization. The algorithms decide both strong and weak bisimulation relations based on deterministic as well as randomized schedulers. These algorithms extend and complete other known algorithms for simpler relations and models. The algorithm we present for strong probabilistic bisimulation has polynomial time complexity, while the algorithm for weak probabilistic bisimulation is exponential; however we argue that the latter is feasible in practice.

Download:
Download the paper from the publisher.

Download an author-created copy of the paper (© Springer-Verlag).