Document Open Access Logo

On the Continuity of the Probabilistic Bisimilarity Distance

Authors Syyeda Zainab Fatmi , Stefan Kiefer , David Parker , Franck van Breugel

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.34.pdf
  • Filesize: 1.06 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Verification by model checking
  • Theory of computation → Probabilistic computation
Keywords
  • probabilistic model checking
  • labelled Markov chain
  • probabilistic bisimilarity distance

Metrics

Abstract

The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity undermines its applicability to empirically derived models, where transition probabilities are often approximations. Recently, we introduced robust probabilistic bisimilarity as a sufficient condition for continuity at distance zero. In this paper, we show that it is also a necessary condition, that is, two states are robustly probabilistic bisimilar if and only if their probabilistic bisimilarity distance is small for any small enough perturbation of the transition probabilities. We further extend robustness to non-bisimilar state pairs to establish a complete characterization for continuity of the probabilistic bisimilarity distance. Based on this characterization, we develop a polynomial time algorithm to decide continuity. Finally, we complement our theoretical contributions with an experimental evaluation demonstrating the proposed approach in practice. Our results show that the extra step of deciding continuity requires minimal additional cost when compared to computing the probabilistic bisimilarity distance.

Cite As Get BibTex

Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel. On the Continuity of the Probabilistic Bisimilarity Distance. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.34

Author Details

Syyeda Zainab Fatmi
  • University of Oxford, UK
Stefan Kiefer
  • University of Oxford, UK
David Parker
  • University of Oxford, UK
Franck van Breugel
  • York University, Toronto, Canada

Funding

  • Fatmi, Syyeda Zainab: Clarendon Fund
  • Kiefer, Stefan: EPSRC grant EP/Z536179/1
  • van Breugel, Franck: Natural Sciences and Engineering Research Council of Canada

Supplementary Materials

References

  1. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. In Nir Piterman and Scott A. 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. URL: https://doi.org/10.1007/978-3-642-36742-7_1.
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. The MIT Press, Cambridge, MA, USA, 2008. Google Scholar
  3. Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, and Vishwanath Raman. Algorithms for game metrics (full version). Logical Methods in Computer Science, 6(3):1-27, 2010. URL: https://doi.org/10.48550/arXiv.0809.4326.
  4. 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.
  5. Anne Condon. On algorithms for simple stochastic games. In Jin-Yi Cai, editor, Advances In Computational Complexity Theory, volume 13 of Series in Discrete Mathematics and Theoretical Computer Science, pages 51-71, New Jersey, USA, December 1990. DIMACS/AMS. URL: https://doi.org/10.1090/DIMACS/013/04.
  6. Luca de Alfaro and Rupak Majumdar. Quantitative solution of omega-regular games. In Jeffrey Scott Vitter, Paul G. Spirakis, and Mihalis Yannakakis, editors, Proceedings of the 33rd Annual Symposium on Theory of Computing, pages 675-683, Heraklion, Crete, Greece, July 2001. ACM. URL: https://doi.org/10.1145/380752.380871.
  7. Salem Derisavi. Signature-based symbolic algorithm for optimal Markov chain lumping. In Proceedings of the 4th International Conference on the Quantitative Evaluation of Systems, pages 141-150, Edinburgh, Scotland, UK, September 2007. IEEE Computer Society. URL: https://doi.org/10.1109/QEST.2007.27.
  8. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled Markov systems. In Jos C. M. Baeten and Sjouke Mauw, editors, Proceedings of the 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.
  9. 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.
  10. Yefim Dinitz. Dinitz' algorithm: the original version and Even’s version. In Arnold L. Rosenberg Oded Goldreich and Alan L. Selman, editors, Theoretical Computer Science: Essays in Memory of Shimon Even, pages 218-240. Springer-Verlag, Berlin, Germany, 2006. URL: https://doi.org/10.1007/11685654_10.
  11. J. Ronald Eastman and Jiena He. A regression-based procedure for Markov transition probability estimation in land change modeling. Land, 9(11), October 2020. URL: https://doi.org/10.3390/land9110407.
  12. Syyeda Zainab Fatmi. Probabilistic model checking of randomized Java code. Master’s thesis, York University, Toronto, Canada, September 2020. URL: http://hdl.handle.net/10315/38445.
  13. Syyeda Zainab Fatmi, Xiang Chen, Yash Dhamija, Maeve Wildes, Qiyi Tang, and Franck van Breugel. Probabilistic model checking of randomized Java code. In Alfons Laarman and Ana Sokolova, editors, Proceedings of the 27th International Symposium on Model Checking Software, SPIN, volume 12864 of Lecture Notes in Computer Science, pages 157-174. Springer, July 2021. URL: https://doi.org/10.1007/978-3-030-84629-9_9.
  14. Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel. PRISM extension for deciding continuity of the probabilistic bisimilarity distance. Software, (visited on 2026-08-12). URL: https://github.com/zainabfatmi/prism/tree/concur
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27642
  15. Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel. Robust probabilistic bisimilarity for labelled Markov chains. In Ruzica Piskac and Zvonimir Rakamaric, editors, Proceedings of the 37th International Conference on Computer Aided Verification, volume 15932 of Lecture Notes in Computer Science, pages 254-275, Zagreb, Croatia, July 2025. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-98679-6_12.
  16. Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel. On the continuity of the probabilistic bisimilarity distance (full version). CoRR, June 2026. URL: https://arxiv.org/abs/2606.27209.
  17. Lester Randolph Ford and Delbert Ray Fulkerson. Flows in networks. Princeton University Press, Princeton, NJ, USA, 1962. Google Scholar
  18. 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 Working Conference on Programming Concepts and Methods, pages 443-458, Sea of Galilee, Israel, April 1990. North-Holland. Google Scholar
  19. Andrew V. Goldberg and Robert Endre Tarjan. Finding minimum-cost circulations by canceling negative cycles. Journal of the ACM, 36(4):873-886, October 1989. URL: https://doi.org/10.1145/76359.76368.
  20. Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, and Enno Ruijters. The quantitative verification benchmark set. In Tomás Vojnar and Lijun Zhang, editors, Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 11427 of Lecture Notes in Computer Science, pages 344-350, Prague, Czech Republic, April 2019. Springer. URL: https://doi.org/10.1007/978-3-030-17462-0_20.
  21. Manfred Jaeger, Hua Mao, Kim Guldstrand Larsen, and Radu Mardare. Continuity properties of distances for Markov processes. In Gethin Norman and William H. Sanders, editors, Proceedings of the 11th International Conference on Quantitative Evaluation of Systems, volume 8657 of Lecture Notes in Computer Science, pages 297-312, Florence, Italy, September 2014. Springer-Verlag. URL: https://doi.org/10.1007/978-3-319-10696-0_24.
  22. 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.
  23. Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, and David N. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking. In 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 2007. Springer. URL: https://doi.org/10.1007/978-3-540-71209-1_9.
  24. John G. Kemeny and J. Laurie Snell. Finite Markov chains. Springer-Verlag, Heidelberg, Germany, 1960. Google Scholar
  25. Morton Klein. A primal method for minimal cost flows with applications to the assignment and transportation problems. Management Science, 14(3):205-220, November 1967. URL: https://doi.org/10.1287/mnsc.14.3.205.
  26. Dexter Kozen. A probabilistic PDL. In David S. Johnson, Ronald Fagin, Michael L. Fredman, David Harel, Richard M. Karp, Nancy A. Lynch, Christos H. Papadimitriou, Ronald L. Rivest, Walter L. Ruzzo, and Joel I. Seiferas, editors, Proceedings of the 15th Annual Symposium on Theory of Computing, pages 291-297, Boston, Massachusetts, USA, April 1983. ACM. URL: https://doi.org/10.1145/800061.808758.
  27. Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 585-591, Snowbird, Utah, USA, July 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-22110-1_47.
  28. 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.
  29. Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York, NY, USA, 2004. URL: https://doi.org/10.1007/B138392.
  30. Daijiro Mizutani, Nam Lethanh, Bryan T. Adey, and Kiyoyuki Kaito. Improving the estimation of Markov transition probabilities using mechanistic-empirical models. Frontiers in Built Environment, 3:58, October 2017. URL: https://doi.org/10.3389/fbuil.2017.00058.
  31. Elena Olariu, Kevin K. Cadwell, Elizabeth Hancock, David Trueman, and Helene Chevrou-Severac. Current recommendations on the estimation of transition probabilities in Markov cohort models for use in health care decision-making: a targeted literature review. ClinicoEconomics and Outcomes Research, 9:537-546, September 2017. URL: https://doi.org/10.2147/CEOR.S135445.
  32. Laurent Perron and Vincent Furnon. OR-Tools. URL: https://developers.google.com/optimization/.
  33. Tushar Srivastava, Nicholas R. Latimer, and Paul Tappenden. Estimation of transition probabilities for state-transition models: a review of NICE appraisals. PharmacoEconomics, 39(8):869-878, August 2021. URL: https://doi.org/10.1007/s40273-021-01034-5.
  34. Qiyi Tang. Computing probabilistic bisimilarity distances. PhD thesis, York University, Toronto, Canada, August 2018. URL: http://hdl.handle.net/10315/35586.
  35. Qiyi Tang and Franck van Breugel. Computing probabilistic bisimilarity distances via policy iteration. In Josée Desharnais and Radha Jagadeesan, editors, Proceedings of the 27th International Conference on Concurrency Theory, volume 59 of LIPIcs, pages 22:1-22:15, Québec City, Canada, August 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.22.
  36. Qiyi Tang and Franck van Breugel. Algorithms to compute probabilistic bisimilarity distances for labelled Markov chains. In Roland Meyer and Uwe Nestmann, editors, Proceedings of the 28th International Conference on Concurrency Theory, volume 85 of LIPIcs, pages 27:1-27:16, Berlin, Germany, September 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.27.
  37. Qiyi Tang and Franck van Breugel. Deciding probabilistic bisimilarity distance one for labelled Markov chains. In Hana Chockler and Georg Weissenbacher, editors, Proceedings of the 30th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, pages 681-699, Oxford, UK, July 2018. Springer. URL: https://doi.org/10.1007/978-3-319-96145-3_39.
  38. Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Park, and Flavio Lerda. Model checking programs. Automated Software Engineering, 10(2):203-232, April 2003. URL: https://doi.org/10.1023/A:1022920129859.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact