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.
The work has been supported by the Grant Agency of the Czech Republic, grant No. 201/03/1161.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Baier, C., Iyer, P., Jonsson, B.: Reasoning about probabilistic lossy channel systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 320–330. Springer, Heidelberg (2000)
Abdulla, P.A., Rabinovich, A.: Verification of probabilistic systems with faulty communication. In: Gordon, A.D. (ed.) ETAPS 2003 and FOSSACS 2003. LNCS, vol. 2620, pp. 39–53. Springer, Heidelberg (2003)
Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 155–165. Springer, Heidelberg (1995)
Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: On the consistency of Koomen’s fair abstraction rule. TCS 51(1), 129–176 (1987)
Baier, C., Engelen, B.: Establishing qualitative properties for probabilistic lossy channel systems: An algorithmic approach. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 34–52. Springer, Heidelberg (1999)
Baier, C., Hermanns, H., Katoen, J.: Probabilistic weak simulation is decidable in polynomial time. Information Processing Letters 89(3), 123–130 (2004)
Bianco, A., de Alfaro, L.: Model checking of probabalistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Brázdil, T., Kučera, A., Stražovský, O.: Deciding probabilistic bisimilarity over infinite-state probabilistic systems. Technical report FIMU-RS-2004-06, Faculty of Informatics, Masaryk University (2004)
Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Handbook of Process Algebra, pp. 545–623 (1999)
Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)
Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of 29th Annual Symposium on Foundations of Computer Science, pp. 338–345. IEEE, Los Alamitos (1988)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. JACM 42(4), 857–907 (1995)
de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using mTBDDs and the kronecker representation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000)
Esparza, J., Kučera, A., Mayr, R.: Model-checking probabilistic pushdown automata. In: Proceedings of LICS 2004. IEEE, Los Alamitos (to appear, 2004)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 512–535 (1994)
Huth, M., Kwiatkowska, M.Z.: Quantitative analysis and model checking. In: Proceedings of LICS 1997, pp. 111–122. IEEE, Los Alamitos (1997)
Iyer, S.P., Narasimha, M.: Probabilistic lossy channel systems. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 667–681. Springer, Heidelberg (1997)
Jonsson, B., Yi, W., Larsen, K.G.: Probabilistic extensions of process algebras. In: Handbook of Process Algebra, pp. 685–710 (1999)
Kučera, A., Mayr, R.: A generic framework for checking semantic equivalences between pushdown automata and finite-state automata. In: Proceedings of IFIP TCS 2004. Kluwer, Dordrecht (to appear, 2004)
Kwiatkowska, M.Z.: Model checking for probability and time: from theory to practice. In: Proceedings of LICS 2003, pp. 351–360. IEEE, Los Alamitos (2003)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. I&C 94(1), 1–28 (1991)
Rabinovich, A.: Quantitative analysis of probabilistic lossy channel systems. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1008–1021. Springer, Heidelberg (2003)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. NJC 2(2), 250–273 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brázdil, T., Kučera, A., Stražovský, O. (2004). Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems. In: Gardner, P., Yoshida, N. (eds) CONCUR 2004 - Concurrency Theory. CONCUR 2004. Lecture Notes in Computer Science, vol 3170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28644-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-28644-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22940-7
Online ISBN: 978-3-540-28644-8
eBook Packages: Springer Book Archive