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. We 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 obtain a canonical generic notion of invariant real-valued modal logic, and provide criteria for such logics to be expressive in the sense that logical distance coincides with behavioural distance. We present positive examples based on this criterion, covering both known and new expressiveness results; in particular, we show that expressiveness holds essentially always for Eilenberg-Moore type trace semantics, and we obtain a new expressiveness result for trace semantics of fuzzy transition systems. As a negative result, we show that trace distance on probabilistic metric transition systems does not admit any characteristic real-valued modal logic, even in a more broadly understood sense.

翻译：行为度量提供了对具有定量数据（如度量或概率转移系统）的系统上经典二值行为等价的定量精化。类似于转移系统上二值行为等价的线性时间/分支时间谱系，行为度量的粒度也有所不同。我们在分级单子的新兴框架下，以余代数的一般性（即参数化于系统类型）对行为度量的谱系进行了统一处理。在定量分级语义的后续发展中，我们引入了度量空间范畴上分级单子的代数表示。此外，我们获得了一个规范的不变实值模态逻辑的通用概念，并提供了此类逻辑在逻辑距离与行为距离一致意义上具有表达性的判据。基于此判据，我们给出了正面示例，涵盖了已知和新的表达性结果；特别地，我们证明了表达性对艾伦伯格-摩尔型迹语义基本总是成立，并获得了模糊转移系统迹语义的一个新表达性结果。作为负面结果，我们证明了概率度量转移系统上的迹距离不承认任何特征实值模态逻辑，即使在更广义的理解下也是如此。