Quantitative Graded Semantics and Spectra of Behavioural Metrics
Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing
TL;DR
This work addresses how to quantify and reason about behavioural distances in coalgebraic systems with quantitative data. It proves a no-go for unary modal logics to characterize probabilistic metric trace distance, motivating a graded-semantic approach based on graded monads over metric spaces. The authors develop graded quantitative theories and logics, provide expressivity criteria, and instantiate the framework to obtain expressive logics for metric trace semantics and, notably, a new characteristic logic for fuzzy metric trace semantics. The results unify linear-time/branching-time spectra in a coalgebraic setting and point to future directions such as game-based characterizations and algorithmic generation of distinguishing formulae.
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.