Document Open Access Logo

Explainability is a Game for Probabilistic Bisimilarity Distances

Authors Emily Vlasman , Anto Nanah Ji , James Worrell , Franck van Breugel

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.36.pdf
  • Filesize: 0.93 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Mathematics of computing → Probability and statistics
Keywords
  • probabilistic bisimilarity distance
  • labelled Markov chain
  • game
  • policy
  • explainability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We revisit a game from the literature that characterizes the probabilistic bisimilarity distances of a labelled Markov chain. We illustrate how an optimal policy of the game can explain these distances. Like the games that characterize bisimilarity and probabilistic bisimilarity, the game is played on pairs of states and matches transitions of those states. To obtain more convincing and interpretable explanations than those provided by generic optimal policies, we restrict to optimal policies that delay reaching observably inequivalent state pairs for as long as possible (called 1-maximal) while quickly reaching equivalent ones (called 0-minimal). We present iterative algorithms that compute 1-maximal and 0-minimal policies and prove an exponential lower bound for the number of iterations of the algorithm that computes 1-maximal policies.

Cite As Get BibTex

Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel. Explainability is a Game for Probabilistic Bisimilarity Distances. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.36

Author Details

Emily Vlasman
  • Department of Computer Science, Oxford University, UK
Anto Nanah Ji
  • Department of Electrical Engineering and Computer Science, York University, Toronto, Canada
James Worrell
  • Department of Computer Science, Oxford University, UK
Franck van Breugel
  • Department of Electrical Engineering and Computer Science, York University, Toronto, Canada

Funding

  • Worrell, James: EPSRC Fellowship EP/X033813/1.
  • van Breugel, Franck: Natural Sciences and Engineering Research Council of Canada.

Acknowledgements

The authors would like to thank the referees for their constructive feedback.

References

  1. Giorgio Bacci, Giovanni Bacci, Kim Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. In Nir Piterman and Scott Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 7795 of Lecture Notes in Computer Science, pages 1-15, Rome, Italy, March 2013. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-36742-7_1.
  2. Christel Baier, Calvin Chau, and Sascha Klüppelholz. Certificates and witnesses for multi-objective queries in Markov decision processes. In Jane Hillston, Sadegh Soudjani, and Masaki Waga, editors, Proceedings of the 1st International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, volume 14996 of Lecture Notes in Computer Science, pages 1-18, Calgary, Canada, September 2024. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-68416-6_1.
  3. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, Cambridge, MA, USA, 2008. Google Scholar
  4. Stefan Banach. Sur les opérations dans les ensembles abstraits et leurs applications aux equations intégrales. Fundamenta Mathematicae, 3:133-181, 1922. URL: https://doi.org/10.4064/fm-3-1-133-181.
  5. Franck van Breugel. On behavioural pseudometrics and closure ordinals. Information Processing Letters, 112(19):715-718, October 2012. URL: https://doi.org/10.1016/J.IPL.2012.06.019.
  6. Franck van Breugel. Probabilistic bisimilarity distances. SIGLOG News, 4(4):33-51, October 2017. URL: https://doi.org/10.1145/3157831.3157837.
  7. Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. An accessible approach to behavioural pseudometrics. In Luís Caires, Giuseppe Italiano, Luís Monteiro, Catuscia Palamidessi, and Moti Yung, editors, Proceedings of the 32nd International Colloquium on Automata, Languages and Programming, volume 3580 of Lecture Notes in Computer Science, pages 1018-1030, Lisbon, Portugal, July 2005. Springer-Verlag. URL: https://doi.org/10.1007/11523468_82.
  8. Damien Busatto-Gaston, Debraj Chakraborty, Anirban Majumdar, Sayan Mukherjee, Guillermo Pérez, and Jean-François Raskin. Bi-objective lexicographic optimization in Markov decision processes with related objectives. In Étienne André and Jun Sun, editors, Proceedings of the 21st International Symposium on Automated Technology for Verification and Analysis, volume 14215 of Lecture Notes in Computer Science, pages 203-223, Signapore, October 2023. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-45329-8_10.
  9. Pablo Castro, Pedro D’Argenio, Ramiro Demasi, and Luciano Putruele. Measuring masking fault-tolerance. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 11428 of Lecture Notes in Computer Science, pages 375-392, Prague, Czech Republic, April 2019. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-17465-1_21.
  10. Di Chen, Franck van Breugel, and James Worrell. On the complexity of computing probabilistic bisimilarity. In Lars Birkedal, editor, Proceedings of the 15th International Conference on Foundations of Software Science and Computational Structures, volume 7213 of Lecture Notes in Computer Science, pages 437-451, Tallinn, Estonia, March/April 2012. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-28729-9_29.
  11. Dmitry Chistikov, Andrzej Murawski, and David Purser. Bisimilarity distances for approximate differential privacy. In Shuvendu Lahiri and Chao Wang, editors, Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis, volume 11138 of Lecture Notes in Computer Science, pages 194-210, Los Angeles, CA, USA, October 2018. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-01090-4_12.
  12. Eric Denardo. Contraction mappings in the theory underlying dynamic programming. SIAM Review, 9(2):165-177, April 1967. URL: https://doi.org/10.1137/1009030.
  13. Salem Derisavi, Holger Hermanns, and William Sanders. Optimal state-space lumping in Markov chains. Information Processing Letters, 87(6):309-315, September 2003. URL: https://doi.org/10.1016/S0020-0190(03)00343-0.
  14. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled Markov systems. In Jos Baeten and Sjouke Mauw, editors, Proceedings of 10th International Conference on Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 258-273, Eindhoven, the Netherlands, August 1999. Springer-Verlag. URL: https://doi.org/10.1007/3-540-48320-9_19.
  15. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, June 2004. URL: https://doi.org/10.1016/J.TCS.2003.09.013.
  16. Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 413-422, Copenhagen, Denmark, July 2002. IEEE. URL: https://doi.org/10.1109/LICS.2002.1029849.
  17. Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate analysis of probabilistic processes: logic, simulation and games. In Proceedings of the 5th International Conference on the Quantitative Evaluation of Systems, pages 264-273, Saint-Malo, France, September 2008. IEEE. URL: https://doi.org/10.1109/QEST.2008.42.
  18. Wolfgang Doeblin. Exposé de la théorie des chaînes simples constantes de Markov à un nombre fini d'états. Revue mathématique de l'union interbalkanique, 2:77-105, 1938. Google Scholar
  19. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129-141, 1961. Google Scholar
  20. Yuan Feng, Runyao Duan, and Mingsheng Ying. Bisimulation for quantum processes. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 523-534, Austin, TX, USA, January 2011. ACM. URL: https://doi.org/10.1145/1926385.1926446.
  21. Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of probabilistic modal logics, revisited. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, Proceedings of 44th International Colloquium on Automata, Languages and Programming, volume 80 of Leibniz International Proceedings in Informatics, pages 105:1-105:12, Warsaw, Poland, July 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.ICALP.2017.105.
  22. Chase Ford, Harsh Beohar, Barbara König, Stefan Milius, and Lutz Schröder. Graded monads and behavioural equivalence games. In Christel Baier and Dana Fisman, editors, Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 61:1-61:13, Haifa, Israel, August 2022. ACM. URL: https://doi.org/10.1145/3531130.3533374.
  23. Vojtech Forejt, Petr Jancar, Stefan Kiefer, and James Worrell. Game characterization of probabilistic bisimilarity and applications to pushown automata. Logical Methods in Computer Science, 14(4:13), November 2018. URL: https://doi.org/10.23638/LMCS-14(4:13)2018.
  24. Roland Fraïssé. Sur une nouvelle classification des systèmes de relations. Comptes Rendus, 230:1022-1024, 1950. Google Scholar
  25. Alessandro Giacalone, Chi-Chang Jou, and Scott Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proceedings of the IFIP WG 2.2/2.3 Working Conference on Programming Concepts and Methods, pages 443-458, Sea of Gallilee, April 1990. North-Holland. Google Scholar
  26. Antoine Girard and George Pappas. Approximate bisimulation: A bridge between computer science and control theory. European Journal of Control, 17(5):568-578, September 2011. URL: https://doi.org/10.3166/EJC.17.568-578.
  27. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Jaco de Bakker and Jan van Leeuwen, editors, Proceedings of 7th International Colloquium on Automata, Languages and Programming, volume 85 of Lecture Notes in Computer Science, pages 299-309, Noordwijkerhout, the Netherlands, July 1980. Springer-Verlag. URL: https://doi.org/10.1007/3-540-10003-2_79.
  28. Ronald Howard. Dynamic programming and Markov processes. The MIT Press, Cambridge, MA, USA, 1960. Google Scholar
  29. Alon Itai and Michael Rodeh. Symmetry breaking in distributed networks. In Proceedings of the 2nd Annual Symposium on Foundations of Computer Science, pages 150-158, Nashville, TN, USA, October 1981. IEEE. URL: https://doi.org/10.1109/SFCS.1981.41.
  30. Bengt Jonsson and Kim Larsen. Specification and refinement of probabilistic processes. In Proceedings of the 6th Annual Symposium on Logic in Computer Science, pages 266-277, Amsterdam, the Netherlands, July 1991. IEEE. URL: https://doi.org/10.1109/LICS.1991.151651.
  31. Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, and David Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking. In Orna Grumberg and Michael Huth, editors, Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 87-101, Braga, Portugal, March/April 2007. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-71209-1_9.
  32. Bronisław Knaster. Un théorème sur les fonctions d'ensembles. Annales Polonici Mathematici, 6:133-134, 1928. Google Scholar
  33. Donald Knuth and Andrew Yao. The complexity of nonuniform random number generation. In Joseph Traub, editor, Proceedings of a Symposium on New Directions and Recent Results in Algorithms and Complexity, pages 375-428, Pittsburgh, PA, USA, April 1976. Academic Press. Google Scholar
  34. Ignace Kolodner. Fixed points. The American Mathematical Monthly, 71(9):906, October 1964. Google Scholar
  35. Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, and Ichiro Hasuo. Codensity games for bisimilarity. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1-13, Vancouver, Canada, June 2019. IEEE. URL: https://doi.org/10.1109/LICS.2019.8785691.
  36. Barbara König and Christina Mika-Michalski. (Metric) bisimulation games and real-valued modal logics for coalgebras. In Sven Schewe and Lijun Zhang, editors, Proceedings of the 29th International Conference on Concurrency Theory, volume 118 of Leibniz International Proceedings in Informatics, pages 37:1-37:17, Beijing, China, September 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.CONCUR.2018.37.
  37. Barbara König, Christina Mika-Michalski, and Lutz Schröder. Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas. In Daniela Petrisan and Jurriaan Rot, editors, Proceedings of the 5th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science, volume 12094 of Lecture Notes in Computer Science, pages 133-154, Dublin, Ireland, April 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-57201-3_8.
  38. Ilya Korsunsky, Kathleen McGovern, Tom LaGatta, Loes Olde Loohuis, Terri Grosso-Applewhite, Nancy Griffeth, and Bud Mishra. Systems biology of cancer: a challenging expedition for clinical and quantitative biologists. Frontiers in Bioengineering and Biotechnology, 2, August 2014. URL: https://doi.org/10.3389/fbioe.2014.00027.
  39. Kim Larsen and Arne Skou. Bisimulation through probabilistic testing. In Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, pages 344-352, Austin, TX, USA, January 1989. ACM. URL: https://doi.org/10.1145/75277.75307.
  40. Qiyuan Liu, Qi Zhou, Rui Yang, and Jie Wang. Robust representation learning by clustering with bisimulation metrics for visual reinforcement learning with distractions. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Proceedings of the AAAI Conference on Artificial Intelligence, Washington, CD, USA, February 2023. URL: https://doi.org/10.1609/aaai.v37i7.26063.
  41. Gary Miller. Riemann’s hypothesis and tests for primality. In William Rounds, Nancy Martin, Jack Carlyle, and Michael Harrison, editors, Proceedings of the 7th Annual ACM Symposium on Theory of Computing, pages 234-239, Albuquerque, NM, USA, May 1975. ACM. URL: https://doi.org/10.1145/800116.803773.
  42. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  43. Anto Nanah Ji. Explainabilty is a game for probabilistic bisimilarity distances. Master’s thesis, York University, Toronto, Canada, May 2025. Google Scholar
  44. David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Proceedings of 5th GI-Conference on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167-183, Karlsruhe, Germany, March 1981. Springer-Verlag. URL: https://doi.org/10.1007/BFB0017309.
  45. Martin Puterman. Markov Decision Processes. Wiley, Hoboken, NJ, USA, 1994. Google Scholar
  46. Michael Rabin. Probabilistic algorithm for testing primality. Journal of Number Theory, 12(1):128-138, February 1980. URL: https://doi.org/10.1016/0022-314X(80)90084-0.
  47. Amgad Rady and Franck van Breugel. Explainability of probabilistic bisimilarity distances for labelled Markov chains. In Orna Kupferman and Pawel Sobocinski, editors, Proceedings of the 26th International Conference on Foundations of Software Science and Computational Structures, volume 13992 of Lecture Notes in Computer Science, pages 285-307, Paris, France, April 2023. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-30829-1_14.
  48. Michael Reiter and Aviel Rubin. Crowds: anonymity for web transactions. ACM Transactions on Information and System Security, 1(1):66-92, November 1998. URL: https://doi.org/10.1145/290163.290168.
  49. Walter Rudin. Principles of Mathematical Analysis. McGraw Hill, New York, NY, USA, 1976. Google Scholar
  50. Colin Stirling. Modal and temporal logics for processes. In Faron Moller and Graham Birtwistle:, editors, Proceedings of 8th Banff Higher Order Workshop, volume 1043 of Lecture Notes in Computer Science, pages 149-237, Banff, Canada, August/September 1995. Springer-Verlag. URL: https://doi.org/10.1007/3-540-60915-6_5.
  51. Qiyi Tang. Computing probabilistic bisimilarity distances. PhD thesis, York University, Toronto, Canada, August 2018. Google Scholar
  52. Alfred Tarski. A lattice-theoretic fixed point theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, June 1955. URL: https://doi.org/10.2140/pjm.1955.5.285.
  53. Emily Vlasman. On logical and game characterizations of probabilistic bisimilarity distances for labelled Markov chains. Master’s thesis, University of Oxford, Oxford, UK, September 2023. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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