Document

# Quantitative Hennessy-Milner Theorems via Notions of Density

## File

LIPIcs.CSL.2023.22.pdf
• Filesize: 0.79 MB
• 20 pages

## Cite As

Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantitative Hennessy-Milner Theorems via Notions of Density. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.22

## Abstract

The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on behavioural distance (e.g. in weighted, metric, or probabilistic transition systems) are witnessed by quantitative modal formulas. Both the qualitative and the quantitative versions have been accommodated within the framework of coalgebraic logic, with distances taking values in quantales, subject to certain restrictions, such as being so-called value quantales. While previous quantitative coalgebraic Hennessy-Milner theorems apply only to liftings of set functors to (pseudo)metric spaces, in the present work we provide a quantitative coalgebraic Hennessy-Milner theorem that applies more widely to functors native to metric spaces; notably, we thus cover, for the first time, the well-known Hennessy-Milner theorem for continuous probabilistic transition systems, where transitions are given by Borel measures on metric spaces, as an instance of such a general result. In the process, we also relax the restrictions imposed on the quantale, and additionally parametrize the technical account over notions of closure and, hence, density, providing associated variants of the Stone-Weierstraß theorem; this allows us to cover, for instance, behavioural ultrametrics.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Modal and temporal logics
• Theory of computation → Concurrency
##### Keywords
• Behavioural distances
• coalgebra
• characteristic modal logics
• density
• Hennessy-Milner theorems
• quantale-enriched categories
• Stone-Weierstraß theorems

## Metrics

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

## References

1. 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.
2. Jirí Adámek, Stefan Milius, Lawrence S. Moss, and Henning Urbat. On finitary functors and their presentations. J. Comput. Syst. Sci., 81(5):813-833, 2015. URL: https://doi.org/10.1016/j.jcss.2014.12.002.
3. Ki Yung Ahn, Ross Horne, and Alwen Tiu. A characterisation of open bisimilarity using an intuitionistic modal logic. In Roland Meyer and Uwe Nestmann, editors, Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pages 7:1-7:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.7.
4. Claudi Alsina, Maurice J. Frank, and Berthold Schweizer. Associative functions. Triangular norms and copulas. World Scientific, 2006. URL: https://doi.org/10.1142/9789812774200.
5. Steve Awodey. Category Theory. Oxford University Press, 2nd edition, 2010.
6. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3):1860-5974, 2018. URL: https://doi.org/10.23638/lmcs-14(3:20)2018.
7. 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. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. This volume.
8. Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jirí Srba. Infinite runs in weighted timed automata with energy constraints. In Franck Cassez and Claude Jard, editors, Formal Modeling and Analysis of Timed Systems, FORMATS 2008, volume 5215 of LNCS, pages 33-47. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85778-5_4.
9. Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema. Modal logics are coalgebraic. Comput. J., 54(1):31-41, 2011. URL: https://doi.org/10.1093/comjnl/bxp004.
10. 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.
11. 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.
12. 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.
13. 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.
14. Robert Flagg. Quantales and continuity spaces. Algebra Univ., 37(3):257-276, 1997.
15. 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.
16. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Kantorovich functors and characteristic logics for behavioural distances, 2022. URL: https://doi.org/10.48550/arXiv.2202.07069.
17. Helle Hvid Hansen, Clemens Kupke, and Eric Pacuit. Neighbourhood structures: Bisimilarity and basic model theory. Log. Methods Comput. Sci., 5(2), 2009. URL: https://doi.org/10.2168/LMCS-5(2:2)2009.
18. 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.
19. Dirk Hofmann and Walter Tholen. Lawvere completion and separation via closure. Applied Categorical Structures, 18(3):259-287, November 2010. URL: https://doi.org/10.1007/s10485-008-9169-9.
20. 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, volume 5700 of LNCS, pages 121-139. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04164-8_7.
21. 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.
22. 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.
23. 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.
24. 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.
25. F. William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del Seminario Matemàtico e Fisico di Milano, 43(1):135-166, 1973. Republished in: Reprints in Theory and Applications of Categories, No. 1 (2002), 1-37. URL: https://doi.org/10.1007/bf02924844.
26. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. System Sci., 81(5):880-900, 2015. URL: https://doi.org/10.1016/j.jcss.2014.12.006.
27. Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame Journal of Formal Logic, 45(1):19-33, 2004. URL: https://doi.org/10.1305/ndjfl/1094155277.
28. Umberto Rivieccio, Achim Jung, and Ramon Jansana. Four-valued modal logic: Kripke semantics and duality. J. Log. Comput., 27(1):155-199, 2017. URL: https://doi.org/10.1093/logcom/exv038.
29. J. Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
30. 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.
31. Franck van Breugel. A behavioural pseudometric for metric labelled transition systems. In Martín Abadi and Luca de Alfaro, editors, Concurrency Theory, CONCUR 2005, volume 3653 of LNCS, pages 141-155. Springer, 2005. URL: https://doi.org/10.1007/11539452_14.
32. 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.
33. 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.
34. 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.
35. 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.
36. 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.
X

Feedback for Dagstuhl Publishing