Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems
by
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
A full version of the paper presented at CONCUR`04. September 2004, 26 pages.
FIMU-RS-2004-06.
Available as Postscript,
PDF.
Abstract:
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.