Wild P, Schröder L (2020)
Publication Type: Conference contribution, Original article
Publication year: 2020
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Book Volume: 171
Pages Range: 271-2723
Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs
ISBN: 9783959771603
DOI: 10.4230/LIPIcs.CONCUR.2020.27
Open Access Link: https://doi.org/10.4230/LIPIcs.CONCUR.2020.27
Behavioural distances provide a fine-grained measure of equivalence in systems involving quantitative data, such as probabilistic, fuzzy, or metric systems. Like in the classical setting of crisp bisimulation-type equivalences, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this kind are emerging within the paradigm of universal coalgebra, based either on lifting pseudometrics along set functors or on lifting general real-valued (fuzzy) relations along functors by means of fuzzy lax extensions. An immediate benefit of the latter is that they allow bounding behavioural distance by means of fuzzy bisimulations that need not themselves be (pseudo-)metrics, in analogy to classical bisimulations (which need not be equivalence relations). The known instances of generic pseudometric liftings, specifically the generic Kantorovich and Wasserstein liftings, both can be extended to yield fuzzy lax extensions, using the fact that both are effectively given by a choice of quantitative modalities. Our central result then shows that in fact all fuzzy lax extensions are Kantorovich extensions for a suitable set of quantitative modalities, the so-called Moss modalities. For non-expansive fuzzy lax extensions, this allows for the extraction of quantitative modal logics that characterize behavioural distance, i.e. satisfy a quantitative version of the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a quantitative version of Moss' coalgebraic logic.
APA:
Wild, P., & Schröder, L. (2020). Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov, Laura Kovacs (Eds.), Leibniz International Proceedings in Informatics, LIPIcs (pp. 271-2723). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
Wild, Paul, and Lutz Schröder. "Characteristic logics for behavioural metrics via fuzzy lax extensions." Proceedings of the 31st International Conference on Concurrency Theory, CONCUR 2020 Ed. Igor Konnov, Laura Kovacs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2020. 271-2723.
BibTeX: Download