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.

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