Deciding probabilistic bisimilarity over infinite-state probabilistic systems

Warning

This publication doesn't include Faculty of Arts. 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 2008
Type Article in Periodical
Magazine / Source Acta informatica
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords probabilistic bisimilarity; infinite-state 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:

You are running an old browser version. We recommend updating your browser to its latest version.