Document Open Access Logo

Constructing Witnesses for Lower Bounds on Behavioural Distances

Authors Ruben Turkenburg , Harsh Beohar , Franck van Breugel , Clemens Kupke , Jurriaan Rot

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.25.pdf
  • Filesize: 1.11 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Probabilistic computation
  • Theory of computation → Logic
  • Theory of computation → Modal and temporal logics
Keywords
  • Behavioural Distances
  • Markov Chains
  • Apartness

Metrics

Abstract

Behavioural distances provide a robust alternative to notions of equivalence such as bisimilarity in the context of probabilistic transition systems. They can be defined as least fixed points, whose universal property allows us to exhibit upper bounds on the distance between states, showing them to be at most some distance apart.
In this paper, we instead consider the problem of bounding distances from below, showing states to be at least some distance apart. Contrary to upper bounds, it is possible to reason about lower bounds inductively. We exploit this by giving an inductive derivation system for lower bounds on an existing definition of behavioural distance for labelled Markov chains. This is inspired by recent work on apartness as an inductive counterpart to bisimilarity. Proofs in our system will be shown to closely match the behavioural distance by soundness and (approximate) completeness results.
We further provide a constructive correspondence between our derivation system and formulas in a modal logic with quantitative semantics. This logic was used in recent work of Rady and van Breugel to construct evidence for lower bounds on behavioural distances. Our constructions provide smaller witnessing formulas in many examples.

Cite As Get BibTex

Ruben Turkenburg, Harsh Beohar, Franck van Breugel, Clemens Kupke, and Jurriaan Rot. Constructing Witnesses for Lower Bounds on Behavioural Distances. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.25

Author Details

Ruben Turkenburg
  • Radboud University, Nijmegen, The Netherlands
Harsh Beohar
  • University of Sheffield, UK
Franck van Breugel
  • York University, Toronto, Canada
Clemens Kupke
  • University of Strathclyde, Glasgow, UK
Jurriaan Rot
  • Radboud University, Nijmegen, The Netherlands

Funding

This research is partially supported by the NWO grant No. OCENW.M20.053.
  • Beohar, Harsh: EPSRC Grant: EP/X019373/1 and Royal Society Grant: IES\R3\223092.
  • van Breugel, Franck: Natural Sciences and Engineering Research Council of Canada.
  • Kupke, Clemens: Leverhulme Trust Research Project Grant RPG-2020-232.

Acknowledgements

This work has benefitted from Dagstuhl Seminar 24432: Behavioural Metrics and Quantitative Logics.

References

  1. Robert B Ash. Real Analysis and Probability: Probability and Mathematical Statistics: A Series of Monographs and Textbooks. Academic press, 1972. Google Scholar
  2. 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.
  3. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. A complete quantitative deduction system for the bisimilarity distance on Markov chains. Log. Methods Comput. Sci., 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:15)2018.
  4. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing probabilistic bisimilarity distances for probabilistic automata. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7147.
  5. 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.
  6. Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. Fixpoint theory - upside down. Log. Methods Comput. Sci., 19(2), 2023. URL: https://doi.org/10.46298/LMCS-19(2:15)2023.
  7. 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.
  8. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Informatica, 54(2):127-190, 2017. URL: https://doi.org/10.1007/S00236-016-0271-4.
  9. Peter Buchholz. Exact and ordinary lumpability in finite Markov chains. Journal of applied probability, 31(1):59-75, 1994. Google Scholar
  10. Pablo Samuel Castro, Tyler Kastner, Prakash Panangaden, and Mark Rowland. Mico: Improved representations via sampling-based state similarity for markov decision processes. In NeurIPS, pages 30113-30126, 2021. URL: https://proceedings.neurips.cc/paper/2021/hash/fd06b8ea02fe5b1c2496fe1700e9d16c-Abstract.html.
  11. Di Chen, Franck van Breugel, and James Worrell. On the complexity of computing probabilistic bisimilarity. In FoSSaCS, volume 7213 of Lecture Notes in Computer Science, pages 437-451. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_29.
  12. Taolue Chen and Stefan Kiefer. On the total variation distance of labelled Markov chains. In CSL-LICS, pages 33:1-33:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603099.
  13. Josée Desharnais, Abbas Edalat, and Prakash Panangaden. A logical characterization of bisimulation for labeled Markov processes. In LICS, pages 478-487. IEEE Computer Society, 1998. URL: https://doi.org/10.1109/LICS.1998.705681.
  14. Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. Inf. Comput., 179(2):163-193, 2002. URL: https://doi.org/10.1006/INCO.2001.2962.
  15. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled Markov systems. In CONCUR, volume 1664 of Lecture Notes in Computer Science, pages 258-273. Springer, 1999. URL: https://doi.org/10.1007/3-540-48320-9_19.
  16. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. URL: https://doi.org/10.1016/J.TCS.2003.09.013.
  17. Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In LICS, pages 413-422. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029849.
  18. Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate analysis of probabilistic processes: Logic, simulation and games. In QEST, pages 264-273. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/QEST.2008.42.
  19. Josée Desharnais and Ana Sokolova. ε-distance via lévy-prokhorov lifting. CoRR, abs/2507.10732, 2025. URL: https://doi.org/10.48550/arXiv.2507.10732.
  20. Alessandro D'Innocenzo, Alessandro Abate, and Joost-Pieter Katoen. Robust PCTL model checking. In HSCC, pages 275-286. ACM, 2012. URL: https://doi.org/10.1145/2185632.2185673.
  21. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for finite Markov decision processes. In AAAI, pages 950-951. AAAI Press/The MIT Press, 2004. URL: http://www.aaai.org/Library/AAAI/2004/aaai04-124.php.
  22. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for Markov decision processes with infinite state spaces. In UAI, pages 201-208. AUAI Press, 2005. URL: https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=1175&proceeding_id=21.
  23. Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of probabilistic modal logics, revisited. In ICALP, volume 80 of LIPIcs, pages 105:1-105:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.105.
  24. Herman Geuvers. Apartness and distinguishing formulas in Hennessy-Milner logic. In A Journey from Process Algebra via Timed Automata to Model Learning, volume 13560 of Lecture Notes in Computer Science, pages 266-282. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15629-8_14.
  25. Herman Geuvers and Bart Jacobs. Relating apartness and bisimulation. Log. Methods Comput. Sci., 17(3), 2021. URL: https://doi.org/10.46298/LMCS-17(3:15)2021.
  26. Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Programming Concepts and Methods, pages 443-458. North-Holland, 1990. Google Scholar
  27. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Kantorovich functors and characteristic logics for behavioural distances. In FoSSaCS, 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.
  28. Claudio Hermida and Bart Jacobs. Structural induction and coinduction in a fibrational setting. Inf. Comput., 145(2):107-152, 1998. URL: https://doi.org/10.1006/INCO.1998.2725.
  29. Arend Heyting. Intuitionism: an introduction, volume 41. Elsevier, 1966. Google Scholar
  30. Bart Jacobs. Structured probabilistic reasoning. Unpublished draft. URL: http://www.cs.ru.nl/B.Jacobs/PAPERS/ProbabilisticReasoning.pdf.
  31. Leonid Vasilevich Kantorovich and SG Rubinshtein. On a space of totally additive functions. Vestnik of the St. Petersburg University: Mathematics, 13(7):52-59, 1958. Google Scholar
  32. Shin-ya Katsumata, Tetsuya Sato, and Tarmo Uustalu. Codensity lifting of monads and its dual. Log. Methods Comput. Sci., 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:6)2018.
  33. Stephen C. Kleene. Introduction to Metamathematics. D. van Nostrand, Princeton, New Jersey, 1952. Google Scholar
  34. Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Samuel Humeau, Clovis Eberhart, and Ichiro Hasuo. Codensity games for bisimilarity. New Gener. Comput., 40(2):403-465, 2022. URL: https://doi.org/10.1007/S00354-022-00186-Y.
  35. Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo. Expressivity of quantitative modal logics: Categorical foundations via codensity and approximation. In LICS, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470656.
  36. Barbara König and Christina Mika-Michalski. (Metric) bisimulation games and real-valued modal logics for coalgebras. In CONCUR, volume 118 of LIPIcs, pages 37:1-37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. 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 CMCS, volume 12094 of Lecture Notes in Computer Science, pages 133-154. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-57201-3_8.
  38. Dexter Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, 1985. URL: https://doi.org/10.1016/0022-0000(85)90012-1.
  39. S. Kullback and R. A. Leibler. On Information and Sufficiency. The Annals of Mathematical Statistics, 22(1):79-86, 1951. URL: https://doi.org/10.1214/aoms/1177729694.
  40. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In LICS, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  41. Jan Martens and Jan Friso Groote. Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable. In CONCUR, volume 279 of LIPIcs, pages 32:1-32:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2023.32.
  42. Jan Martens and Jan Friso Groote. Minimal depth distinguishing formulas without until for branching bisimulation. In Logics and Type Systems in Theory and Practice, volume 14560 of Lecture Notes in Computer Science, pages 188-202. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-61716-4_12.
  43. Yu V Prokhorov. Convergence of random processes and limit theorems in probability theory. Theory of Probability & Its Applications, 1(2):157-214, 1956. Google Scholar
  44. Amgad Rady and Franck van Breugel. Explainability of probabilistic bisimilarity distances for labelled Markov chains. In FoSSaCS, volume 13992 of Lecture Notes in Computer Science, pages 285-307. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_14.
  45. Wojciech Rozowski. A complete quantitative axiomatisation of behavioural distance of regular expressions. In ICALP, volume 297 of LIPIcs, pages 149:1-149:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.149.
  46. Jan J. M. M. Rutten. Relators and metric bisimulations. In CMCS, volume 11 of Electronic Notes in Theoretical Computer Science, pages 252-258. Elsevier, 1998. URL: https://doi.org/10.1016/S1571-0661(04)00063-5.
  47. Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, and Tim Quatmann. A spectrum of approximate probabilistic bisimulations. In CONCUR, volume 311 of LIPIcs, pages 37:1-37:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.37.
  48. 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.
  49. Qiyi Tang. Computing Probabilistic Bisimilarity Distances. PhD thesis, York University, Toronto, 2018. Google Scholar
  50. Kathleen Trustrum. Linear programming. Springer, 1971. Google Scholar
  51. Ruben Turkenburg, Harsh Beohar, Clemens Kupke, and Jurriaan Rot. Proving behavioural apartness. In CMCS, volume 14617 of Lecture Notes in Computer Science, pages 156-173. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-66438-0_8.
  52. Franck van Breugel. A behavioural pseudometric for metric labelled transition systems. In CONCUR, volume 3653 of Lecture Notes in Computer Science, pages 141-155. Springer, 2005. URL: https://doi.org/10.1007/11539452_14.
  53. Franck van Breugel. On behavioural pseudometrics and closure ordinals. Inf. Process. Lett., 112(19):715-718, 2012. URL: https://doi.org/10.1016/J.IPL.2012.06.019.
  54. Franck van Breugel. Probabilistic bisimilarity distances. ACM SIGLOG News, 4(4):33-51, 2017. URL: https://doi.org/10.1145/3157831.3157837.
  55. 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.
  56. Franck van Breugel, Babita Sharma, and James Worrell. Approximating a behavioural pseudometric without discount for probabilistic systems. Log. Methods Comput. Sci., 4(2), 2008. URL: https://doi.org/10.2168/LMCS-4(2:2)2008.
  57. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115-142, 2005. URL: https://doi.org/10.1016/J.TCS.2004.09.035.
  58. Cédric Villani et al. Optimal transport: old and new, volume 338. Springer, 2008. Google Scholar
  59. Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel. Explainability is a game for probabilistic bisimilarity distances. In CONCUR, volume 348 of LIPIcs, pages 36:1-36:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2025.36.
  60. Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Quasilinear-time computation of generic modal witnesses for behavioural inequivalence. Log. Methods Comput. Sci., 18(4), 2022. URL: https://doi.org/10.46298/LMCS-18(4:6)2022.
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