Deciding Bisimilarities on Distributions

  • Christian Eisentraut
  • Holger Hermanns
  • Julia Krämer
  • Andrea Turrini
  • Lijun Zhang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)


Probabilistic automata (PA) are a prominent compositional concurrency model. As a way to justify property-preserving abstractions, in the last years, bisimulation relations over probability distributions have been proposed both in the strong and the weak setting. Different to the usual bisimulation relations, which are defined over states, an algorithmic treatment of these relations is inherently hard, as their carrier set is uncountable, even for finite PAs. The coarsest of these relation, weak distribution bisimulation, stands out from the others in that no equivalent state-based characterisation is known so far. This paper presents an equivalent state-based reformulation for weak distribution bisimulation, rendering it amenable for algorithmic treatment. Then, decision procedures for the probability distribution-based bisimulation relations are presented.


Decision Algorithm Weak Transition Probabilistic Automaton Preserve Transition Weak Setting 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Chatterjee, K., Henzinger, M.R.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SODA, pp. 1318–1336 (2011)Google Scholar
  4. 4.
    de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)Google Scholar
  5. 5.
    Deng, Y., Hennessy, M.: On the semantics of Markov automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 307–318. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Deng, Y., Hennessy, M.: On the semantics of Markov automata. I&C 222, 139–168 (2012)MathSciNetGoogle Scholar
  7. 7.
    Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae 49, 129–144 (1961)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 21–39. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  9. 9.
    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010)Google Scholar
  10. 10.
    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. Reports of SFB/TR 14 AVACS 62, SFB/TR 14 AVACS (2010)Google Scholar
  11. 11.
    Hennessy, M.: Exploring probabilistic bisimulations, part I. Formal Aspects of Computing 24(4-6), 749–768 (2012)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002)Google Scholar
  13. 13.
    Hermanns, H., Turrini, A.: Deciding probabilistic automata weak bisimulation in polynomial time. In: FSTTCS, pp. 435–447 (2012)Google Scholar
  14. 14.
    Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. I&C 86(1), 43–68 (1990)MathSciNetzbMATHGoogle Scholar
  15. 15.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing (preliminary report). In: POPL, pp. 344–352 (1989)Google Scholar
  16. 16.
    Lynch, N.A., Segala, R., Vaandrager, F.W.: Compositionality for probabilistic automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 208–221. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. 17.
    Lynch, N.A., Segala, R., Vaandrager, F.W.: Observing branching structure through probabilistic contexts. SIAM J. on Computing 37(4), 977–1013 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    Schuster, J., Siegle, M.: Markov automata: Deciding weak bisimulation by means of “non-naïvely” vanishing states,
  20. 20.
    Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT (1995)Google Scholar
  21. 21.
    Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64–78. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  22. 22.
    Stirling, C.: Local model checking games (extended abstract). In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  23. 23.
    Thomas, W.: On the Ehrenfeucht-Fraïssé game in theoretical computer science. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) TAPSOFT 1993. LNCS, vol. 668, pp. 559–568. Springer, Heidelberg (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Christian Eisentraut
    • 1
  • Holger Hermanns
    • 1
  • Julia Krämer
    • 1
  • Andrea Turrini
    • 1
  • Lijun Zhang
    • 2
    • 3
    • 1
  1. 1.Computer ScienceSaarland UniversitySaarbrückenGermany
  2. 2.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  3. 3.DTU InformaticsTechnical University of DenmarkDenmark

Personalised recommendations