Skip to main content
SpringerLink
Log in

Distribution-Based Bisimulation for Labelled Markov Processes

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10419))

Abstract

In this paper we propose a (sub)distribution-based bisimulation for labelled Markov processes and compare it with earlier definitions of state and event bisimulation, which both only compare states. In contrast to those state-based bisimulations, our distribution bisimulation is weaker, but corresponds more closely to linear properties. We construct a logic and a metric to describe our distribution bisimulation and discuss linearity, continuity and compositional properties.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey. Electr. Notes Theor. Comput. Sci. 297, 3–25 (2013)

    Article  MATH  Google Scholar 

  2. Abate, A., Katoen, J.-P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 16(6), 624–641 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On-the-fly exact computation of bisimilarity distances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 1–15. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_1

    Chapter  Google Scholar 

  4. Blute, R., Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 149–158. IEEE Computer Society (1997)

    Google Scholar 

  5. van Breugel, F., Sharma, B., Worrell, J.: Approximating a behavioural pseudometric without discount for probabilistic systems. Logical Methods Comput. Sci. 4(2), 123–137 (2008)

    MathSciNet  MATH  Google Scholar 

  6. Chaput, P., Danos, V., Panangaden, P., Plotkin, G.D.: Approximating Markov processes by averaging. J. ACM 61(1), 5:1–5:45 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  7. Daca, P., Henzinger, T.A., Křetínský, J., Petrov, T.: Linear distances between Markov chains. In: Concurrency Theory (CONCUR). Leibniz International Proceedings in Informatics (LIPIcs), vol. 59, pp. 20:1–20:15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  8. Danos, V., Desharnais, J., Laviolette, F., Panangaden, P.: Bisimulation and cocongruence for probabilistic systems. Inf. Comput. 204(4), 503–523 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. Danos, V., Desharnais, J., Panangaden, P.: Conditional expectation and the approximation of labelled markov processes. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 477–491. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45187-7_31

    Chapter  Google Scholar 

  10. Danos, V., Desharnais, J., Panangaden, P.: Labelled Markov processes: stronger and faster approximations. Electr. Notes Theor. Comput. Sci. 87, 157–203 (2004)

    Article  MATH  Google Scholar 

  11. D’Argenio, P.R., Terraf, P.S., Wolovick, N.: Bisimulations for non-deterministic labelled Markov processes. Math. Struct. Comput. Sci. 22(1), 43–68 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  12. Deng, Y.: Semantics of Probabilistic Processes. Springer, Heidelberg (2014)

    Book  MATH  Google Scholar 

  13. Desharnais, J., Edalat, A., Panangaden, P.: A logical characterization of bisimulation for labeled Markov processes. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 478–487. IEEE Computer Society (1998)

    Google Scholar 

  14. Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163–193 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  15. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating labelled Markov processes. Inf. Comput. 184(1), 160–200 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  16. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Doyen, L., Henzinger, T.A., Raskin, J.F.: Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci. 19(3), 549–563 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  18. Durrett, R.: Probability: Theory and Examples, 3rd edn. Duxbury Press, Belmont (2004)

    MATH  Google Scholar 

  19. Feng, Y., Zhang, L.: When equivalence and bisimulation join forces in probabilistic automata. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 247–262. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_18

    Chapter  Google Scholar 

  20. Ferns, N., Panangaden, P., Precup, D.: Bisimulation metrics for continuous Markov decision processes. SIAM J. Comput. 40(6), 1662–1714 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  21. Gebler, D., Larsen, K.G., Tini, S.: Compositional metric reasoning with probabilistic process calculi. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 230–245. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46678-0_15

    Chapter  Google Scholar 

  22. Hennessy, M.: Exploring probabilistic bisimulations, part I. Formal Asp. Comput. 24(4–6), 749–768 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  23. Hermanns, H., Krčál, J., Křetínský, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249–265. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44584-6_18

    Google Scholar 

  24. Kemeny, J.G., Snell, J.L.: Finite Markov chains. Springer, Heidelberg (1960)

    MATH  Google Scholar 

  25. Larsen, K.G., Skou, A.: Bisimulation through probablistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MATH  Google Scholar 

  26. Panangaden, P.: Labelled Markov Processes. Imperial College Press, London (2009)

    Book  MATH  Google Scholar 

  27. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)

    MathSciNet  MATH  Google Scholar 

  28. Tang, Q., van Breugel, F.: Computing probabilistic bisimilarity distances via policy iteration. In: Concurrency Theory (CONCUR). LIPIcs, vol. 59, p. 22:1–22:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  29. Terraf, P.S.: Unprovability of the logical characterization of bisimulation. CoRR abs/1005.5142 (2010)

    Google Scholar 

  30. Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative simulations by Matrices. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 451–466. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44584-6_31

    Google Scholar 

  31. Vink, E.P., Rutten, J.J.M.M.: Bisimulation for probabilistic transition systems: a coalgebraic approach. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 460–470. Springer, Heidelberg (1997). doi:10.1007/3-540-63165-8_202

    Chapter  Google Scholar 

Download references

Acknowledgement

This work has been supported by the National Natural Science Foundation of China (Grants 61532019, 61472473), the CAS/SAFEA International Partnership Program for Creative Research Teams, the Sino-German CDZ project CAP (GZ 1023).

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China

    Pengfei Yang, David N. Jansen & Lijun Zhang

  2. University of Chinese Academy of Sciences, Beijing, China

    Pengfei Yang & Lijun Zhang

Authors
  1. Pengfei Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David N. Jansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lijun Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lijun Zhang .

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, United Kingdom

    Alessandro Abate

  2. Dept. d’Informatique, Université Libre de Bruxelles, Brussels, Belgium

    Gilles Geeraerts

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Yang, P., Jansen, D.N., Zhang, L. (2017). Distribution-Based Bisimulation for Labelled Markov Processes. In: Abate, A., Geeraerts, G. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2017. Lecture Notes in Computer Science(), vol 10419. Springer, Cham. https://doi.org/10.1007/978-3-319-65765-3_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-65765-3_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-65764-6

  • Online ISBN: 978-3-319-65765-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation