The report FIMU-RS-2004-06
Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems
A full version of the paper presented at CONCUR`04. September 2004, 26 pages.
Available as Postscript,
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.