Document Open Access Logo

Threshold-Based Behavioural Distances

Authors Jonas Forster , Lutz Schröder , Paul Wild , Barbara König , Pedro Nora

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.35.pdf
  • Filesize: 0.87 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Modal and temporal logics
Keywords
  • Behavioural distance
  • modal logic
  • quantitative logic
  • coalgebra
  • Sugeno integration

Metrics

Abstract

Behavioural distances generally offer more fine-grained means of comparing quantitative systems than two-valued behavioural equivalences. They often relate to quantitative modal logics that characterize a given behavioural distance in terms of the induced logical distance. We develop a unified framework for behavioural distances and logics induced by a special type of modalities that lift two-valued predicates to quantitative predicates. A typical example is the probability operator, which maps a two-valued predicate A to a quantitative predicate on probability distributions assigning to each distribution the respective probability of A. Correspondingly, the prototypical example of our framework is ε-bisimulation distance of Markov chains, which has recently been shown to coincide with the behavioural distance induced by the popular Lévy-Prokhorov distance on distributions. Other examples include behavioural distance on metric transition systems and Hausdorff behavioural distance on fuzzy transition systems. We establish a number of general results in this framework, including existence and polynomial-time computation of distinguishing formulae in two characteristic modal logics: A two-valued logic with a notion of satisfaction up to ε, and a quantitative logic. These general results instantiate to new results in many of the mentioned examples. Notably, we obtain polynomial-time computation of distinguishing formulae for ε-bisimulation distance of Markov chains in a quantitative logic featuring a "generally" modality used in probabilistic knowledge representation.

Cite As Get BibTex

Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, and Pedro Nora. Threshold-Based Behavioural Distances. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.35

Author Details

Jonas Forster
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Paul Wild
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Barbara König
  • Universität Duisburg-Essen, Germany
Pedro Nora
  • Universität Duisburg-Essen, Germany

Funding

Research funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project numbers 434050016 (Jonas Forster, Barbara König, Pedro Nora, Lutz Schröder), 531706730 (Lutz Schröder) and 419850228 (Paul Wild).

References

  1. Peter Aczel and Nax Paul Mendler. A final coalgebra theorem. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, CTCS 1989, LNCS, pages 357-365. Springer, 1989. URL: https://doi.org/10.1007/BFB0018361.
  2. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories: The joy of cats. John Wiley & Sons Inc., 1990. Republished in: Reprints in Theory and Applications of Categories, No. 17 (2006) pp. 1-507. URL: http://tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
  3. Liviu Aolaritei, Oliver Wang, Julie Zhu, Michael Jordan, and Youssef Marzouk. Conformal prediction under Lévy-Prokhorov distribution shifts: Robustness to local and global perturbations. In Neural Information Processing Systems, NeurIPS 2025, 2025. To appear. Preprint available at https://arxiv.org/abs/2502.14105. URL: https://doi.org/10.48550/arXiv.2502.14105.
  4. Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. Polynomial relators (extended abstract). In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo, editors, Algebraic Methodology and Software Technology, AMAST 1991, Workshops in Computing, pages 303-326. Springer, 1991. Google Scholar
  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. Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299-315, 1993. URL: https://doi.org/10.1016/0304-3975(93)90076-6.
  7. Falk Bartels, Ana Sokolova, and Erik P. de Vink. A hierarchy of probabilistic system types. Theor. Comput. Sci., 327(1-2):3-22, 2004. URL: https://doi.org/10.1016/J.TCS.2004.07.019.
  8. Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin. Probabilistic relational reasoning for differential privacy. In John Field and Michael Hicks, editors, Principles of Programming Languages, POPL 2012, pages 97-110. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103670.
  9. M. Amine Bennouna, Ryan Lucas, and Bart P. G. Van Parys. Certified robust neural networks: Generalization and corruption resistance. In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett, editors, International Conference on Machine Learning, ICML 2023, volume 202 of Proc. Machine Learning Res., pages 2092-2112. PMLR, 2023. URL: https://proceedings.mlr.press/v202/bennouna23a.html.
  10. Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-milner theorems via galois connections. In Bartek Klin and Elaine Pimentel, editors, Computer Science Logic, CSL 2023, LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.12.
  11. Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer Aided Verification, CAV 1990, volume 531 of LNCS, pages 364-372. Springer, 1990. URL: https://doi.org/10.1007/BFB0023750.
  12. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Trans. Software Eng., 35(2):258-273, 2009. URL: https://doi.org/10.1109/TSE.2008.106.
  13. Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate analysis of probabilistic processes: Logic, simulation and games. In Quantitative Evaluation of Systems, QEST 2008, pages 264-273. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/QEST.2008.42.
  14. Josée Desharnais and Ana Sokolova. ε-distance via Lévy-Prokhorov lifting. In Stefano Guerrini and Barbara König, editors, Computer Science Logic, CSL 2026, volume 363 of LIPIcs, pages 26:1-26:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. URL: https://doi.org/10.4230/LIPIcs.CSL.2026.26.
  15. Gianluca Dini, Fabio Martinelli, Ilaria Matteucci, Andrea Saracino, and Daniele Sgandurra. Introducing probabilities in contract-based approaches for mobile application security. In Joaquín García-Alfaro, Georgios V. Lioudakis, Nora Cuppens-Boulahia, Simon N. Foley, and William M. Fitzgerald, editors, Data Privacy Management and Autonomous Spontaneous Security, DPM-SETOP 2013, volume 8247 of LNCS, pages 284-299. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-54568-9_18.
  16. Uli Fahrenberg and Axel Legay. The quantitative linear-time-branching-time spectrum. Theor. Comput. Sci., 538:54-69, 2014. URL: https://doi.org/10.1016/J.TCS.2013.07.030.
  17. Santiago Figueira and Daniel Gorín. On the size of shortest modal descriptions. In Lev D. Beklemishev, Valentin Goranko, and Valentin B. Shehtman, editors, Advances in Modal Logic, AiML 2010, pages 120-139. College Publications, 2010. URL: http://www.aiml.net/volumes/volume8/Figueira-Gorin.pdf.
  18. Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantitative Hennessy-Milner theorems via notions of density. In Bartek Klin and Elaine Pimentel, editors, Computer Science Logic, CSL 2023, volume 252 of LIPIcs, pages 22:1-22:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.22.
  19. Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Quantitative graded semantics and spectra of behavioural metrics. In Computer Science Logic, CSL 2025, volume 326 of LIPIcs, pages 33:1-33:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CSL.2025.33.
  20. Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, and Pedro Nora. Computing distinguishing formulae for threshold-based behavioural distances. CoRR, abs/2602.12084, 2026. URL: https://doi.org/10.48550/arXiv.2602.12084.
  21. Stefan Gebhart, Lutz Schröder, and Paul Wild. Non-expansive fuzzy ALC. In International Joint Conference on Artificial Intelligence, IJCAI 2025, pages 4509-4517. ijcai.org, 2025. URL: https://doi.org/10.24963/IJCAI.2025/502.
  22. Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods, pages 443-458. North-Holland, 1990. Google Scholar
  23. Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of LNCS, pages 253-266. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40206-7_19.
  24. Daniel Hausmann and Lutz Schröder. Game-based local model checking for the coalgebraic mu-calculus. In Wan J. Fokkink and Rob van Glabbeek, editors, Concurrency Theory, CONCUR 2019, LIPIcs, pages 35:1-35:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.35.
  25. Bartek Klin. Structural operational semantics for weighted transition systems. In Jens Palsberg, editor, Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, LNCS, pages 121-139. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04164-8_7.
  26. Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, and Ichiro Hasuo. Codensity games for bisimilarity. In Logic in Computer Science, LICS 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785691.
  27. Barbara König and Christina Mika-Michalski. (Metric) bisimulation games and real-valued modal logics for coalgebras. In Sven Schewe and Lijun Zhang, editors, Concurrency Theory, CONCUR 2018, 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.
  28. 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, Coalgebraic Methods in Computer Science, CMCS 2020, volume 12094 of LNCS, pages 133-154. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-57201-3_8.
  29. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  30. Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, FOSSACS 2011, volume 6604 of LNCS, pages 27-41. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_3.
  31. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci., 81(5):880-900, 2015. URL: https://doi.org/10.1016/J.JCSS.2014.12.006.
  32. Pedro Nora, Jurriaan Rot, Lutz Schröder, and Paul Wild. Relational connectors and heterogeneous simulations. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2025, volume 15691 of LNCS, pages 111-132. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90897-2_6.
  33. Amgad Rady and Franck van Breugel. Explainability of probabilistic bisimilarity distances for labelled Markov chains. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2023, volume 13992 of LNCS, pages 285-307. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_14.
  34. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  35. Lutz Schröder and Dirk Pattinson. Description logics and fuzzy probability. In Toby Walsh, editor, International Joint Conference on Artificial Intelligence, IJCAI 2011, pages 1075-1081. IJCAI/AAAI, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-184.
  36. Umberto Straccia. A fuzzy description logic. In Jack Mostow and Chuck Rich, editors, Artificial Intelligence/ Innovative Applications of Artificial Intelligence, AAAI 1998, IAAI 1998, pages 594-599. AAAI Press / The MIT Press, 1998. URL: http://www.aaai.org/Library/AAAI/1998/aaai98-084.php.
  37. Michio Sugeno. Theory of fuzzy integrals and its applications. PhD thesis, Tokyo Institute of Technology, 1974. Google Scholar
  38. Albert Thijs. Simulation and fixpoint semantics. PhD thesis, University of Groningen, 1996. Google Scholar
  39. 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.
  40. Paul Wild and Lutz Schröder. A quantified coalgebraic van Benthem theorem. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, FOSSACS 2021, volume 12650 of LNCS, pages 551-571. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_28.
  41. Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:19)2022.
  42. Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König. A van Benthem theorem for fuzzy modal logic. In Anuj Dawar and Erich Grädel, editors, Logic in Computer Science, LICS 2018, pages 909-918. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209180.
  43. Paul Wild, Lutz Schröder, Karla Messing, Barbara König, and Jonas Forster. Generalized Kantorovich-Rubinstein duality beyond Hausdorff and Kantorovich. In Natalie Betrand and Stefan Milius, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2026, LNCS, pages 636-657. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22730-0_30.
  44. Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Explaining behavioural inequivalence generically in quasilinear time. In Serge Haddad and Daniele Varacca, editors, Concurrency Theory, CONCUR 2021, LIPIcs, pages 32:1-32:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.32.
  45. 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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact