Document Open Access Logo

ε-Distance via Lévy-Prokhorov Lifting

Authors Josée Desharnais , Ana Sokolova

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.26.pdf
  • Filesize: 0.85 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Probabilistic computation
  • Theory of computation → Categorical semantics
  • Theory of computation → Program verification
Keywords
  • Lévy-Prokhorov metric
  • behavioural distance
  • epsilon-bisimulation
  • reactive probabilistic transition systems
  • discrete labelled Markov processes
  • coalgebraic epsilon-(bi)simulation

Metrics

Abstract

The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. It is also the foundation for a categorical lifting of pseudometrics.
Other notions of behavioural pseudometrics have also been proposed, one of them (ε-distance) based on ε-bisimulation. ε-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of ε-coupling. Finally, this distance is easy to compute.
We show that ε-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokhorov distance. In addition, we show that ε-couplings and ε-bisimulations have an appealing coalgebraic characterization.

Cite As Get BibTex

Josée Desharnais and Ana Sokolova. ε-Distance via Lévy-Prokhorov Lifting. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 26:1-26:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.26

Author Details

Josée Desharnais
  • Laval University, Québec, Canada
Ana Sokolova
  • University of Salzburg, Austria

Funding

  • Desharnais, Josée: Work funded by NSERC grant.

Acknowledgements

This work was partly done during a sabbatical of Josée Desharnais at the University of Salzburg, as well as during Dagstuhl Seminar 24432 and the Bellairs Workshop on Quantitative Reasoning 2025. We thank these venues, the organizers, and the participants for providing a perfect working environment. We also thank Matteo Mio and Franck van Breugel for some fruitful and motivating discussions, and the anonymous reviewers for their insightful and constructive suggestions.

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. URL: https://doi.org/10.1016/j.entcs.2013.12.002.
  2. Alessandro Abate, Marta Z. 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, pages 40-58. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06880-0_2.
  3. Peter Aczel and Nax Mendler. A final coalgebra theorem. In Proc. 3^rd CTCS, volume 389 of LNCS, pages 357-365. Springer, 1989. URL: https://doi.org/10.1007/BFB0018361.
  4. Pedro Azevedo de Amorim, Mayuko Kori, and Koko Muroya. A framework for coalgebraic reward-sensitive bisimulation, 2025. Google Scholar
  5. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-fly computation of bisimilarity distances. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:13)2017.
  6. Giovanni Bacci, Giorgio Bacci, Kim G. Larsen, and Radu Mardare. On the metric-based approximate minimization of markov chains. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 104:1-104:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.104.
  7. C. Baier. On Algorithmic Verification Methods for Probabilistic Systems. Habilitation Thesis, 1998. Google Scholar
  8. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  9. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  10. 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 - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 321-337, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_19.
  11. Richard Blute, Josée Desharnais, Abbas Edalat, and Panangaden Panangaden. Bisimulation for labelled Markov processes. In Proceedings of the Twelfth IEEE Symposium On Logic In Computer Science (LICS), Warsaw, Poland, 1997. Google Scholar
  12. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. Math. Struct. Comput. Sci., 33(4-5):182-221, 2023. URL: https://doi.org/10.1017/S0960129523000166.
  13. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In CONCUR 2017, volume 85, pages 23:1-23:18. LIPIcs, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
  14. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism, probability, and termination. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:21)2022.
  15. Nicolas Bourbaki. Elements of Mathematics. Springer-Verlag, 1995. Original French edition published by MASSON, Paris in 1971. Google Scholar
  16. Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Rozowski, and Paul Wild. Behavioural metrics: Compositionality of the kantorovich lifting and an application to up-to techniques. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory, CONCUR 2024, September 9-13, 2024, Calgary, Canada, volume 311 of LIPIcs, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.20.
  17. Vincent Danos, Josée Desharnais, François Laviolette, and Prakash Panangaden. Bisimulation and cocongruence for probabilistic systems. Information and Computation, 2005. Special issue for selected papers from CMCS04. 22 pages. Google Scholar
  18. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching metrics for quantitative transition systems. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, volume 3142 of Lecture Notes in Computer Science, pages 97-109. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_11.
  19. Luca de Alfaro and Rupak Majumdar. Quantitative solution of omega-regular games. In STOC '01: Proceedings of the thirty-third annual ACM symposium on Theory of computing, pages 675-683, New York, NY, USA, 2001. ACM. URL: https://doi.org/10.1145/380752.380871.
  20. Erik P. de Vink and Jan J. M. M. Rutten. Bisimulation for probabilistic transition systems: A coalgebraic approach. Theor. Comput. Sci., 221(1-2):271-293, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00035-3.
  21. Josée Desharnais. Labelled Markov Processes. PhD thesis, McGill University, 2000. Google Scholar
  22. Josée Desharnais, Vineet Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labeled Markov processes. In Jos C. M. Baeten and S. Mauw, editors, Proceedings of 10th International Conference on Concurrency Theory, Eindhoven, The Netherlands, Lecture Notes in Computer Science, pages 258-273. Springer-Verlag, August 1999. Google Scholar
  23. Josée Desharnais, Vineet Gupta, R. Jagadeesan, and P. Panangaden. Approximating continuous Markov processes. In Proceedings of the 15th Annual IEEE Symposium On Logic In Computer Science, Santa Barbara, Californie, USA, 2000. pp. 95-106. Google Scholar
  24. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, 2004. URL: https://doi.org/10.1016/j.tcs.2003.09.013.
  25. Josée Desharnais, R. Jagadeesan, Vineet Gupta, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS02), pages 413-422, Copenhagen, Denmark, July 2002. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2002.1029849.
  26. Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate analysis of probabilistic processes: Logic, simulation and games. In Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), 14-17 September 2008, Saint-Malo, France, pages 264-273. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/QEST.2008.42.
  27. Alessandro D'Innocenzo, Alessandro Abate, and Joost-Pieter Katoen. Robust PCTL model checking. In Thao Dang and Ian M. Mitchell, editors, Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC'12, Beijing, China, April 17-19, 2012, pages 275-286. ACM, 2012. URL: https://doi.org/10.1145/2185632.2185673.
  28. A. Giacalone, P.Misra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. In LNCS 352: TAPSOFT 89, 1989. Google Scholar
  29. Alessandro Giacalone, Chi chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, pages 443-458. North-Holland, 1990. Google Scholar
  30. Antoine Girard and George J. Pappas. Approximate bisimulation relations for constrained linear systems. Automatica, 43(8):1307-1317, 2007. URL: https://doi.org/10.1016/j.automatica.2007.01.019.
  31. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Kantorovich functors and characteristic logics for behavioural distances. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 46-67. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_3.
  32. Ichiro Hasuo. Generic forward and backward simulations. In CONCUR 2006, pages 406-420. LNCS 4137, 2006. URL: https://doi.org/10.1007/11817949_27.
  33. Ichiro Hasuo. Generic forward and backward simulations II: probabilistic simulation. In CONCUR 2010, pages 447-461. LNCS 6269, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_31.
  34. Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theor. Comput. Sci., 327(1-2):71-108, 2004. URL: https://doi.org/10.1016/J.TCS.2004.07.022.
  35. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  36. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859-879, 2015. URL: https://doi.org/10.1016/J.JCSS.2014.12.005.
  37. Dexter Kozen. Semantics of probabilistic programs. Journal of Computer and Systems Sciences, 22:328-350, 1981. URL: https://doi.org/10.1016/0022-0000(81)90036-2.
  38. Kim G. Larsen and Arne Skou. Bisimulation through probablistic testing. Information and Computation, 94:1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  39. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  40. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. On the axiomatizability of quantitative algebras. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005102.
  41. R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  42. Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470717.
  43. Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Universal quantitative algebra for fuzzy relations and generalised metric spaces. Log. Methods Comput. Sci., 20(4), 2024. URL: https://doi.org/10.46298/LMCS-20(4:19)2024.
  44. Prakash Panangaden. Labelled Markov Processes. Imperial College Press, 2009. Google Scholar
  45. Yu. V. Prokhorov. Convergence of random processes and limit theorems in probability theory. Theory of Probability & Its Applications, 1(2):157-214, 1956. URL: https://doi.org/10.1137/1101016.
  46. Jurriaan Rot and Thorsten Wißmann. Bisimilar states in uncertain structures. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, Indiana University Bloomington, IN, USA, June 19-21, 2023, volume 270 of LIPIcs, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CALCO.2023.12.
  47. J.J.M.M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249:3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  48. R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. In Proc. Concur'94, pages 481-496. LNCS 836, 1994. Google Scholar
  49. A. Sokolova. Coalgebraic Analysis of Probabilistic Systems. PhD thesis, TU Eindhoven, 2005. Google Scholar
  50. Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, and Tim Quatmann. A spectrum of approximate probabilistic bisimulations. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory, CONCUR 2024, September 9-13, 2024, Calgary, Canada, volume 311 of LIPIcs, pages 37:1-37:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, August 2024. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.37.
  51. David Sprunger, Shin-ya Katsumata, Jérémy Dubut, and Ichiro Hasuo. Fibrational bisimulations and quantitative reasoning. In Corina Cîrstea, editor, Coalgebraic Methods in Computer Science, pages 190-213, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-00389-0_11.
  52. David Sprunger, Shin-ya Katsumata, Jérémy Dubut, and Ichiro Hasuo. Fibrational bisimulations and quantitative reasoning: Extended version. J. Log. Comput., 31(6):1526-1559, 2021. URL: https://doi.org/10.1093/LOGCOM/EXAB051.
  53. Qiyi Tang and Franck van Breugel. Algorithms to compute probabilistic bisimilarity distances for labelled markov chains. In Proc. CONCUR 2017, volume 85 of LIPIcs, pages 27:1-27:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.27.
  54. 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. URL: https://doi.org/10.4204/EPTCS.57.11.
  55. Franck van Breugel. Probabilistic bisimilarity distances. ACM SIGLOG News, 4(4):33-51, November 2017. URL: https://doi.org/10.1145/3157831.3157837.
  56. Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. Recursively defined metric spaces without contraction. Theor. Comput. Sci., 380(1-2):143-163, 2007. URL: https://doi.org/10.1016/j.tcs.2007.02.059.
  57. Franck van Breugel, Babita Sharma, and James Worrell. Approximating a behavioural pseudometric without discount for probabilistic systems. In Helmut Seidl, editor, FoSSaCS, volume 4423 of Lecture Notes in Computer Science, pages 123-137. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71389-0_10.
  58. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In ICALP '01: Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, pages 421-432, London, UK, 2001. Springer-Verlag. URL: https://doi.org/10.1007/3-540-48224-5_35.
  59. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115-142, February 2005. URL: https://doi.org/10.1016/j.tcs.2004.09.035.
  60. Rob J. van Glabbeek, Scott A. Smolka, and Bernhard Steffen. Reactive, generative and stratified models of probabilistic processes. Inf. Comput., 121(1):59-80, 1995. URL: https://doi.org/10.1006/inco.1995.1123.
  61. Mingsheng Ying and Martin Wirsing. Approximate bisimilarity. In AMAST '00: Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, pages 309-322, London, UK, 2000. Springer-Verlag. URL: https://doi.org/10.1007/3-540-45499-3_23.
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