Quantitative Graded Semantics and Spectra of Behavioural Metrics

Authors Jonas Forster , Lutz Schröder , Paul Wild , Harsh Beohar , Sebastian Gurke , Barbara König , Karla Messing



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.33.pdf
  • Filesize: 0.84 MB
  • 21 pages

Document Identifiers

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
Harsh Beohar
  • University of Sheffield, UK
Sebastian Gurke
  • Universität Duisburg-Essen, Germany
Barbara König
  • Universität Duisburg-Essen, Germany
Karla Messing
  • Universität Duisburg-Essen, Germany

Cite As Get BibTex

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 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.33

Abstract

Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/ branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • transition systems
  • modal logics
  • coalgebras
  • behavioural metrics

Metrics

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

References

  1. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories. John Wiley and Sons, 1990. Reprint: URL: http://www.tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
  2. 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.
  3. Radim Belohlávek. Determinism and fuzzy automata. Inf. Sci., 143(1-4):205-209, 2002. URL: https://doi.org/10.1016/S0020-0255(02)00192-5.
  4. 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, volume 252 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.12.
  5. Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive quantale-valued logics for coalgebras: An adjunction-based approach. In Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov, editors, Theoretical Aspects of Computer Science, STACS 2024, volume 289 of LIPIcs, pages 10:1-10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.STACS.2024.10.
  6. Marco Bernardo and Stefania Botta. A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems. Math. Struct. Comput. Sci., 18(1):29-55, 2008. URL: https://doi.org/10.1017/S0960129507006408.
  7. Valentina Castiglioni, Konstantinos Chatzikokolakis, and Catuscia Palamidessi. A logical characterization of differential privacy via behavioral metrics. In Kyungmin Bae and Peter Ölveczky, editors, Formal Aspects of Component Software, FACS 2018, volume 11222 of LNCS, pages 75-96. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02146-7.
  8. Valentina Castiglioni, Daniel Gebler, and Simone Tini. Logical characterization of bisimulation metrics. In Mirco Tribastone and Herbert Wiklicky, editors, Quantitative Aspects of Programming Languages and Systems, QAPL 2016, volume 227 of EPTCS, pages 44-62, 2016. URL: https://doi.org/10.4204/EPTCS.227.
  9. Ivan Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Jos C. M. Baeten and Jan Willem Klop, editors, Theories of Concurrency: Unification and Extension, CONCUR 1990, volume 458 of LNCS, pages 126-140. Springer, 1990. URL: https://doi.org/10.1007/BFb0039056.
  10. 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.
  11. 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.
  12. Liliana D'Errico and Michele Loreti. Modeling fuzzy behaviours in concurrent systems. In Giuseppe F. Italiano, Eugenio Moggi, and Luigi Laura, editors, Theoretical Computer Science, 10th Italian Conference, ICTCS 2007, pages 94-105. World Scientific, 2007. URL: https://doi.org/10.1142/9789812770998_0012.
  13. 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.
  14. Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded monads and graded logics for the linear time - branching time spectrum. In Wan J. Fokkink and Rob van Glabbeek, editors, Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 36:1-36:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.36.
  15. 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.
  16. Uli Fahrenberg, Axel Legay, and Claus Thrane. The quantitative linear-time-branching-time spectrum. In Supratik Chakraborty and Amit Kumar, editors, Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, volume 13 of LIPIcs, pages 103-114. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.103.
  17. Ihor Filimonov, Ross Horne, Sjouke Mauw, and Zach Smith. Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity. In Kazue Sako, Steve A. Schneider, and Peter Y. A. Ryan, editors, Computer Security, ESORICS 2019, volume 11735 of LNCS, pages 577-594. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29959-0_28.
  18. Melvin Fitting. Many-valued modal logics. Fund. Inform., 15:235-254, 1991. URL: https://doi.org/10.3233/FI-1991-153-404.
  19. Chase Ford, Stefan Milius, and Lutz Schröder. Behavioural preorders via graded monads. In Logic in Computer Science, LICS 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470517.
  20. Chase Ford, Stefan Milius, and Lutz Schröder. Monads on categories of relational structures. In Fabio Gadducci and Alexandra Silva, editors, Algebra and Coalgebra in Computer Science, CALCO 2021, volume 211 of LIPIcs, pages 14:1-14:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.14.
  21. Chase Ford, Stefan Milius, Lutz Schröder, Harsh Beohar, and Barbara König. Graded monads and behavioural equivalence games. In Christel Baier and Dana Fisman, editors, Logic in Computer Science, LICS 2022, pages 61:1-61:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533374.
  22. 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.
  23. Jonas Forster, Lutz Schröder, and Paul Wild. Quantitative graded semantics and spectra of behavioural metrics. CoRR, abs/2306.01487, 2023. URL: https://doi.org/10.48550/arXiv.2306.01487.
  24. Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, and Karla Messing. Graded semantics and graded logics for Eilenberg-Moore coalgebras. In Barbara König and Henning Urbat, editors, Coalgebraic Methods in Computer Science, CMCS 2024, volume 14617 of LNCS, pages 114-134. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-66438-0_6.
  25. Alessandro Giacalone, Chi-Chang Jou, and Scott Smolka. Algebraic reasoning for probabilistic concurrent systems. In Manfred Broy, editor, Programming concepts and methods, PCM 1990, pages 443-458. North-Holland, 1990. Google Scholar
  26. 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, FoSSaCS 2023, volume 13992 of LNCS, pages 46-67. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_3.
  27. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Methods Comput. Sci., 3(4), 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  28. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  29. 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.
  30. Manisha Jain, Alexandre Madeira, and Manuel A. Martins. A fuzzy modal logic for fuzzy transition systems. In Amy P. Felty and João Marcos, editors, Logical and Semantic Frameworks with Applications, LSFA 2019, volume 348 of ENTCS, pages 85-103. Elsevier, 2019. URL: https://doi.org/10.1016/j.entcs.2020.02.006.
  31. Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. Log. Methods Comput. Sci., 12(4), 2016. URL: https://doi.org/10.2168/LMCS-12(4:10)2016.
  32. Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo. Expressivity of quantitative modal logics : Categorical foundations via codensity and approximation. In Logic in Computer Science, LICS 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470656.
  33. 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.
  34. Clemens Kupke and Jurriaan Rot. Expressive logics for coinductive predicates. Log. Methods Comput. Sci., 17(4), 2021. URL: https://doi.org/10.46298/lmcs-17(4:19)2021.
  35. F. E. J. Linton. Some aspects of equational categories. In S. Eilenberg, D. K. Harrison, S. MacLane, and H. Röhrl, editors, Proceedings of the Conference on Categorical Algebra, pages 84-94. Springer, 1966. URL: https://doi.org/10.1007/978-3-642-99902-4_3.
  36. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Logic in Computer Science, LICS 2016, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  37. Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. In Lawrence S. Moss and Pawel Sobocinski, editors, Algebra and Coalgebra in Computer Science, CALCO 2015, volume 35 of LIPIcs, pages 253-269. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CALCO.2015.253.
  38. Haiyu Pan, Yongming Li, Yongzhi Cao, and Zhanyou Ma. Model checking computation tree logic over finite lattices. Theor. Comput. Sci., 612:45-62, 2016. URL: https://doi.org/10.1016/j.tcs.2015.10.014.
  39. Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19-33, 2004. URL: https://doi.org/10.1305/NDJFL/1094155277.
  40. 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.
  41. Jurriaan Rot, Bart Jacobs, and Paul Blain Levy. Steps and traces. J. Log. Comput., 31(6):1482-1525, 2021. URL: https://doi.org/10.1093/logcom/exab050.
  42. Jan J. M. M. Rutten. Relators and metric bisimulations. In Bart Jacobs, Larry Moss, Horst Reichel, and Jan J. M. M. Rutten, editors, Coalgebraic Methods in Computer Science, CMCS 1998, volume 11 of ENTCS, pages 252-258. Elsevier, 1998. URL: https://doi.org/10.1016/S1571-0661(04)00063-5.
  43. 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.
  44. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390(2-3):230-247, 2008. URL: https://doi.org/10.1016/j.tcs.2007.09.023.
  45. 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.
  46. 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.
  47. Rob J. van Glabbeek. The linear time - branching time spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3-99. North-Holland/Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50019-9.
  48. Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov and Laura Kovács, editors, Concurrency Theory, CONCUR 2020, volume 171 of LIPIcs, pages 27:1-27:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.27.
  49. 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.
  50. 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.
  51. 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.
  52. 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, volume 203 of LIPIcs, pages 32:1-32:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.32.
  53. James Worrell. Coinduction for recursive data types: partial orders, metric spaces and omega-categories. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 337-356. Elsevier, 2000. URL: https://doi.org/10.1016/S1571-0661(05)80356-1.
  54. Hengyang Wu, Taolue Chen, Tingting Han, and Yixiang Chen. Bisimulations for fuzzy transition systems revisited. Int. J. Approx. Reason., 99:1-11, 2018. URL: https://doi.org/10.1016/j.ijar.2018.04.010.
  55. Hengyang Wu, Yixiang Chen, Tian-Ming Bu, and Yuxin Deng. Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems. Fuzzy Sets Syst., 333:106-123, 2018. URL: https://doi.org/10.1016/j.fss.2017.02.008.
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