Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BRÁZDIL Tomáš KUČERA Antonín STRAŽOVSKÝ Oldřich
Year of publication	2004
Type	Article in Proceedings
Conference	Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004)
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	probabilistic bisimilarity; probabilistic systems
Description	We prove that probabilistic bisimilarity is decidable over probabilistic extensions of BPA and BPP processes. For normed subclasses of probabilistic BPA and BPP processes we obtain polynomial-time algorithms. Further, we show that probabilistic bisimilarity between probabilistic pushdown automata and finite-state systems is decidable in exponential time. If the number of control states in PDA is bounded by a fixed constant, then the algorithm needs only polynomial time.
Related projects:	Verification of infinite-state systems Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing