Quantitative Graded Semantics and Spectra of Behavioural Metrics

Forster J, Schröder L, Wild P, Beohar H, Gurke S, König B, Messing K (2025)

Publication Type: Conference contribution

Publication year: 2025

Journal

LIPIcs : Leibniz International Proceedings in Informatics Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik

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

Book Volume: 326

Conference Proceedings Title: Leibniz International Proceedings in Informatics, LIPIcs

Event location: Amsterdam NL

ISBN: 9783959773621

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

Authors with CRIS profile

Jonas Forster Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik) Paul Wild Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

University of Sheffield GB United Kingdom (GB) Universität Duisburg-Essen (UDE) DE Germany (DE)

How to cite

APA:

Forster, J., Schröder, L., Wild, P., Beohar, H., Gurke, S., König, B., & Messing, K. (2025). Quantitative Graded Semantics and Spectra of Behavioural Metrics. In Jorg Endrullis, Sylvain Schmitz (Eds.), Leibniz International Proceedings in Informatics, LIPIcs. Amsterdam, NL: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.

MLA:

Forster, Jonas, et al. "Quantitative Graded Semantics and Spectra of Behavioural Metrics." Proceedings of the 33rd EACSL Annual Conference on Computer Science Logic, CSL 2025, Amsterdam Ed. Jorg Endrullis, Sylvain Schmitz, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2025.

BibTeX: Download