Document Open Access Logo

A Spectrum of Approximate Probabilistic Bisimulations

Authors Timm Spork , Christel Baier , Joost-Pieter Katoen , Jakob Piribauer , Tim Quatmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2024.37.pdf
  • Filesize: 0.85 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Random walks and Markov chains
Keywords
  • Markov chains
  • Approximate bisimulation
  • Abstraction
  • Model checking

Metrics

Abstract

This paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation, as well as a notion of ε-perturbed bisimulation that relates LMCs that can be made (exactly) probabilistically bisimilar by small perturbations of their transition probabilities. We explore how the notions interrelate and establish their connections to other well-known notions like ε-bisimulation.

Cite As Get BibTex

Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, and Tim Quatmann. A Spectrum of Approximate Probabilistic Bisimulations. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CONCUR.2024.37

Author Details

Timm Spork
  • Technische Universität Dresden, Dresden, Germany
Christel Baier
  • Technische Universität Dresden, Dresden, Germany
Joost-Pieter Katoen
  • RWTH Aachen University, Aachen, Germany
Jakob Piribauer
  • Technische Universität Dresden, Dresden, Germany
  • Universität Leipzig, Leipzig, Germany
Tim Quatmann
  • RWTH Aachen University, Aachen, Germany

Funding

Christel Baier, Jakob Piribauer and Timm Spork: This work was partly funded by the DFG Grant 389792660 as part of TRR 248 (Foundations of Perspicuous Software Systems) and the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy).
  • Quatmann, Tim: This research was funded by a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW.

Acknowledgements

We thank the reviewers for their helpful feedback, comments and suggestions. In particular, we thank the reviewer who pointed out the work in [Haesaert et al., 2021; Haesaert and Soudjani, 2021] on approximate simulation relations which we were previously not aware of.

References

  1. Alessandro Abate. Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: A survey. Electronic Notes in Theoretical Computer Science, 297:3-25, 2013. Proceedings of the first workshop on Hybrid Autonomous Systems. Google Scholar
  2. Alessandro Abate, Marta Kwiatkowska, Gethin Norman, and David Parker. Probabilistic model checking of labelled Markov processes via finite approximate bisimulations. In Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, and Jan Rutten, editors, Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday, volume 8464 of Lecture Notes in Computer Science (LNCS), pages 40-58. Springer International Publishing, Cham, 2014. Google Scholar
  3. Alessandro Aldini. A note on the approximation of weak probabilistic bisimulation, 2009. Google Scholar
  4. Alessandro Aldini, Mario Bravetti, Alessandra Di Pierro, Roberto Gorrieri, Chris Hankin, and Herbert Wiklicky. Two formal approaches for approximating noninterference properties. In Riccardo Focardi and Roberto Gorrieri, editors, Foundations of Security Analysis and Design II (FOSAD 2001), volume 2946 of Lecture Notes in Computer Science (LNCS), pages 1-43. Springer, Berlin, Heidelberg, 2004. Google Scholar
  5. Alessandro Aldini, Mario Bravetti, and Roberto Gorrieri. A process-algebraic approach for the analysis of probabilistic noninterference. J. Comput. Secur., 12(2):191-245, April 2004. Google Scholar
  6. Alessandro Aldini and Alessandra Di Pierro. A quantitative approach to noninterference for probabilistic systems. Electronic Notes in Theoretical Computer Science, 99:155-182, 2004. Proceedings of the MEFISTO Project 2003, Formal Methods for Security and Time. Google Scholar
  7. Alessandro Aldini and Roberto Gorrieri. Security analysis of a probabilistic non-repudiation protocol. In Holger Hermanns and Roberto Segala, editors, Process Algebra and Probabilistic Methods: Performance Modeling and Verification, volume 2399 of Lecture Notes in Computer Science (LNCS), pages 17-36. Springer, Berlin, Heidelberg, 2002. Google Scholar
  8. Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. It usually works: The temporal logic of stochastic systems. In Pierre Wolper, editor, Computer Aided Verification (CAV 1995), volume 939 of Lecture Notes in Computer Science (LNCS), pages 155-165, Berlin, Heidelberg, 1995. Springer, Berlin, Heidelberg. Google Scholar
  9. Christel Baier. Polynomial time algorithms for testing probabilistic bisimulation and simulation. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification (CAV 1996), volume 1102 of Lecture Notes in Computer Science (LNCS), pages 50-61. Springer, Berlin, Heidelberg, 1996. Google Scholar
  10. Christel Baier and Holger Hermanns. Weak bisimulation for fully probabilistic processes. In Orna Grumberg, editor, Computer Aided Verification (CAV 1997), volume 1254 of Lecture Notes in Computer Science (LNCS), pages 119-130. Springer, Berlin, Heidelberg, 1997. Google Scholar
  11. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  12. Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Verena Wolf. Comparative branching-time semantics for Markov chains. Information and Computation, 200(2):149-214, 2005. Google Scholar
  13. Massimo Bartoletti, Maurizio Murgia, and Roberto Zunino. Sound approximate and asymptotic probabilistic bisimulations for PCTL. Logical Methods in Computer Science, 19(1), 2023. Google Scholar
  14. Gaoang Bian and Alessandro Abate. On the relationship between bisimulation and trace equivalence in an approximate probabilistic context. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures (FoSSaCS), volume 10203 of Lecture Notes in Computer Science (LNCS), pages 321-337. Springer, Berlin, Heidelberg, 2017. Google Scholar
  15. Gaoang Bian and Alessandro Abate. On the relationship between bisimulation and trace equivalence in an approximate probabilistic context (extended version). CoRR, abs/1701.04547, 2017. Full version of [Bian and Abate, 2017]. URL: https://arxiv.org/abs/1701.04547.
  16. Béla Bollobás and Nicolas Th. Varopoulos. Representation of systems of measurable sets. Mathematical Proceedings of the Cambridge Philosophical Society, 78(2):323-325, 1975. Google Scholar
  17. Peter Buchholz. Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability, 31:59-75, January 1995. Google Scholar
  18. David de Frutos-Escrig, Jeroen J. A. Keiren, and Tim A. C. Willemse. Games for bisimulations and abstraction. CoRR, abs/1611.00401, 2016. URL: https://arxiv.org/abs/1611.00401.
  19. Salem Derisavi, Holger Hermanns, and William H. Sanders. Optimal state-space lumping in Markov chains. Information Processing Letters, 87(6):309-315, 2003. Google Scholar
  20. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled Markov systems. In Jos C. M. Baeten and Sjouke Mauw, editors, CONCUR'99 Concurrency Theory (CONCUR 1999), volume 1664 of Lecture Notes in Computer Science (LNCS), pages 258-273. Springer, Berlin, Heidelberg, 1999. Google Scholar
  21. Josée Desharnais, Abbas Edalat, and Prakash Panangaden. A logical characterization of bisimulation for labeled Markov processes. In Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LiCS), pages 478-487, 1998. Google Scholar
  22. Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. Information and Computation, 179(2):163-193, 2002. Google Scholar
  23. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Approximating labelled Markov processes. Information and Computation, 184(1):160-200, 2003. Google Scholar
  24. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Weak bisimulation is sound and complete for pCTL*. Information and Computation, 208(2):203-219, 2010. Google Scholar
  25. Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate analysis of probabilistic processes: Logic, simulation and games. In Fifth International Conference on Quantitative Evaluation of Systems (QEST 2008), pages 264-273, 2008. Google Scholar
  26. Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. Measuring the confinement of probabilistic systems. Theoretical Computer Science, 340(1):3-56, 2005. Theoretical Foundations of Security Analysis and Design II. Google Scholar
  27. Alessandro D'Innocenzo, Alessandro Abate, and Joost-Pieter Katoen. Robust PCTL model checking. In Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2012), pages 275-286, New York, NY, USA, 2012. Association for Computing Machinery. Google Scholar
  28. András Faragó. On the convergence rate of quasi lumpable Markov chains. In András Horváth and Miklós Telek, editors, Formal Methods and Stochastic Models for Performance Evaluation, volume 4054 of Lecture Notes in Computer Science (LNCS), pages 138-147. Springer, Berlin, Heidelberg, 2006. Google Scholar
  29. Giuliana Franceschinis and Richard R. Muntz. Bounds for quasi-lumpable markow chains. Perform. Evaluation, 20:223-243, 1994. Google Scholar
  30. Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Manfred Broy and Cliff B. Jones, editors, Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods, pages 443-458, 1990. Google Scholar
  31. Sofie Haesaert, Petter Nilsson, and Sadegh Soudjani. Formal multi-objective synthesis of continuous-state mdps. In 2021 American Control Conference (ACC), pages 3428-3433, 2021. Google Scholar
  32. Sofie Haesaert and Sadegh Soudjani. Robust dynamic programming for temporal logic control of stochastic systems. IEEE Transactions on Automatic Control, 66(6):2496-2511, 2021. Google Scholar
  33. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512-535, 1994. Google Scholar
  34. Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker storm. International Journal on Software Tools for Technology Transfer (STTT), 24:589-610, 2022. Google Scholar
  35. David N. Jansen, Jan Friso Groote, Ferry Timmers, and Pengfei Yang. A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:20, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  36. Joost-Pieter Katoen. The probabilistic model checking landscape. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS'16), pages 31-45, New York, NY, USA, 2016. Association for Computing Machinery. Google Scholar
  37. Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, and David N. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking. In Orna Grumberg and Michael Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), volume 4424 of Lecture Notes in Computer Science (LNCS), pages 87-101. Springer, Berlin, Heidelberg, 2007. Google Scholar
  38. Stefan Kiefer and Qiyi Tang. Approximate Bisimulation Minimisation. In Mikołaj Bojańczy and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), volume 213 of Leibniz International Proceedings in Informatics (LIPIcs), pages 48:1-48:16, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  39. Stefan Kiefer and Qiyi Tang. Approximate bisimulation minimisation. CoRR, abs/2110.00326, 2021. Full version of [Kiefer and Tang, 2021]. URL: https://arxiv.org/abs/2110.00326.
  40. Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. In Nicolas Halbwachs and Doron Peled, editors, Computer Aided Verification (CAV 1999), volume 1633 of Lecture Notes in Computer Science (LNCS), pages 172-183, Berlin, Heidelberg, 1999. Springer, Berlin, Heidelberg. Google Scholar
  41. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. Google Scholar
  42. R. Milner. Communication and Concurrency. Prentice-Hall, Inc., USA, 1989. Google Scholar
  43. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science (LNCS). Springer-Verlag, Berlin, Heidelberg, 1982. Google Scholar
  44. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pages 46-57, 1977. Google Scholar
  45. Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1995. Google Scholar
  46. Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. In Bengt Jonsson and Joachim Parrow, editors, CONCUR '94: Concurrency Theory, volume 836 of Lecture Notes in Computer Science (LNCS), pages 481-496. Springer, Berlin, Heidelberg, 1994. Google Scholar
  47. Mathieu Tracol, Josée Desharnais, and Abir Zhioua. Computing distances between probabilistic automata. In Mieke Massink and Gethin Norman, editors, Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), Saarbrücken, Germany, April 1-3, 2011, volume 57 of EPTCS, pages 148-162, 2011. Google Scholar
  48. Antti Valmari and Giuliana Franceschinis. Simple O(m logn) time Markov chain lumping. In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science (LNCS), pages 38-52, Berlin, Heidelberg, 2010. Springer, Berlin, Heidelberg. Google Scholar
  49. Franck van Breugel. Probabilistic bisimilarity distances. ACM SIGLOG News, 4(4):33-51, 2017. Google Scholar
  50. Rob J. van Glabbeek, Jan Friso Groote, and Erik P. de Vink. A complete axiomatization of branching bisimilarity for a simple process language with probabilistic choice. In Mário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, and Frank Valencia, editors, The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, volume 11760 of Lecture Notes in Computer Science (LNCS), pages 139-162, Cham, 2019. Springer International Publishing. Google Scholar
  51. Rob J. van Glabbeek and W. Peter Weijland. Branching time and abstraction in bisimulation semantics. J. ACM, 43(3):555-600, May 1996. Google Scholar
  52. Ralf Wimmer and Bernd Becker. Correctness issues of symbolic bisimulation computation for Markov chains. In Bruno Müller-Clostermann, Klaus Echtle, and Erwin P. Rathgeb, editors, Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB&DFT 2010), volume 5987 of Lecture Notes in Computer Science (LNCS), pages 287-301. Springer, Berlin, Heidelberg, 2010. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact