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 classical linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics come in various degrees of granularity, depending on the observer's ability to interact with the system. Graded monads have been shown to provide a unifying framework for spectra of behavioural equivalences. Here, we transfer this principle to spectra of behavioural metrics, working at a coalgebraic level of generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we discuss presentations of graded monads on the category of metric spaces in terms of graded quantitative equational theories. 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 the respective behavioural distance. We thus recover recent expressiveness results for coalgebraic branching-time metrics and for trace distance in metric transition systems; moreover, we obtain a new expressiveness result for trace semantics of fuzzy transition systems. We also provide a number of salient negative results. In particular, we show that trace distance on probabilistic metric transition systems does not admit a characteristic real-valued modal logic at all.

翻译：行为度量提供了对具有定量数据的系统（如度量或概率转移系统）中经典二值行为等价性的定量精细化。类似于转移系统上二值行为等价性的经典线性时间/分支时间谱系，行为度量根据观察者与系统交互的能力呈现出不同粒度的层级。已有研究表明，分级单子可为行为等价性谱系提供统一框架。在此，我们将这一原理推广至行为度量谱系，并在余代数层面（即参数化于系统类型）的通用性下开展工作。在后续定量分级语义的构建过程中，我们探讨了度量空间范畴上分级单子基于分级定量方程理论的表示方法。此外，我们获得了规范的一般性不变实值模态逻辑概念，并给出了此类逻辑在“逻辑距离与对应行为距离一致”意义上具有表达性的判据。由此，我们不仅重构了余代数分支时间度量与度量转移系统迹距离的近期表达性结果，还获得了模糊转移系统迹语义的新表达性结果。同时，我们提供了一系列显著的否定性结论：特别地，我们证明了概率度量转移系统上的迹距离完全不具有特征性实值模态逻辑。