Quantitative Hennessy-Milner Theorems via Notions of Density

Forster J, Goncharov S, Hofmann D, Nora P, Schröder L, Wild P (2023)

Publication Type: Conference contribution

Publication year: 2023

Journal

Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

Book Volume: 252

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Warsaw

ISBN: 9783959772648

DOI: 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.

Authors with CRIS profile

Involved external institutions

Center for Research & Development in Mathematics and Applications / Centro de Investigação e Desenvolvimento em Matemática e Aplicações (CIDMA) Portugal (PT)

How to cite

APA:

Forster, J., Goncharov, S., Hofmann, D., Nora, P., Schröder, L., & Wild, P. (2023). Quantitative Hennessy-Milner Theorems via Notions of Density. In Bartek Klin, Elaine Pimentel (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Warsaw, PL: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Forster, Jonas, et al. "Quantitative Hennessy-Milner Theorems via Notions of Density." Proceedings of the 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, Warsaw Ed. Bartek Klin, Elaine Pimentel, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2023.

BibTeX: Download