Quantitative Graded Semantics and Spectra of Behavioural Metrics

Forster, Jonas; Schröder, Lutz; Wild, Paul; Beohar, Harsh; Gurke, Sebastian; König, Barbara; Messing, Karla

doi:10.4230/LIPIcs.CSL.2025.33

Quantitative Graded Semantics and
Spectra of Behavioural Metrics

Jonas Forster

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany Lutz Schröder

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany Paul Wild

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany Harsh Beohar

University of Sheffield, UK Sebastian Gurke

Universität Duisburg-Essen, Germany Barbara König

Universität Duisburg-Essen, Germany Karla Messing

Universität Duisburg-Essen, Germany

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.

Keywords and phrases:

transition systems, modal logics, coalgebras, behavioural metrics

Copyright and License:

© Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and
Karla Messing; licensed under Creative Commons License CC-BY 4.0

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Modal and temporal logics

Related Version:

Full Version: https://arxiv.org/abs/2306.01487 [23]

Funding:

The fourth author was supported by the EPSRC NIA Grant EP/X019373/1, while the remaining authors were supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 434050016 (SpeQt).

DOI:

10.4230/LIPIcs.CSL.2025.33

Event:

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Editors:

Jörg Endrullis and Sylvain Schmitz

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

While qualitative models of concurrent systems are traditionally analysed using various notions of two-valued process equivalence, it has long been recognized that for systems involving quantitative data, notions of behavioural distance play a useful role as a more fine-grained measure of process similarity. Well-known examples include behavioural distances on probabilistic transition systems [25, 13, 46], on systems combining nondeterminism and probability [8], and on metric transition systems [11, 16]. Like in the two-valued case, where process equivalences of varying granularity are arranged on the linear-time/branching-time spectrum [47], one has a spectrum of behavioural metrics on a given system type that vary in granularity (with greater distances thought of as having finer granularity) [15].

An important point of interest in this context are characteristic modal logics. In the two-valued setting, a logic is characteristic for a given behavioural equivalence if the latter coincides with the respective induced logical indistinguishability relation, so that behavioural inequivalence can be certified by distinguishing formulae (as in the recent proof of the failure of unlinkability in the ICAO 9303 e-passport standard [17])). For instance, Hennessy-Milner logic is characteristic for bisimilarity [28], and most equivalences on the classical spectrum are characterized by fragments of Hennessy-Milner logic [47] that are compositionally defined, i.e. given by a choice of modalities and propositional operators equipped with a recursively defined semantics (e.g. trace equivalence is characterized by the logic built from diamonds, truth, and – optionally – disjunction). In the quantitative setting, a logic is characteristic if the induced logical distance coincides with the respective behavioural distance, so that high behavioural distance may be certified by means of distinguishing modal formulae [40]. A prototypical example is quantitative probabilistic modal logic, which is characteristic for branching-time behavioural distance on probabilistic transition systems [46]. However, it turns out that in general, the quantitative setting behaves less smoothly in this respect than the two-valued setting. Indeed, we show as our first main result that for probabilistic metric trace distance (on generative probabilistic transition systems in which the set of labels is equipped with a metric, i.e. on the probabilistic variant of metric transition systems), there does not exist any characteristic quantitative modal logic at all. Here, the term modal logic is understood in a fairly broad sense; essentially, we stipulate no more than that, in analogy to the two-valued case as discussed above, the logic should be a compositionally defined fragment of a bisimulation-invariant next-step logic with unary modalities.

We subsequently work towards positive results, using the framework of graded semantics [37, 14] to achieve an appropriate level of generality. Graded semantics is parametric both in the type of systems (e.g. probabilistic, metric, fuzzy) and in the quantitative semantics of systems, i.e. the choice of behavioural distance. The system type is abstracted as an endofunctor on a suitable base category following the paradigm of universal coalgebra [43]. Parametricity in the system semantics, on the other hand, is based on the choice of a graded monad, which handles additional semantic identifications (beyond branching-time equivalence) by algebraic means, using grades to control the depth of look-ahead. Both Kleisli-style coalgebraic trace semantics [27] and the smoother, but less widely applicable Eilenberg-Moore-style coalgebraic trace semantics [29] are subsumed by this framework [37].

Graded semantics has recently been extended to cover behavioural distances in the Eilenberg-Moore-style setting [5, 24], and, generalizing the two-valued case [37, 14], a canonical notion of quantitative graded logic has been identified. Quantitative graded logics are always invariant under the underlying behavioural distance in the sense that formula evaluation is nonexpansive, so that logical distance is below behavioural distance. In some cases, the reverse inequality, i.e. expressivity of quantitative graded logics, can be established by a straightforward generalization of corresponding criteria for the two-valued case. Notably, one can show that in the Eilenberg-Moore setting, one essentially always has a characteristic modal logic [24], in sharp contrast to our present negative result. The flip side of the coin is that Eilenberg-Moore style trace semantics applies to only rather few system types (essentially automata with effects), and in particular does not support a metric on the labels as found, for instance, in standard metric transition systems.

Our second, now positive, contribution in the present work is to extend the framework to unrestricted graded semantics, notably including Kleisli-style coalgebraic trace semantics and, hence, trace semantics on systems with labels taken from a metric space. For the syntactic treatment of spectra of behavioural distances in this sense, we introduce a graded extension of quantitative algebra [36] that allows describing graded monads on the category of metric spaces by operations and approximate equations. As suggested by our negative result, establishing expressivity of graded logics in the general case presents additional challenges compared to the two-valued variant and the Eilenberg-Moore case. In particular, it turns out that the expressivity criterion needs to be parametric in a strengthening of the inductive hypothesis in the induction on depth of look-ahead that it encapsulates; indeed, this happens already in strikingly simple cases such as metric streams. We develop a number of example applications: We recover results on expressivity of quantitative modal logics for (finite-depth) branching-time distances [33, 48, 19, 32], as well as a recent result on expressivity of a quantitative modal logic for trace distance in metric transition systems [4], which in fact we generalize to systems with metric state space and closed branching. In a concluding case study, we moreover identify a new characteristic modal logic for trace distance on fuzzy metric transition systems, which turns out to require next-step modalities incorporating a constant shift on label distances.

Omitted proofs and additional details can be found in the full version [23].

Related Work.

We have mentioned previous work on coalgebraic branching-time behavioural distances [2, 33, 22, 49, 50, 4, 32] and on graded semantics for two-valued behavioural equivalences and preorders [37, 14, 19]. Kupke and Rot [34] study logics for coinductive predicates, which generalize branching-time behavioural distances. Generally, our overall setup differs from the one used in [34] and elsewhere by working with coalgebras that already live on metric spaces (e.g. [42, 53, 46, 22, 26]); this allows covering functors on metric spaces that are not liftings of set functors, such as the full Hausdorff functor (which takes closed subsets). Recent work on Galois connections for logical distances [4, 5] is highly general (and in fact not even tied to state-based systems) but leaves more work to the instantiation than the framework of graded monads. Moreover, it is aimed primarily at fixpoint characterizations of logical distance, and in fact induces behavioural distance from the logic, while we aim to provide logical characterizations of given behavioural distances. Alternative coalgebraic approaches to process equivalences coarser than branching time include coalgebraic trace semantics in Kleisli [27] and Eilenberg-Moore categories [29], which are both subsumed by the paradigm of graded monads [37], as well as an approach in which behavioural equivalences are defined via characteristic logics [31]. The Eilenberg-Moore and Kleisli setups can be unified using corecursive algebras, which also support, under certain assumptions, a logical characterization for these cases [41]. The Eilenberg-Moore approach has been applied to linear-time behavioural distances [2]. Recently, some of the present authors used the graded-semantics approach to Eilenberg-Moore semantics to extract characteristic logics that factor through the determinization of a coalgebra [24]. We make use of their notion of graded logic and complement their work by considering unrestricted graded semantics, in particular covering the more broadly applicable Kleisli-style semantics.

De Alfaro et al. [11] introduce a linear-time logic for (state-labelled) metric transition systems. The semantics of this logic is defined by first computing the set of paths of a system, so that propositional operators and modalities have a different meaning than in corresponding branching-time logics, while our graded logics are fragments of branching-time logics. Fahrenberg et al. [16] present a game-based approach to a spectrum of behavioural distances on metric transition systems. A two-valued logic for probabilistic trace semantics (for a discrete set of labels) has been considered in the context of differential privacy [7]. A notion of logical distance is then obtained via a real-valued semantics defined using a syntactic distance on formulae; this semantics is not compositional (truth values are defined by taking infima over the whole logical syntax), so subsequent results relating this logical distance to notions of weak anonymity do not contradict our impossibility result on (compositional) characteristic logics for probabilistic trace semantics.

2 Preliminaries

Basic familiarity with category theory is assumed (e.g. [1]). We write $\mathbf{Set}$ for the category of sets and maps. Below, we recall some background on (bounded) metric spaces and universal coalgebra.

Metric spaces.

The real unit interval $[0,1]$ will serve as the domain of distances and truth values. Under the usual ordering $\leq$ , $[0,1]$ forms a complete lattice; we write $\bigvee,\bigwedge$ for joins and meets in $[0,1]$ (e.g. $\bigvee_{i}x_{i}=\sup_{i}x_{i}$ ), and $\vee,\wedge$ for binary join and meet, respectively. We denote truncated addition and subtraction by $\oplus$ and $\ominus$ , respectively; that is, $x\oplus y=\min(x+y,1)$ and $x\ominus y=\max(x-y,0)$ . These operations form part of a structure of $[0,1]$ as a (co-)quantale; for readability, we refrain from working with more general quantales [49, 22].

Definition 2.1.

A (bounded) pseudometric space is a pair $(X,d)$ consisting of a set $X$ and a function $d\colon X\times X\to[0,1]$ satisfying the standard conditions of reflexivity ( $d(x,x)=0$ for all $x\in X$ ), symmetry ( $d(x,y)=d(y,x)$ for all $x,y\in X$ ), and the triangle inequality ( $d(x,z)\leq d(x,y)+d(y,z)$ for all $x,y,z\in X$ ); if additionally separation holds (for $x,y\in X$ , if $d(x,y)=0$ then $x=y$ ), then $(X,d)$ is a metric space. A function $f\colon X\to Y$ between pseudometric spaces $(X,d_{X})$ and $(Y,d_{Y})$ is nonexpansive if $d_{Y}(f(x),f(y))\leq d_{X}(x,y)$ for all $x,y\in X$ . Metric spaces and nonexpansive maps form a category $\mathbf{Met}$ .

We often do not distinguish notationally between a (pseudo-)metric space $(X,d)$ and its underlying set $X$ . Occasionally we use subscripts to make explicit the carrier to which a (pseudo-)metric is associated, i.e. $d_{X}$ is the (pseudo-)metric of the space with carrier $X$ . The categorical product $(X,d_{X})\times(Y,d_{Y})$ of (pseudo-)metric spaces equips the Cartesian product $X\times Y$ with the supremum (pseudo-)metric $d_{X\times Y}((a,b),(a^{\prime},b^{\prime}))=d_{X}(a,a^{\prime})\vee d_{Y}(b,b% ^{\prime})$ . Similarly, the Manhattan tensor $\boxplus$ equips $X\times Y$ with the Manhattan (pseudo-)metric $d_{X\boxplus Y}((a,b),(a^{\prime},b^{\prime}))=d_{X}(a,a^{\prime})\oplus d_{Y}% (b,b^{\prime})$ . We occasionally write elements of the product $X^{n+m}$ as $v w$ if $v\in X^{n}$ and $w\in X^{m}$ . Given (pseudo-)metric spaces $X, Y$ , the nonexpansive functions $X\to Y$ form a (pseudo-)metric space under the standard supremum distance.

Example 2.2.

We recall some key examples of functors on $\mathbf{Set}$ and $\mathbf{Met}$ .

1.

We write $\mathcal{P}_{\omega}$ for the finite powerset functor on $\mathbf{Set}$ , and $\overline{\mathcal{P}}_{\omega}$ for the lifting of $\mathcal{P}_{\omega}$ to $\mathbf{Met}$ given by the Hausdorff metric. Explicitly, for a metric space $(X,d)$ and $A,B\in\mathcal{P}_{\omega}X$ ,

$d_{\overline{\mathcal{P}}_{\omega}X}(A,B)=\textstyle(\bigvee_{\raisebox{1.0pt}% {$\scriptstyle a\in A$}}\bigwedge_{b\in B}d(a,b))\vee(\bigvee_{\raisebox{1.0pt% }{$\scriptstyle{b\in B}$}}\bigwedge_{\raisebox{1.0pt}{$\scriptstyle a\in A$}}d% (a,b)).$ (2.1)

Both $\mathcal{P}_{\omega}$ and $\overline{\mathcal{P}}_{\omega}$ are monads, with multiplication taking big unions.
2.

Related to the above, the closed Hausdorff monad $\mathcal{P}_{c}$ on $\mathbf{Met}$ sends a metric space $X$ to the set of closed subsets of $X$ , again equipped with the Hausdorff metric. For a nonexpansive function $f\colon X\to Y$ , $\mathcal{P}_{c}f$ sends $A\in\mathcal{P}_{c}X$ to the closure of $f[A]$ . Monad multiplication takes the closure of the big union.
3.

Similarly, $\mathcal{D}_{\omega}$ denotes the functor on $\mathbf{Set}$ that maps a set $X$ to the set of finitely supported probability distributions on $X$ , and $\overline{\mathcal{D}}_{\omega}$ denotes the lifting of $\mathcal{D}_{\omega}$ to $\mathbf{Met}$ that equips $\mathcal{D}_{\omega}X$ with the Kantorovich metric. Explicitly, for a metric space $(X,d)$ and $\mu,\nu\in\mathcal{D}_{\omega}X$ ,

$\textstyle d_{\overline{\mathcal{D}}_{\omega}X}(\mu,\nu)=\bigvee_{f}\sum_{x\in X% }f(x)(\mu(x)\ominus\nu(x))$

where $f$ ranges over all nonexpansive functions $X\to[0,1]$ . We often write elements of $\overline{\mathcal{D}}_{\omega}X$ as finite formal sums $\sum p_{i}\cdot x_{i}$ , with $x_{i}\in X$ and $\sum p_{i}=1$ .
4.

The finite fuzzy powerset functor $\mathcal{F}_{\omega}$ is given on sets $X$ by $\mathcal{F}_{\omega}X=\{A\colon X\to[0,1]\mid A(x)=0\text{ for almost all $x\in X$}\}$ , and on maps $f\colon X\to Y$ by $\mathcal{F}_{\omega}f(A)(y)=\bigvee\{A(x)\mid f(x)=y\}$ for $A\in\mathcal{F}_{\omega}X$ . That is, $\mathcal{F}_{\omega}X$ consists of the finite fuzzy subsets of $X$ , given by assigning membership degrees in $[0,1]$ to elements of $X$ , and $\mathcal{F}_{\omega}f$ acts by taking fuzzy direct images. We lift $\mathcal{F}_{\omega}$ to a functor $\overline{\mathcal{F}}_{\omega}$ on metric spaces that equips $\mathcal{F}_{\omega}X$ with the fuzzy Hausdorff distance [49, Example 5.3.1]. Explicitly, $d_{\overline{\mathcal{F}}_{\omega}X}(A,B)=d_{0}(A,B)\vee d_{0}(B,A)$ for a metric space $(X,d)$ and $A,B\in\mathcal{F}_{\omega}X$ , where

$\textstyle d_{0}(A,B)=\bigvee_{x}\bigwedge_{y}(A(x)\ominus B(y))\vee(A(x)% \wedge d(x,y)).$

Thus, $d_{0}(A,B)$ is analogous to the left-hand term in the binary join defining the Hausdorff metric (2.1): Both terms can be read intuitively as “ $B$ is far from $A$ if there is $x$ such that $x\in A$ and for all $y$ , if $y\in B$ then $y$ is far from $x$ ”, where $d_{0}(A,B)$ takes into account that the sets $A, B$ are fuzzy (in particular, the “if $y\in B$ ” is reflected in the contribution of $B(y)$ being negative).

Coalgebra.

Universal coalgebra [43] has established itself as a way to reason about state-based systems at an appropriate level of abstraction. It is based on encapsulating the transition type of systems as an endofunctor $G\colon\mathcal{C}\to\mathcal{C}$ on a base category $\mathcal{C}$ . Then, a $G$ -coalgebra $(X,\gamma)$ consists of a $\mathcal{C}$ -object $X$ , thought of as an object of states, and a morphism $\gamma\colon X\to GX$ , thought of as assigning to each state a collection of successors, structured according to $G$ . A $\mathcal{C}$ -morphism $h\colon X\to Y$ is a morphism of $G$ -coalgebras $(X,\gamma)\to(Y,\delta)$ if $Gh\cdot\gamma=\delta\cdot h$ .

For a functor $G\colon\mathbf{Met}\to\mathbf{Met}$ , one has a canonical notion of branching-time behavioural distance $d^{G}_{\gamma}$ on a $G$ -coalgebra $(X,\gamma)$ [22]. In case $G$ is a lifting of a set functor (which means roughly that the underlying set of $G X$ is independent of the metric on $X$ ), the general definition simplifies as follows: $d^{G}_{\gamma}$ is the least fixpoint of the map $d\mapsto d_{G(X,d)}\circ(\gamma\times\gamma)$ [2, 22].

Example 2.3.

Throughout the paper, we fix a metric space $\mathcal{A}$ of labels. Finitely branching metric transition systems with transition labels in $\mathcal{A}$ are coalgebras for the functor $\overline{\mathcal{P}}_{\omega}(\mathcal{A}\times{-})$ . (More precisely, a metric transition system is usually assumed to have a set as its state space, while $\overline{\mathcal{P}}_{\omega}(\mathcal{A}\times{-})$ -coalgebras more generally have a metric space of states, subsuming mere sets of states as discrete metric spaces). Similarly, coalgebras for the functor $\mathcal{P}_{c}(\mathcal{A}\times{-})$ are closed-branching metric transition systems, where sets of successors can be infinite but are required to be closed. With few exceptions (e.g. [22]), most coalgebraic approaches to behavioural metrics (e.g. [2, 33, 50, 34]) rely on the functor being a lifting of a $\mathbf{Set}$ -functor. We work with unrestricted functors on $\mathbf{Met}$ , thus, e.g., covering the above-mentioned functor $\mathcal{P}_{c}(\mathcal{A}\times{-})$ , which is not a lifting of a set functor. We use trace semantics on metric labelled transition systems (both finitely branching and closed-branching) as a running example of concepts as they appear throughout the text.

Quantitative Coalgebraic Modal Logic.

We proceed to introduce the requisite notion of quantitative coalgebraic modal logic [45, 33, 50, 24], in a formulation geared towards easing the extraction of invariant fragments for various semantics [24], and instantiated to the category of metric spaces. The notion of quantitative coalgebraic modal logic will also serve as the yardstick for our negative result on characteristic modal logics for probabilistic metric trace semantics (Section 3).

Syntactically, a modal logic is a triple $\mathcal{L}=(\Theta,\mathcal{O},\Lambda)$ where $\Theta$ is a set of truth constants, $\mathcal{O}$ is a set of propositional operators, each with associated finite arity, and $\Lambda$ is a set of modal operators, also each with an associated finite arity. For readability, we restrict to unary modal operators; extending our positive results to modal operators of higher arity is simply a matter of adding indices. The set of formulae of $\mathcal{L}$ is then given by the grammar

\phi::=c\mid p(\phi_{1},\ldots,\phi_{n})\mid L\phi\qquad\qquad(c\in\Theta,\;p% \in\mathcal{O}\text{ $n$-ary},\;L\in\Lambda).

Formulae are interpreted in $G$ -coalgebras for a given functor $G\colon\mathbf{Met}\to\mathbf{Met}$ , and take values in the truth value object $\Omega=[0,1]$ , which we equip with the standard metric $d_{\Omega}(x,y)=|x-y|$ . Moreover, the semantics is parametric in the following components:

$\blacksquare$

For every $c\in\Theta$ , a nonexpansive map $\hat{c}\colon 1\to\Omega$ .
$\blacksquare$

For $p\in\mathcal{O}$ with arity $n$ , a nonexpansive map $\llbracket p\rrbracket\colon\Omega^{n}\to\Omega$
$\blacksquare$

For $L\in\Lambda$ , a nonexpansive map $\llbracket L\rrbracket\colon G\Omega\to\Omega$

The evaluation of a formula $\phi$ on a $G$ -coalgebra $(X,\gamma)$ is then a nonexpansive map $\llbracket\phi\rrbracket_{\gamma}\colon X\to\Omega$ , inductively defined by

\begin{gathered}\llbracket c\rrbracket_{\gamma}=(X\xrightarrow{!}1\xrightarrow% {\hat{c}}\Omega)\qquad\qquad\llbracket p(\phi_{1},\ldots,\phi_{n})\rrbracket_{% \gamma}=(X\xrightarrow{\langle\llbracket\phi_{1}\rrbracket_{\gamma},\ldots,% \llbracket\phi_{n}\rrbracket_{\gamma}\rangle}\Omega^{n}\xrightarrow{\llbracket p% \rrbracket}\Omega)\\[5.0pt] \llbracket L\phi\rrbracket_{\gamma}=(X\xrightarrow{\gamma}GX\xrightarrow{G% \llbracket\phi\rrbracket_{\gamma}}G\Omega\xrightarrow{\llbracket L\rrbracket}% \Omega)\end{gathered}

Example 2.4.

We briefly exemplify the semantics of modalities: Take the functor $G=\overline{\mathcal{P}}_{\omega}(\mathcal{A}\times(-))$ modelling metric transition systems (2.3), and define the interpretation $\llbracket\Diamond_{a}\rrbracket\colon\overline{\mathcal{P}}_{\omega}(\mathcal% {A}\times\Omega)\to\Omega$ of modalities $\Diamond_{a}$ , for $a\in\mathcal{A}$ , by $\llbracket\Diamond_{a}\rrbracket(U)=\bigvee_{(b,v)\in U}(1-d(a,b))\land v$ . Then, roughly speaking, the degree to which a state in a metric transition system satisfies a formula $\Diamond_{a}\phi$ is the degree to which it has a $b$ -successor that satisfies $\phi$ , for some $b$ that is close to $a$ . (The use of $1-d(a,b)$ is owed to the usual discrepancy between $1$ representing “true” but also “far apart”.)

In the framework defined so far, truth constants are interchangeable with nullary propositional operators, but in the setting of graded logics (Section 6), the two concepts will play syntactically and semantically distinct roles. In particular, invariance w.r.t. a target semantics (Theorem 6.6) will in general hold only for formulae of uniform depth, that is, formulae in which all occurrences of truth constants are nested under the same number of modal operators. In cases where there are no truth constants, all formulae are uniform. We write $\mathcal{L}_{\mathsf{unif}}$ for the set of uniform-depth $\mathcal{L}$ -formulae.

Definition 2.5.

Logical distance under the logic $\mathcal{L}$ on a $G$ -coalgebra $(X,\gamma)$ is the pseudometric $d^{\mathcal{L}}$ given by $\textstyle d^{\mathcal{L}}(x,y)=\bigvee\{d_{\Omega}(\llbracket\phi\rrbracket_{% \gamma}(x),\llbracket\phi\rrbracket_{\gamma}(y))\mid\phi\in\mathcal{L}_{% \mathsf{unif}}\}$ .

Logical distance is always a lower bound for branching-time behavioural distance [33, 50, 22]; we discuss details in 7.10.

3 Probabilistic Metric Trace Semantics

Finitely branching probabilistic metric transition systems over a metric space of transition labels $\mathcal{A}$ are coalgebras for the functor ${G^{\mathsf{prob}}}=\overline{\mathcal{D}}_{\omega}(\mathcal{A}\boxplus(-))$ (cf. 2.2 and 2.3). The probabilistic (metric) trace semantics [9] of a probabilistic transition system calculates, at each depth $n$ , a distribution over length- $n$ traces. One then obtains a notion of depth- $n$ probabilistic trace distance $d_{n}^{\mathsf{ptrace}}$ , which takes Kantorovich distances of depth- $n$ trace distributions under the Manhattan distance on traces. Formal definitions are as follows.

Definition 3.1.

We write $\mathcal{A}^{\boxplus n}$ for the $n$ -fold Manhattan tensor $\mathcal{A}\boxplus\dots\boxplus\mathcal{A}$ . Let $(X,\gamma)$ be a ${G^{\mathsf{prob}}}$ -coalgebra. For each $x\in X$ , the depth- $n$ trace distribution $\mu^{n}_{x}\in\overline{\mathcal{D}}_{\omega}(\mathcal{A}^{\boxplus n})$ is inductively defined as $\mu^{n+1}_{x}(aw)=\sum_{y\in X}\gamma(x)(a,y)\mu^{n}_{y}(w)$ for $a\in\mathcal{A}$ and $w\in\mathcal{A}^{n}$ , with $\mu^{0}_{x}\in\overline{\mathcal{D}}_{\omega}(\mathcal{A}^{\boxplus 0})\cong% \overline{\mathcal{D}}_{\omega}(1)$ being the unique distribution on the singleton set $1$ . The probabilistic trace distance on $X$ is $d^{\mathsf{ptrace}}=\bigvee_{n<\omega}d_{n}^{\mathsf{ptrace}}$ , where $d^{\mathsf{ptrace}}_{n}(x,y)=d_{\overline{\mathcal{D}}_{\omega}(\mathcal{A}^{% \boxplus n})}(\mu^{n}_{x},\mu^{n}_{y})$ .

Consider the following concrete example, where we assume that $d(b,c)=0.5$ .

For $n\geq 2$ we then have by the above definition that $\mu^{n}_{x}=\frac{1}{2}aba^{n-2}+\frac{1}{2}aca^{n-2}$ while $\mu^{n}_{y}=\frac{1}{4}aba^{n-2}+\frac{3}{4}aca^{n-2}$ . The distance of the two relevant traces is given by $d(aba^{n-2},aca^{n-2})=d(a,a)\oplus d(b,c)\oplus d(a,a)\oplus\ldots\oplus d(a,% a)=0.5$ . Calculating the Kantorovich distance of trace distributions then gives us that $d(\mu^{n}_{x},\mu^{n}_{y})=\frac{1}{4}d(aba^{n-2},aca^{n-2})=0.125$ , and by extension $d^{\mathsf{ptrace}}(x,y)=0.125$ .

One would now like to have a logic that characterizes the trace distance $d^{\mathsf{ptrace}}$ . However, we establish the following impossibility result instead:

Theorem 3.2.

Let $\mathcal{L}=(\Theta,\mathcal{O},\Lambda)$ be a coalgebraic modal logic with unary modalities for the functor ${G^{\mathsf{prob}}}$ , over a non-discrete metric space $\mathcal{A}$ of labels. Then $d^{\mathcal{L}}\not=d^{\mathsf{ptrace}}$ .

In other words, no quantitative coalgebraic modal logic with unary modalities has a compositionally defined fragment that characterizes probabilistic metric trace distance. The restriction to coalgebraic modal logics effectively means only that modal logics should be invariant under the standard branching-time semantics and have only next-step modalities [39, 44]. Theorem 3.2 implies in particular that the logic featuring modalities $\Diamond_{a}$ for $a\in\mathcal{A}$ , with $\Diamond_{a}\phi$ being the expected truth value of $\phi$ restricted to $a$ -successors, fails to characterize probabilistic metric trace distance (even though it characterizes two-valued probabilistic trace equivalence [6, 14]). In fact, it can even be shown that giving up the requirement of interpretations of modalities being nonexpansive does not help.

Proof sketch (Theorem 3.2).

Suppose that $\mathcal{L}$ is invariant under probabilistic metric trace semantics ( $d^{\mathcal{L}}\leq d^{\mathsf{ptrace}}$ ); we show that $\mathcal{L}$ fails to be expressive ( $d^{\mathcal{L}}\not\geq d^{\mathsf{ptrace}}$ ). As an intermediate step, we show that invariance under probabilistic metric trace semantics implies that modal operators are affine maps. Then calculation shows that affine modalities are unable to distinguish the states $x$ and $y$ in the following system, where $d(a,b)=v<1$ , to a degree greater than $v^{2}$ , even though the behavioural distance of $x$ and $y$ under probabilistic trace semantics is $v$ .

$\hfill\blacktriangleleft$ We leave the question of whether a characteristic logic with higher-arity modalities exists as an open problem.

While expressive quantitative coalgebraic logics for branching-time semantics exist for a wide variety of systems [33, 50, 22, 26], this is thus apparently not always the case for linear-time semantics. The no-go result above emphasizes the challenges of the quantitative setting and the need for a theory of quantitative coalgebraic logics beyond branching time. In the following, we will address precisely this problem, by adopting techniques from the theory of graded semantics and highlighting issues unique to the metric setting.

4 Graded Monads and Graded Algebras

The framework of graded semantics [14, 37] is based on the central notion of graded monads, which algebraically describe the structure of observable behaviours, in particular identifications beyond branching time, at each finite depth. Here, depth is understood as look-ahead, measured in terms of the number of transition steps.

Definition 4.1.

A graded monad $\mathbb{M}=((M_{n})_{n\in\mathbb{N}},\eta,(\mu^{n,k})_{n,k\in\mathbb{N}})$ on a category $\mathcal{C}$ consists of a family of functors $M_{n}\colon\mathcal{C}\to\mathcal{C}$ for $n\in\mathbb{N}$ and natural transformations $\eta\colon\mathit{Id}\to M_{0}$ (the unit) and $\mu^{n,k}\colon M_{n}M_{k}\to M_{n+k}$ for all $n,k\in\mathbb{N}$ (the multiplications), subject to essentially the same laws as ordinary monads up to the insertion of grades; specifically, one has unit laws $\mu^{0,n}\cdot\eta M_{n}=\mathit{id}_{M_{n}}=\mu^{n,0}\cdot M_{n}\eta$ and an associative law $\mu^{n+k,m}\cdot\mu^{n,k}M_{m}=\mu^{n,k+m}\cdot M_{n}\mu^{k,m}$ .

In particular, $(M_{0},\eta,\mu^{00})$ is an ordinary (non-graded) monad.

The understanding of the data constituting a graded monad is similar as for plain monads: Roughly speaking (this will be made more precise in Section 5), $M_{n}X$ may be thought of as a space of terms of depth $n$ , modulo given identities, over variables from $X$ ; $\mu^{nk}$ substitutes depth- $k$ terms into a depth- $n$ term, obtaining a depth- $(n+k)$ term; and $\eta$ converts variables into terms of depth $0$ .

Example 4.2.

We discuss graded monads modelling the linear-time end of the spectrum, noting that graded monads cover also branching-time (7.10) and intermediate semantics, involving simulation, readiness, failures etc. [14]. A Kleisli distributive law is a natural transformation $\lambda\colon FT\to TF$ where $F$ is a functor and $T$ a monad, subject to coherence with the monad structure [27]. This yields a graded monad with $M_{n}=TF^{n}$ [37]; here, $T$ may be understood as defining the branching type of the system, and $F$ as defining a type of accepted structure. We will use the following instance of this construction as a running example: Take $F=\mathcal{A}\times(-)$ and $T=\overline{\mathcal{P}}_{\omega}$ or $T=\mathcal{P}_{c}$ (corresponding to nondeterministic branching). Then $\lambda(a,U)=\{(a,x)\mid x\in U\}$ defines a distributive law $\lambda\colon\mathcal{A}\times T({-})\to T(\mathcal{A}\times({-}))$ (in particular, $\lambda$ is nonexpansive). We obtain the graded metric trace monads $M_{n}=T(\mathcal{A}^{n}\times(-))$ .

Graded monads come with a graded analogue of Eilenberg-Moore algebras, which play a central role in the semantics of graded logics [37, 14].

Definition 4.3 (Graded Algebra).

Let $\mathbb{M}$ be a graded monad in $\mathcal{C}$ . A graded $M_{n}$ -algebra $((A_{k})_{k\leq n},(a^{mk})_{m+k\leq n})$ consists of a family of $\mathcal{C}$ -objects $A_{i}$ and morphisms $a^{mk}\colon M_{m}A_{k}\to A_{m+k}$ satisfying essentially the same laws as a monad algebra, up to insertion of the grades. Specifically, we have $a^{0m}\cdot\eta_{A_{m}}=\mathit{id}_{A_{m}}$ for $m\leq n$ , and whenever $m+r+k\leq n$ , then $a^{m+r,k}\cdot\mu^{m,r}_{A_{k}}=a^{m,r+k}\cdot M_{m}a^{r,k}$ . An $M_{n}$ -homomorphism of $M_{n}$ -algebras $A$ and $B$ is a family $(f_{k}\colon A_{k}\to B_{k})_{k\leq n}$ of maps such that whenever $m+k\leq n$ , then $f_{m+k}\cdot a^{m,k}=b^{m,k}\cdot M_{m}f_{k}$ . Graded $M_{n}$ -Algebras and their homomorphisms form a category $\text{Alg}_{n}(\mathbb{M})$ .

That is, elements of a graded algebra are stratified by depth, and applying an operation of depth $m$ to elements of depth $k$ yields elements of depth $m+k$ , For $n=1$ , this definition instantiates as follows: An $M_{1}$ -algebra is a tuple $(A_{0},A_{1},a^{00},a^{01},$ $a^{10})$ , such that 1) $(A_{0},a^{00})$ and $(A_{1},a^{01})$ are $M_{0}$ -algebras. 2) (Homomorphy) $a^{10}\colon M_{1}A_{0}\to A_{1}$ is an $M_{0}$ -homomorphism $(M_{1}A_{0},\mu^{01})\to(A_{1},a^{01})$ . 3) (Coequalization) $a^{10}\cdot M_{1}a^{00}=a^{10}\cdot\mu^{10}$ , i.e. the following diagram commutes (without necessarily being a coequalizer):

(4.1)

It is easy to see that $((M_{k}X)_{k\leq n},(\mu^{m,k})_{m+k\leq n})$ is an $M_{n}$ -algebra for every $\mathcal{C}$ -object $X$ . Again, $M_{0}$ -algebras are just (non-graded) algebras for the monad $(M_{0},\eta,\mu^{00})$ .
The semantics of modalities will later need the following property:

Definition 4.4 (Canonical algebras).

Let $({-})_{0}\colon\text{Alg}_{1}(\mathbb{M})\rightarrow\text{Alg}_{0}(\mathbb{M})$ be the functor taking an $M_{1}$ -algebra $A=((A_{k})_{k\leq 1},(a^{mk})_{m+k\leq 1})$ to the $M_{0}$ -algebra $(A_{0},a^{00})$ . An $M_{1}$ -algebra $A$ is canonical if it is free over $(A)_{0}$ , i.e. if for every $M_{1}$ -algebra $B$ and $M_{0}$ -homomorphism $f:(A)_{0}\rightarrow(B)_{0}$ , there is a unique $M_{1}$ -homomorphism $g:A\rightarrow B$ such that $(g)_{0}=f$ .

Lemma 4.5 ([14, Lemma 5.3]).

An $M_{1}$ -algebra $A$ is canonical iff (4.1) is a coequalizer diagram in the category of $M_{0}$ -algebras.

5 Graded Quantitative Theories

Monads on $\mathbf{Set}$ are induced by equational theories [35]. By equipping each operation with an assigned depth and requiring each axiom to be of uniform depth, one obtains a notion of graded equational theory which, modulo size issues, can be brought into bijective correspondence with graded monads [37]. On the other hand, Mardare et al. [36] introduce a system of quantitative equational reasoning, with formulae of the form $s=_{\epsilon}t$ understood as “ $s$ differs from $t$ by at most $\epsilon$ ”. These quantitative equational theories induce monads on the category of metric spaces. We introduce a graded version of this system to present graded monads in $\mathbf{Met}$ , keeping to finitary operations (and hence finite branching) for ease of presentation.

Definition 5.1 (Graded signatures, uniform terms).

A graded signature consists of an algebraic signature $\Sigma$ and a function $\delta\colon\Sigma\rightarrow\mathbb{N}$ assigning a depth to each algebraic operation. Uniform depth of terms is then defined inductively: Variables have uniform depth $0$ , and for $m$ -ary $f\in\Sigma$ , $f(t_{1},\ldots,t_{m})$ has uniform depth $n+k$ if $\delta(f)=n$ and all $t_{i}$ have uniform depth $k$ . In particular, constants $c\in\Sigma$ , as terms, have uniform depth $n$ for all $n\geq\delta(c)$ . We write $\mathbb{T}^{\Sigma}_{n}X$ , or just $\mathbb{T}_{n}X$ , for the set of terms of uniform depth $n$ over $X$ . A substitution of uniform depth $n$ is a function $\sigma\colon X\rightarrow\mathbb{T}_{n}Y$ . Such a substitution extends to a map $\sigma:\mathbb{T}_{k}X\rightarrow\mathbb{T}_{k+n}Y$ on terms for all $k\in\mathbb{N}$ , where as usual one defines $\sigma(f(t_{1},\ldots,t_{m}))=f(\sigma(t_{1}),\ldots,\sigma(t_{m}))$ . A substitution is uniform-depth if it is of uniform depth $n$ for some $n$ .

Definition 5.2 (Graded quantitative theory).

For a set $Z$ , we let $\mathcal{E}(Z)$ denote the set of quantitative equalities $z_{1}=_{\epsilon}z_{2}$ where $z_{1},z_{2}\in Z$ and $\epsilon\in[0,1]$ . Given a set $X$ of variables, we then write $\mathcal{E}(\mathbb{T}(X))=\bigcup_{n\in\mathbb{N}}\mathcal{E}(\mathbb{T}_{n}(% X))$ ; that is, $\mathcal{E}(\mathbb{T}(X))$ is the set of uniform-depth quantitative equalities among $\Sigma$ -terms over $X$ . A quantitative theory $\mathcal{T}=(\Sigma,\delta,E)$ consists of a graded signature $(\Sigma,\delta)$ and a set $E\subseteq\mathcal{P}(\mathcal{E}(X))\times\mathcal{E}(\mathbb{T}X)$ of axioms. Axioms $(\Gamma,s=_{\epsilon}t)$ are written in the form $\Gamma\vdash s=_{\epsilon}t$ ; we refer to $\Gamma$ as the context of the axiom. The depth of $\Gamma\vdash s=_{\epsilon}t$ is that of $s=_{\epsilon}t$ . We say that $\mathcal{T}$ is depth-1 if all its operations and axioms have depth at most $1$ .

The context $\Gamma$ of an axiom $\Gamma\vdash s=_{\epsilon}t$ forms a constraint on the variables that is required in order for $s=_{\epsilon}t$ to hold. Correspondingly, derivability of quantitative equalities in $\mathcal{E}(\mathbb{T}(X))$ over a graded quantitative theory $\mathcal{T}=(\Sigma,\delta,E)$ in a context $\Gamma_{0}\in\mathcal{P}(\mathcal{E}(X))$ is defined inductively by the following rules:

	$\displaystyle(\mathbf{triang})\;\frac{t=_{\epsilon}s\quad s=_{\epsilon^{\prime% }}u}{t=_{\epsilon+\epsilon^{\prime}}u}\qquad(\mathbf{refl})\;\frac{}{s=_{0}s}% \qquad(\mathbf{sym})\;\frac{t=_{\epsilon}s}{s=_{\epsilon}t}$
	$\displaystyle(\mathbf{wk})\;\frac{t=_{\epsilon}s}{t=_{\epsilon^{\prime}}s}\;(% \epsilon^{\prime}\geq\epsilon)\qquad(\mathbf{arch})\;\frac{\{t=_{\epsilon^{% \prime}}s\mid\epsilon^{\prime}>\epsilon\}}{t=_{\epsilon}s}\qquad(\mathbf{assn}% )\;\frac{}{\,\phi\,}\;(\phi\in\Gamma_{0})$
	$\displaystyle(\mathbf{ax})\;\frac{\{\sigma(u)\mid u\in\Gamma\}}{\sigma(t)=_{% \epsilon}\sigma(s)}\;((\Gamma,t=_{\epsilon}s)\in E)\qquad(\mathbf{nexp})\;% \frac{t_{1}=_{\epsilon}s_{1}\qquad\dots\qquad t_{n}=_{\epsilon}s_{n}}{f(t_{1},% \dots,t_{n})=_{\epsilon}f(s_{1},\dots,s_{n})}$

where $\sigma$ is a uniform-depth substitution. Note the difference between rules $(\mathbf{ax})$ and $(\mathbf{assn})$ : Quantitative equalities from the theory can be substituted into, while this is not sound for quantitative equalities from the context. A graded quantitative equational theory presents a graded monad $\mathbb{M}$ on $\mathbf{Met}$ where $M_{n}X$ is the set of terms of uniform depth $n$ over variables in $X$ , quotiented by the equivalence relation that identifies terms $s, t$ if $s=_{0}t$ is derivable in context $X$ , with the distance $d_{M_{n}}([s],[t])=\epsilon$ of equivalence classes $[s],[t]\in M_{n}X$ being the least $\epsilon$ such that $s=_{\epsilon}t$ is derivable (which exists by (arch)). Multiplication collapses terms-over-terms, and the unit maps an element of $x\in X$ to $[x]\in M_{0}X$ .

$\blacktriangleright$ Remark 5.3.

The above system for quantitative reasoning follows Ford et al. [20] in slight modifications to the original (ungraded) system [36]. In particular, we make do without a cut rule, and allow substitution only into axioms (substitution into derived equalities is then admissible [20]). We include the rule (nexp) ensuring that all operations are nonexpansive, i.e. the induced graded monad is enriched (acts nonexpansively on functions).

We recall that a graded monad is depth- $1$ [37, 14] if $\mu^{nk}$ and $M_{0}\mu^{1k}$ are epi-transformations and the diagram below is a coequalizer of $M_{0}$ -algebras for all $X$ and $n<\omega$ :

(5.1)

By 4.5 the following is then immediate:

Proposition 5.4 ([14, Corollary 5.4]).

If $\mathbb{M}$ is a depth-1 graded monad, then for every $n\in\mathbb{N}$ and every object $X$ , the $M_{1}$ -algebra with carriers $M_{n}X$ , $M_{n+1}X$ and multiplications as algebra structure is canonical.

We briefly refer to canonical algebras as per the above proposition as being of the form $M_{n}X$ .
Crucially, we establish a metric variant of a result on depth- $1$ graded monads on $\mathbf{Set}$ [37]:

Theorem 5.5.

Graded monads on $\mathbf{Met}$ presented by depth- $1$ graded quantitative theories are depth- $1$ .

$\blacktriangleright$ Remark 5.6.

A depth-1 graded monad $\mathbb{M}$ can be reconstructed from its constituents of depth at most one, i.e. from $M_{0}$ , $M_{1}$ , $\eta$ , and the $\mu^{nk}$ for $n+k\leq 1$ [14]. Graded semantics (Section 6) does however make use of the full structure of $\mathbb{M}$ also at higher depths.

Presentations of graded trace monads.

We proceed to investigate the quantitative-algebraic presentation of graded trace monads that are given by a Kleisli distributive law of the functor $\mathcal{A}\times(-)$ (with $\mathcal{A}$ being the space of action labels) over a monad (Example 4.2). Given a function $k\colon[0,1]^{2}\to[0,1]$ with suitable properties, we write $\otimes$ for the tensor that equips the Cartesian product of two sets with the metric $d_{A\otimes B}((a,b),(a^{\prime},b^{\prime}))=k(d(a,a^{\prime}),d(b,b^{\prime}))$ generated by $k$ . This induces trace distances on $\mathcal{A}^{n}$ , $n\geq 0$ , by viewing $\mathcal{A}^{n}$ as the $n$ -fold tensor of $\mathcal{A}$ . Examples include the Euclidean ( $k(x,y)=\sqrt{x^{2}+y^{2}}$ ), supremum ( $k(x,y)=\max(x,y)$ ), and Manhattan ( $k(x,y)=x\oplus y$ ) distances. The fact that $k$ computes distances of traces recursively “one symbol at a time” translates into uniform depth-1 equations:

Definition 5.7.

Let $\mathcal{T}=(\Sigma,\mathcal{E})$ be a quantitative algebraic presentation of a (plain) monad $T$ on $\mathbf{Met}$ . We define a graded quantitative theory $\mathcal{T}[\mathcal{A}]$ by including the operations and equations of $\mathcal{T}$ at depth $0$ , along with unary depth-1 operations $a$ for all labels $a\in\mathcal{A}$ , and as depth-1 axioms the distributive laws $\vdash a(f(x_{1},\ldots,x_{n}))=_{0}f(a(x_{1}),\ldots,a(x_{n}))$ for all $a\in\mathcal{A}$ and $f\in\Sigma$ , as well as the distance axioms $x=_{\epsilon}y\vdash a(x)=_{k(d(a,b),\epsilon)}b(y)$ .

The obvious candidate for a Kleisli distributive law inducing the graded monad presented by the theory $\mathcal{T}[\mathcal{A}]$ is the family of maps $\lambda_{X}\colon\mathcal{A}\otimes TX\to T(\mathcal{A}\otimes X)$ given by

\lambda_{X}(a,t)=T\langle a,\mathit{id}_{X}\rangle_{\otimes}(t)

(5.2)

where $\langle a,\mathit{id}_{X}\rangle_{\otimes}$ takes $x\in X$ to $(a,x)\in\mathcal{A}\otimes X$ . However, these maps $\lambda_{X}$ may fail to be nonexpansive, depending on $T$ and $\otimes$ ; for instance, this happens for $T=\overline{\mathcal{D}}_{\omega}$ and $\otimes$ being Cartesian product $\times$ (which carries the supremum distance):

Example 5.8.

Put $X=\{x,y\}$ where $d(x,y)=1$ , and $s=0.5\cdot x+0.5\cdot y$ , $t=1\cdot x\in\overline{\mathcal{D}}_{\omega}X$ . Clearly $d(s,t)=0.5$ . Given $a,b\in\mathcal{A}$ with $d(a,b)=0.5$ , we have $d((a,s),(b,t))=0.5$ in $\mathcal{A}\times\overline{\mathcal{D}}_{\omega}X$ while $d(\lambda_{X}(a,s),\lambda_{X}(b,t))=d(0.5\cdot(a,x)+0.5\cdot(a,y),1\cdot(b,x)% )=0.75$ in $\overline{\mathcal{D}}_{\omega}(\mathcal{A}\times X)$ .

Nonexpansiveness is, of course, needed to obtain a graded monad on $\mathbf{Met}$ , and as we show later (6.3), its failure may cause undesirable effects. In the case of Manhattan distance, nonexpansiveness always holds:

Lemma 5.9.

The maps $\lambda_{X}$ as per (5.2) are nonexpansive as maps $\mathcal{A}\boxplus TX\to T(\mathcal{A}\boxplus X)$ .

In case the $\lambda_{X}$ as per (5.2) are nonexpansive, we do in fact have that the distributive law $\lambda$ and the algebraic theory $\mathcal{T}[\mathcal{A}]$ induce the same graded monad:

Lemma 5.10.

Let $\lambda_{X}$ be defined by (5.2). If $\lambda_{X}\colon\mathcal{A}\otimes T\to T(\mathcal{A}\otimes(-))$ is nonexpansive for all $X$ , then the $\lambda_{X}$ form a Kleisli distributive law $\lambda\colon\mathcal{A}\otimes T\to T(\mathcal{A}\otimes(-))$ , and the graded monad induced by $\lambda$ according to Example 4.2 is presented by the quantitative equational theory $\mathcal{T}[\mathcal{A}]$ as per 5.7.

Example 5.11.

In our running example of finitely branching metric trace semantics, it is easy to check that the distributive law claimed in Example 4.2 is indeed nonexpansive, so the induced graded monad is, by 5.10, presented by the corresponding theory as per 5.7, and in particular is depth- $1$ . Explicitly, recall [36, Corollary 9.4] that $\overline{\mathcal{P}}_{\omega}$ is a monad, presented in quantitative algebra by the usual axioms of join semilattices for a binary join operation $+$ and a constant $0$ (nonexpansiveness of $+$ is enforced by the deduction rules). The quantitative graded theory presenting the graded metric trace monad $\overline{\mathcal{P}}_{\omega}(\mathcal{A}^{n}\times{-})$ according to 5.10 has depth-0 operators $+$ and $0$ as above and adds unary depth- $1$ operations $a$ for all $a\in\mathcal{A}$ , subject to axioms (for $a,b\in\mathcal{A}$ , $\epsilon\in[0,1]$ )

\vdash a(0)=_{0}0\qquad\vdash a(x+y)=_{0}a(x)+a(y)\qquad x=_{\epsilon}y\vdash a% (x)=_{\epsilon\vee d_{\mathcal{A}}(a,b)}b(y).

The distribution of the operations $a$ over the join semilattice structure effectively implements trace equivalence, and the last axiom determines the metric on traces, which in this case is taken to be the supremum metric.

6 Graded Quantitative Semantics and Graded Logics

We proceed to introduce the framework of graded quantitative semantics, to study spectra of behavioural metrics for various system types. By “spectra” we informally refer to collections of process comparisons of varying granularity that arise by observing a specific system type in different ways, as exemplified by the classical linear-time/branching-time spectrum on labelled transition systems [47]. Generally, a graded semantics [37] $(\mathbb{M},\alpha)$ of a functor $G\colon\mathcal{C}\to\mathcal{C}$ consists of a graded monad $\mathbb{M}$ and a natural transformation $\alpha\colon G\to M_{1}$ . Intuitively, $M_{n}1$ (where $1$ is a terminal object of $\mathcal{C}$ ) is a domain of behaviours observable after $n$ transition steps, with $\alpha$ determining behaviours after one step. For a $G$ -coalgebra $(X,\gamma)$ , we inductively define behaviour maps $\gamma^{(n)}\colon X\to M_{n}1$ assigning to a state in $X$ its behaviour after $n$ steps:

\gamma^{(0)}\colon X\xrightarrow{M_{0}!\cdot\eta}M_{0}1\hskip 30.00005pt\gamma% ^{(n+1)}\colon X\xrightarrow{\alpha\cdot\gamma}M_{1}X\xrightarrow{M_{1}\gamma^% {(n)}}M_{1}M_{n}1\xrightarrow{\mu^{1n}}M_{n+1}1

For $\mathcal{C}=\mathbf{Met}$ , these maps induce a notion of graded behavioural distance (for readability, we refrain from working with more general $\mathcal{C}$ , such as categories of relational structures [20]):

Definition 6.1 (Graded behavioural distance).

Given a graded semantics $\alpha\colon G\to M_{1}$ of a functor $G$ on $\mathbf{Met}$ , (graded) behavioural distance is the pseudometric on states in $G$ -coalgebras $(X,\gamma)$ given by $d^{\alpha}(x,y)=\bigvee_{n\in\mathbb{N}}d_{M_{n}1}(\gamma^{(n)}(x),\gamma^{(n)% }(y))$ for $x,y\in X$ .

Example 6.2.

The metric trace semantics of finitely branching metric transition systems [11, 15] and closed-branching metric transition systems is captured by the graded metric trace monads $M_{n}=\overline{\mathcal{P}}_{\omega}(\mathcal{A}^{n}\times{-})$ and $M_{n}=\mathcal{P}_{c}(\mathcal{A}^{n}\times{-})$ (Example 4.2), respectively (with $\alpha$ being identity). The behaviour maps calculate, at each depth $n$ , sets of length- $n$ traces, whose distance is given by the Hausdorff distance induced by the supremum metric on traces.

$\blacktriangleright$ Remark 6.3.

In cases where nonexpansiveness of $\alpha$ or the natural transformations of $\mathbb{M}$ does not hold (e.g. if one attempts to construct $\mathbb{M}$ using a family of maps (5.2) that fails to be nonexpansive, cf. Example 5.8), other expected properties can fail. For instance, it can happen that trace distance exceeds branching time distance (while for trace semantics induced by nonexpansive graded semantics, general properties of graded semantics imply that trace distance is below branching-time distance, in tune with the two-valued setting where trace equivalence is coarser than bisimilarity). Example 5.8 manifests in the $\overline{\mathcal{D}}_{\omega}(\mathcal{A}\times{-})$ -coalgebra (i.e. generative probabilistic metric transition system) shown below, where $\mathcal{A}=\{a,b,c,d\}$ with relevant distances $d(a,b)=0.5$ and $d(c,d)=1$ :

Here, we have length- $n$ trace distributions $\mu^{n}_{x}=\frac{1}{2}\cdot(aca^{n-2})+\frac{1}{2}\cdot(ada^{n-2})$ and $\mu^{n}_{y}=1\cdot(bca^{n-2})$ for $n\geq 2$ . When the metric on traces is defined via supremum distance, instead of Manhattan distance as in Section 3, the trace distance of the states $x$ and $y$ is $\bigvee_{n\in\mathbb{N}}d(\mu^{n}_{x},\mu^{n}_{y})=0.75$ , while their branching-time distance (cf. Section 2) is $0.5$ .

We have the following criterion for invariance of a logic under a graded semantics $(\alpha,\mathbb{M})$ , with $\mathbb{M}$ depth-1, for a functor $G\colon\mathbf{Met}\to\mathbf{Met}$ that we fix from now on; recall from Section 2 that we use $\Omega$ to denote the unit interval $[0,1]$ equipped with Euclidean distance.

Definition 6.4 (Graded logic).

Let $o\colon M_{0}\Omega\to\Omega$ be an $M_{0}$ -algebra structure on $\Omega$ . A logic $\mathcal{L}$ is a graded logic (for $(\alpha,\mathbb{M})$ ) if the following hold:

1.

For $n$ -ary $p\in\mathcal{O}$ , the semantics $\llbracket p\rrbracket$ is an $M_{0}$ -algebra homomorphism $(\Omega,o)^{n}\to(\Omega,o)$ .
2.

For each $L\in\Lambda$ , there is an associated nonexpansive map $\llparenthesis L\rrparenthesis\colon M_{1}\Omega\to\Omega$ such that the semantics $\llbracket L\rrbracket\colon G\Omega\to\Omega$ factors as $\llbracket L\rrbracket=(G\Omega\xrightarrow{\alpha_{\Omega}}M_{1}\Omega% \xrightarrow{\llparenthesis L\rrparenthesis}\Omega)$ , and such that the tuple $(\Omega,\Omega,o,o,\llparenthesis L\rrparenthesis)$ constitutes an $M_{1}$ -algebra (that is, $\llparenthesis L\rrparenthesis$ satisfies homomorphy and coequalization, cf. Section 2). We abuse notation and write $\llparenthesis L\rrparenthesis$ to denote the $M_{1}$ -algebra $(\Omega,\Omega,o,o,\llparenthesis L\rrparenthesis)$ .

Notice the different treatment of nullary propositional operators and truth constants: The former are required to be interpreted as homomorphisms $1\to(\Omega,o)$ in a graded logic, while no such condition is imposed on truth constants. In many examples, $\alpha=id$ , in which case condition 2 just states that $(\Omega,\Omega,o,o,\llbracket L\rrbracket)$ is an $M_{1}$ -algebra (non-identity $\alpha$ are associated, for instance, with readiness and failure semantics [14]).

Definition 6.5.

We say that $\mathcal{L}$ is invariant with respect to a graded semantics $(\alpha,\mathbb{M})$ if $d^{\mathcal{L}}\leq d^{\alpha}$ holds in all $G$ -coalgebras; expressive if $d^{\mathcal{L}}\geq d^{\alpha}$ ; and characteristic if $d^{\mathcal{L}}=d^{\alpha}$ .

Theorem 6.6 ([24, Proposition 21]).

Let $\mathcal{L}$ be a graded logic for $(\alpha,\mathbb{M})$ . Then the evaluation maps $\llbracket\phi\rrbracket_{\gamma}$ of uniform-depth $\mathcal{L}$ -formulae $\phi$ on $G$ -coalgebras $(X,\gamma)$ are nonexpansive w.r.t. behavioural distance $d^{\alpha}$ , and hence $\mathcal{L}$ is invariant.

The assumption of uniform depth cannot be removed in general [24].

Example 6.7.

We have a graded logic $\mathcal{L}^{\mathsf{mtrace}}$ for metric trace semantics (Example 6.2) featuring modalities $\Diamond_{a}$ for all $a\in\mathcal{A}$ as in 2.4, a single truth constant $1$ , and no propositional operators. We equip the set $\Omega=[0,1]$ of truth values with the usual $\overline{\mathcal{P}}_{\omega}$ -algebra (i.e. join semilattice) structure $([0,1],\vee,0)$ , and let $\hat{1}\colon 1\to[0,1]$ take the value $1$ . The logic $\mathcal{L}^{\mathsf{mtrace}}$ remains invariant under metric trace semantics when extended with propositional operators that are nonexpansive join-semilattice morphisms, such as $\vee$ . Analogously we define the logic $\mathcal{L}^{\mathsf{cmtrace}}$ for trace semantics of closed-branching metric transition systems. Notice that the interpretation of $1$ fails to be homomorphic, so $1$ needs to be a truth constant.

7 Expressivity Criteria

We proceed to adapt expressivity criteria appearing in previous work on two-valued behavioural equivalences [14, 19] to the quantitative setting, which poses quite specific challenges. A key role in the treatment of expressivity of logics will be played by the notion of initiality [1].

Definition 7.1.

A family of maps $(f_{i}\colon A\to B)_{i\in I}$ between metric spaces $A$ and $B$ is initial if $A$ carries the smallest (pseudo-)metric making all maps $f_{i}$ nonexpansive, explicitly: $d(x,y)=\bigvee_{i}d(f_{i}(x),f_{i}(y))$ .

Using this notion, the definition of expressivity can be rephrased as follows: An invariant logic $\mathcal{L}$ is expressive if for every $G$ -coalgebra $(X,\gamma)$ , the family of all evaluation maps $\llbracket\phi\rrbracket_{\gamma}$ of uniform-depth formulae $\phi$ is initial on $(X,d^{\alpha})$ .

$\blacktriangleright$ Remark 7.2.

In the branching-time case, a stronger notion of expressivity, roughly phrased as density of the set of depth- $n$ formulae in the set of nonexpansive properties at depth $n$ , follows from expressivity under certain additional conditions [22, 48, 49, 51, 33], using lattice-theoretic variants of the Stone-Weierstraß theorem. The analogue of the Stone-Weierstraß theorem in general fails for coarser semantics. Also, for semantics coarser than branching time, expressivity in the sense of 6.5 can often be established using more economic sets of propositional operators (e.g. no propositional operators at all), for which density will clearly fail.

Our expressivity result is based on propagating initiality through an induction on depth. Unlike in the Eilenberg-Moore case [24], this requires, in many examples, to strengthen the inductive invariant; we treat this systematically as follows:

Definition 7.3.

An initiality invariant is a property $\Phi$ of sets $\mathfrak{A}\subseteq\mathbf{Met}(X,\Omega)$ of nonexpansive functions such that (i) every family of maps satisfying $\Phi$ is initial, and (ii) $\Phi$ is upwards closed w.r.t. subset inclusion.

Example 7.4.

1.

Initiality itself is an initiality invariant. If $\Phi$ is initiality, then we say “initial-type” for “ $\Phi$ -type”.
2.

We say that $\mathfrak{A}\subseteq\mathbf{Met}(X,\Omega)$ is normed isometric if whenever $d(x,y)>\epsilon$ for $x,y\in X$ and $\epsilon>0$ , then there is some $f\in\mathfrak{A}$ such that $|f(x)-f(y)|>\epsilon$ and $f(x)\vee f(y)=1$ . Normed isometry is an initiality invariant.

Our expressivity criterion then takes the following shape:

Definition 7.5.

Let $\Phi$ be an initiality invariant. A graded logic $\mathcal{L}=(\Theta,\mathcal{O},\Lambda)$ with truth value object $(\Omega,o)$ is $\Phi$ -type depth-0 separating if the family of maps $\{o\cdot M_{0}\hat{c}\colon M_{0}1\to\Omega\mid c\in\Theta\}$ has property $\Phi$ . Moreover, $\mathcal{L}$ is $\Phi$ -type depth-1 separating if whenever $A$ is a canonical $M_{1}$ -algebra of the form $M_{n}1$ (5.4) and $\mathfrak{A}$ is a set of $M_{0}$ -homomorphisms $A_{0}\rightarrow\Omega$ that has property $\Phi$ and is closed under the propositional operators in $\mathcal{O}$ , then the set

\Lambda(\mathfrak{A}):=\{\llparenthesis L\rrparenthesis^{\bullet}(g):A_{1}% \rightarrow\Omega\mid L\in\Lambda,g\in\mathfrak{A}\}

has property $\Phi$ , where $\llparenthesis L\rrparenthesis^{\bullet}(g)\colon A_{1}\to\Omega$ is the (by canonicity, unique) morphism extending the $M_{0}$ -algebra morphism $g$ to an $M_{1}$ -algebra morphism $A\to\llparenthesis L\rrparenthesis$ (6.4).

Theorem 7.6 (Expressivity).

Let $\Phi$ be an initiality invariant, and suppose that a graded logic $\mathcal{L}$ is both $\Phi$ -type depth-0 separating and $\Phi$ -type depth-1 separating. Then $\mathcal{L}$ is expressive.

$\blacktriangleright$ Remark 7.7.

Our definition of separation differs from notions used for two-valued logics [14, 19] and for quantitative graded semantics induced by Eilenberg-Moore distributive laws [24], which overall have turned out to be much more well-behaved than the more general setting of the present work. The most obvious novelty is the use of an initiality invariant $\Phi$ strengthening the induction hypothesis in the inductive proof of Theorem 7.6. We will see that this is needed even in very simple examples in our more general setting. Moreover, we have phrased separation in terms of the specific canonical algebras $M_{n}1$ on which it is needed, rather than on unrestricted canonical algebras. This allows exploiting additional properties of $M_{n}1$ , e.g. that for graded monads $M_{n}=TF^{n}$ arising from Kleisli distributive laws (Example 4.2), $M_{n}1$ is free as an $M_{0}$ -algebra.

Example 7.8.

1.

Metric Streams: A simple example for failure of initial-type separation (Example 7.4) are metric streams, i.e. streams over a metric space of labels $(\mathcal{A},d_{\mathcal{A}})$ ; these are coalgebras for the functor $G=\mathcal{A}\times{-}$ . Behavioural distance on streams is captured by the graded monad $G^{n}=\mathcal{A}^{n}\times\{-\}$ . The logic $\mathcal{L}$ consisting of the truth constant $1$ and modalities $\Diamond_{a}$ for all $a\in\mathcal{A}$ , with interpretation $\llbracket\Diamond_{a}\rrbracket\colon\mathcal{A}\times[0,1]\to[0,1]$ given by $(b,v)\mapsto(1-d_{\mathcal{A}}(a,b))\wedge v$ , is $\Phi$ -type depth-0 separating and $\Phi$ -type depth-1 separating for $\Phi$ being normed isometry, and hence expressive by Theorem 7.6. (The modality $\Diamond_{a}$ restricts the corresponding modality for metric transition systems as per 2.4 and 6.7 to metric streams: a state satisfies $\Diamond_{a}\phi$ to the degree that its output is close to $a$ and its successor satisfies $\phi$ ). On the other hand, $\mathcal{L}$ fails to be initial-type depth-1 separating, illustrating the necessity of the general form of Theorem 7.6.
2.

Metric transition systems: The graded logics $\mathcal{L}^{\mathsf{mtrace}}$ and $\mathcal{L}^{\mathsf{cmtrace}}$ for metric trace semantics (Example 6.7), in the version with no propositional operators, are $\Phi$ -type depth- $0$ separating and $\Phi$ -type depth- $1$ separating for $\Phi$ being normed isometry, and hence are expressive by Theorem 7.6. We thus improve on an example from recent work based on Galois connections [4], where application of the general framework required the inclusion of propositional shift operators (which were subsequently eliminated in an ad-hoc manner), and we generalize to systems with closed branching on a metric state space.
3.

Probabilistic metric trace semantics is modelled straightforwardly as a graded semantics using a graded trace monad (Example 4.2). By Theorem 3.2, however, there is no graded logic for probabilistic metric trace semantics that satisfies the conditions of Theorem 7.6.

$\blacktriangleright$ Remark 7.9.

In a recent approach based on Galois connections [4, 5], logics are related to fixpoints of behaviour functions induced by the logic itself (similar to approaches that define trace semantics via intended characteristic logics [31]), while our present interest is in providing logical characterizations of given behavioural distances. The Galois framework is highly general, and in fact not even tied to coalgebraic modelling, or in fact to state-based systems of any kind [4], but correspondingly offers less concrete recipes. Instantiated to our current setup, the key condition of compatibility appearing in op. cit. roughly speaking amounts to initial-type depth-1 separation of the logic w.r.t. its own Kantorovich lifting [2, 5].

$\blacktriangleright$ Remark 7.10 (Branching-time semantics).

Any functor $G$ yields a graded monad given by iterated application of $G$ , that is $M_{n}=G^{n}$ , and by unit and multiplication being identity [37]. In general, the finite-depth branching-time semantics of a $G$ -coalgebra $(X,\gamma)$ is defined via its canonical cone $(p_{i}\colon X\to G^{i}1)_{i<\omega}$ into the final sequence $1\xleftarrow{!}G1\xleftarrow{G!}G^{2}1\leftarrow\dots$ of $G$ . The $p_{i}$ are defined inductively by $p_{0}=\mathord{!}\,\colon X\to 1$ and $p_{i+1}=Gp_{i}\cdot\gamma$ . This semantics is captured by the graded monad $M_{n}=G^{n}$ and $\alpha=\mathit{id}$ [37]. More specifically, the finite-depth branching-time behavioural distance of states $x,y\in X$ is $\bigvee_{i<\omega}d(p_{i}(x),p_{i}(y))$ , and thus agrees with the graded behavioural distance obtained via the graded semantics in the graded monad $M_{n}=G^{n}$ . This monad has $M_{0}=\mathit{id}$ , so that the corresponding graded logics are just branching-time logics without further restriction [37, 14]. Coalgebraic quantitative logics of this kind have received some recent attention [22, 48, 49, 51, 11, 30, 33]. Suppose $\Lambda$ is a finite separating set of modalities, i.e. the maps $\llbracket L\rrbracket\cdot Gf\colon GX\to\Omega$ , with $L$ ranging over modalities and $f$ over nonexpansive maps $X\to\Omega$ , form an initial family. Moreover, let $\mathcal{O}$ contain truth $1$ , meet $\land$ , fuzzy negation $\neg$ (i.e. $\neg x=1-x$ ), and truncated addition of constants $(-)\oplus c$ . Then one shows using a variant of the Stone-Weierstraß theorem [51] that the graded logic $\mathcal{L}$ given by $\Lambda$ , $\mathcal{O}$ , and $\Theta=\emptyset$ is initial-type depth- $0$ separating and initial-type depth- $1$ separating. By Theorem 7.6, we obtain that $\mathcal{L}$ is expressive. Previous work on quantitative branching-time logics [51, 33, 48, 49, 22] discusses, amongst other things, conditions on $G$ that allow concluding expressivity even for infinite-depth behavioural distance.

8 Case Study: Fuzzy Metric Trace Semantics

We apply the recipe outlined above to obtain a characteristic logic for trace distance on fuzzy metric transition systems. That is, we proceed as follows: We cast fuzzy metric trace distance as a graded semantics using a suitable depth-1 graded monad $\mathbb{M}$ , and check that $\mathbb{M}$ is depth-1 using the techniques outlined in Section 5. We then identify a corresponding graded logic $\mathcal{L}$ , verifying the requirements of 6.4. Invariance of $\mathcal{L}$ then follows automatically (Theorem 6.6). Finally, we show expressivity using Theorem 7.6.

A fuzzy $\mathcal{A}$ -labelled metric transition system (fuzzy metric LTS) [12, 54, 55, 30]) consists of a set (or metric space) $X$ of states and a fuzzy transition relation $R\colon X\times\mathcal{A}\times X\to[0,1]$ , with $\mathcal{A}$ a metric space. A fuzzy LTS $(X,R)$ is finitely branching if $\{(a,y)\mid R(x,a,y)>0\}$ is finite for every $x\in X$ . Equivalently, a finitely branching fuzzy LTS is a coalgebra for the functor $\overline{\mathcal{F}}_{\omega}(\mathcal{A}\times(-))$ (cf. 2.2.4).

A natural fuzzy trace semantics of fuzzy transition systems assigns to each state $x$ of a fuzzy LTS $(X,R)$ a fuzzy trace set $\mathit{Tr}(x)\in\mathcal{F}_{\omega}(\mathcal{A}^{*})$ where

\textstyle\mathit{Tr}(x)(a_{1}\dots a_{n})=\bigvee\{\bigwedge_{i=1}^{n}R(x_{i-% 1},a_{i},x_{i})\mid x=x_{0},x_{1},\dots,x_{n}\in X\}.

This notion of trace relates, for instance, to a notion of fuzzy path that is implicit in the semantics of fuzzy computation tree logic [38] and to notions of fuzzy language accepted by fuzzy automata (e.g. [3]). We obtain a notion of fuzzy trace distance $d^{T}$ of states $x, y$ , given by the distance of $\mathit{Tr}(x)$ , $\mathit{Tr}(y)$ in $\overline{\mathcal{F}}_{\omega}(\mathcal{A}^{*})$ , i.e. under fuzzy Hausdorff distance (2.2.4) w.r.t. the metric on $\mathcal{A}^{*}$ that is the supremum metric on each $\mathcal{A}^{n}$ , and assigns distance $1$ to traces of different lengths. To capture this distance in a graded semantics, consider the distributive law $\lambda\colon\mathcal{A}\times\overline{\mathcal{F}}_{\omega}({-})\to\overline% {\mathcal{F}}_{\omega}(\mathcal{A}\times{-})$ given by $\lambda(a,U)(a,x)=U(x)$ and $\lambda(a,U)(b,x)=0$ for $b\neq a$ . By Example 4.2 we thus obtain the graded fuzzy metric trace monad $M_{n}=\overline{\mathcal{F}}_{\omega}(\mathcal{A}^{n}\times(-))$ . The monad $\overline{\mathcal{F}}_{\omega}$ can be presented by the following quantitative equational theory: Take a binary operation $+$ , a constant $0$ , and unary operations $r$ for every $r\in[0,1]$ . Impose strict equations ( $=_{0}$ ) saying that $+$ , $0$ form a join semilattice structure and that the operations $r$ define an action of the monoid $([0,1],\wedge)$ (i.e. $1(x)=x$ , $r(s(x))=_{0}(r\wedge s)(x)$ ). Finally, impose axioms $x=_{\epsilon}y\vdash r(x)=_{\epsilon}s(y)$ for $r,s\in[0,1]$ such that $|r-s|\leq\epsilon$ . By 5.10, the graded fuzzy trace monad $M_{n}=\overline{\mathcal{F}}_{\omega}(\mathcal{A}^{n}\times X)$ is presented by the above algebraic description of $\overline{\mathcal{F}}_{\omega}$ at depth $0$ , with additional depth-1 unary operations $a$ for $a\in\mathcal{A}$ and depth-1 equations $a(x+y)=_{0}a(x)+a(y)$ , $a(0)=_{0}0$ , $a(r(x))=_{0}r(a(x))$ , and $x=_{\epsilon}y\vdash a(x)=_{\epsilon\vee d(a,b)}b(y)$ .

Fuzzy metric trace logic interprets the additional operations $r\in[0,1]$ on the truth value object $[0,1]$ by $r(x)=r\wedge x$ , and otherwise uses the same quantitative join semilattice structure as for metric trace semantics (Example 6.7). We include the truth constant $1$ and modal operators $\Diamond_{a}^{c}$ for $a\in\mathcal{A}$ and $c\in[0,1]\cap\mathbb{Q}$ , with interpretation $\llbracket\Diamond_{a}^{c}\rrbracket\colon M_{1}[0,1]\to[0,1]$ given by $\llbracket\Diamond_{a}^{c}\rrbracket(A)=\bigvee_{b\in\mathcal{A},v\in[0,1]}A(b% ,v)\wedge v\wedge(c\ominus d(a,b))$ . (When $\mathcal{A}$ is discrete, then $\Diamond_{a}^{1}$ is the usual fuzzy diamond modality, e.g. [18]). Thus, a state $x$ in a fuzzy metric transition system satisfies $\Diamond^{c}_{a}\phi$ to the degree that $x$ has a $b$ -successor $y$ with $b$ close to $a$ and $y$ satisfying $\phi$ ; crucially, “closeness” of $b$ to $a$ needs to be shifted down as governed by the parameter $c$ . This logic is initial-type depth- $0$ separating and initial-type depth- $1$ separating, and hence expressive for fuzzy trace distance by Theorem 7.6; both this result and the logic itself appear to be new (the case with $\mathcal{A}$ discrete is partially covered in work on Galois connections [5]). Indeed for non-discrete $\mathcal{A}$ , the logic with only $\Diamond_{a}^{1}$ instead of all $\Diamond_{a}^{c}$ fails to be expressive. The logic remains invariant when extended with additional nonexpansive propositional operators that are $\overline{\mathcal{F}}_{\omega}$ -homomorphic, such as $\vee$ .

9 Conclusions

We have shown that there is no unary quantitative coalgebraic modal logic characterizing a natural notion of quantitative trace distance on probabilistic metric transition systems. Moving onwards from this observation, we have developed a generic framework for linear-time/branching-time spectra of behavioural distances on state-based systems in coalgebraic generality, covering, for instance, metric, probabilistic, and fuzzy transition systems. Unlike previous work on Eilenberg-Moore-style coalgebraic trace distances [5, 24], the framework covers also systems with labels from a metric space. The key abstractions in the framework are based on the notion of a graded monad on the category of metric spaces and an arising notion of quantitative graded semantics. We have provided a graded quantitative algebraic system for the description of such graded monads (extending and modifying the existing non-graded system [36]). Moreover, we have established sufficient conditions for canonical invariant quantitative graded logics [24] to be expressive for given quantitative graded semantics, and we have exploited this result to obtain expressive logics for some instances of Kleisli-type trace semantics [27], notably including a new result for fuzzy metric trace semantics.

One important next step in the development will be to identify a generic game-based characterization of behavioural distances in the framework of graded semantics, generalizing work specific to metric transition systems [15] and building on game-based concepts for two-valued graded semantics [21]. Also, there is interest in computing distinguishing quantitative formulae (cf. [10, 52] for the two-valued branching-time setting), generalizing recent results for the branching-time case [40] to spectra of coarser semantics.

References

[1] Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories. John Wiley and Sons, 1990. Reprint: http://www.tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
[2] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:20)2018.
[3] Radim Belohlávek. Determinism and fuzzy automata. Inf. Sci., 143(1-4):205–209, 2002. doi:10.1016/S0020-0255(02)00192-5.
[4] Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner theorems via Galois connections. In Bartek Klin and Elaine Pimentel, editors, Computer Science Logic, CSL 2023, volume 252 of LIPIcs, pages 12:1–12:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.CSL.2023.12.
[5] Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive quantale-valued logics for coalgebras: An adjunction-based approach. In Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov, editors, Theoretical Aspects of Computer Science, STACS 2024, volume 289 of LIPIcs, pages 10:1–10:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.STACS.2024.10.
[6] Marco Bernardo and Stefania Botta. A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems. Math. Struct. Comput. Sci., 18(1):29–55, 2008. doi:10.1017/S0960129507006408.
[7] Valentina Castiglioni, Konstantinos Chatzikokolakis, and Catuscia Palamidessi. A logical characterization of differential privacy via behavioral metrics. In Kyungmin Bae and Peter Ölveczky, editors, Formal Aspects of Component Software, FACS 2018, volume 11222 of LNCS, pages 75–96. Springer, 2018. doi:10.1007/978-3-030-02146-7.
[8] Valentina Castiglioni, Daniel Gebler, and Simone Tini. Logical characterization of bisimulation metrics. In Mirco Tribastone and Herbert Wiklicky, editors, Quantitative Aspects of Programming Languages and Systems, QAPL 2016, volume 227 of EPTCS, pages 44–62, 2016. doi:10.4204/EPTCS.227.
[9] Ivan Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Jos C. M. Baeten and Jan Willem Klop, editors, Theories of Concurrency: Unification and Extension, CONCUR 1990, volume 458 of LNCS, pages 126–140. Springer, 1990. doi:10.1007/BFb0039056.
[10] Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer Aided Verification, CAV 1990, volume 531 of LNCS, pages 364–372. Springer, 1990. doi:10.1007/BFB0023750.
[11] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Trans. Software Eng., 35(2):258–273, 2009. doi:10.1109/TSE.2008.106.
[12] Liliana D’Errico and Michele Loreti. Modeling fuzzy behaviours in concurrent systems. In Giuseppe F. Italiano, Eugenio Moggi, and Luigi Laura, editors, Theoretical Computer Science, 10th Italian Conference, ICTCS 2007, pages 94–105. World Scientific, 2007. doi:10.1142/9789812770998_0012.
[13] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323–354, 2004. doi:10.1016/j.tcs.2003.09.013.
[14] Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded monads and graded logics for the linear time - branching time spectrum. In Wan J. Fokkink and Rob van Glabbeek, editors, Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 36:1–36:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.CONCUR.2019.36.
[15] Uli Fahrenberg and Axel Legay. The quantitative linear-time-branching-time spectrum. Theor. Comput. Sci., 538:54–69, 2014. doi:10.1016/j.tcs.2013.07.030.
[16] Uli Fahrenberg, Axel Legay, and Claus Thrane. The quantitative linear-time–branching-time spectrum. In Supratik Chakraborty and Amit Kumar, editors, Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, volume 13 of LIPIcs, pages 103–114. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2011. doi:10.4230/LIPIcs.FSTTCS.2011.103.
[17] Ihor Filimonov, Ross Horne, Sjouke Mauw, and Zach Smith. Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity. In Kazue Sako, Steve A. Schneider, and Peter Y. A. Ryan, editors, Computer Security, ESORICS 2019, volume 11735 of LNCS, pages 577–594. Springer, 2019. doi:10.1007/978-3-030-29959-0_28.
[18] Melvin Fitting. Many-valued modal logics. Fund. Inform., 15:235–254, 1991. doi:10.3233/FI-1991-153-404.
[19] Chase Ford, Stefan Milius, and Lutz Schröder. Behavioural preorders via graded monads. In Logic in Computer Science, LICS 2021, pages 1–13. IEEE, 2021. doi:10.1109/LICS52264.2021.9470517.
[20] Chase Ford, Stefan Milius, and Lutz Schröder. Monads on categories of relational structures. In Fabio Gadducci and Alexandra Silva, editors, Algebra and Coalgebra in Computer Science, CALCO 2021, volume 211 of LIPIcs, pages 14:1–14:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.CALCO.2021.14.
[21] Chase Ford, Stefan Milius, Lutz Schröder, Harsh Beohar, and Barbara König. Graded monads and behavioural equivalence games. In Christel Baier and Dana Fisman, editors, Logic in Computer Science, LICS 2022, pages 61:1–61:13. ACM, 2022. doi:10.1145/3531130.3533374.
[22] Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantitative Hennessy-Milner theorems via notions of density. In Bartek Klin and Elaine Pimentel, editors, Computer Science Logic, CSL 2023, volume 252 of LIPIcs, pages 22:1–22:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.CSL.2023.22.
[23] Jonas Forster, Lutz Schröder, and Paul Wild. Quantitative graded semantics and spectra of behavioural metrics. CoRR, abs/2306.01487, 2023. doi:10.48550/arXiv.2306.01487.
[24] Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, and Karla Messing. Graded semantics and graded logics for Eilenberg-Moore coalgebras. In Barbara König and Henning Urbat, editors, Coalgebraic Methods in Computer Science, CMCS 2024, volume 14617 of LNCS, pages 114–134. Springer, 2024. doi:10.1007/978-3-031-66438-0_6.
[25] Alessandro Giacalone, Chi-Chang Jou, and Scott Smolka. Algebraic reasoning for probabilistic concurrent systems. In Manfred Broy, editor, Programming concepts and methods, PCM 1990, pages 443–458. North-Holland, 1990.
[26] Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Kantorovich functors and characteristic logics for behavioural distances. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2023, volume 13992 of LNCS, pages 46–67. Springer, 2023. doi:10.1007/978-3-031-30829-1_3.
[27] Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Methods Comput. Sci., 3(4), 2007. doi:10.2168/LMCS-3(4:11)2007.
[28] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137–161, 1985. doi:10.1145/2455.2460.
[29] Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859–879, 2015. doi:10.1016/j.jcss.2014.12.005.
[30] Manisha Jain, Alexandre Madeira, and Manuel A. Martins. A fuzzy modal logic for fuzzy transition systems. In Amy P. Felty and João Marcos, editors, Logical and Semantic Frameworks with Applications, LSFA 2019, volume 348 of ENTCS, pages 85–103. Elsevier, 2019. doi:10.1016/j.entcs.2020.02.006.
[31] Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. Log. Methods Comput. Sci., 12(4), 2016. doi:10.2168/LMCS-12(4:10)2016.
[32] Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo. Expressivity of quantitative modal logics : Categorical foundations via codensity and approximation. In Logic in Computer Science, LICS 2021, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470656.
[33] Barbara König and Christina Mika-Michalski. (metric) bisimulation games and real-valued modal logics for coalgebras. In Sven Schewe and Lijun Zhang, editors, Concurrency Theory, CONCUR 2018, volume 118 of LIPIcs, pages 37:1–37:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.CONCUR.2018.37.
[34] Clemens Kupke and Jurriaan Rot. Expressive logics for coinductive predicates. Log. Methods Comput. Sci., 17(4), 2021. doi:10.46298/lmcs-17(4:19)2021.
[35] F. E. J. Linton. Some aspects of equational categories. In S. Eilenberg, D. K. Harrison, S. MacLane, and H. Röhrl, editors, Proceedings of the Conference on Categorical Algebra, pages 84–94. Springer, 1966. doi:10.1007/978-3-642-99902-4_3.
[36] Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Logic in Computer Science, LICS 2016, pages 700–709. ACM, 2016. doi:10.1145/2933575.2934518.
[37] Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. In Lawrence S. Moss and Pawel Sobocinski, editors, Algebra and Coalgebra in Computer Science, CALCO 2015, volume 35 of LIPIcs, pages 253–269. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPIcs.CALCO.2015.253.
[38] Haiyu Pan, Yongming Li, Yongzhi Cao, and Zhanyou Ma. Model checking computation tree logic over finite lattices. Theor. Comput. Sci., 612:45–62, 2016. doi:10.1016/j.tcs.2015.10.014.
[39] Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19–33, 2004. doi:10.1305/NDJFL/1094155277.
[40] Amgad Rady and Franck van Breugel. Explainability of probabilistic bisimilarity distances for labelled Markov chains. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2023, volume 13992 of LNCS, pages 285–307. Springer, 2023. doi:10.1007/978-3-031-30829-1_14.
[41] Jurriaan Rot, Bart Jacobs, and Paul Blain Levy. Steps and traces. J. Log. Comput., 31(6):1482–1525, 2021. doi:10.1093/logcom/exab050.
[42] Jan J. M. M. Rutten. Relators and metric bisimulations. In Bart Jacobs, Larry Moss, Horst Reichel, and Jan J. M. M. Rutten, editors, Coalgebraic Methods in Computer Science, CMCS 1998, volume 11 of ENTCS, pages 252–258. Elsevier, 1998. doi:10.1016/S1571-0661(04)00063-5.
[43] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.
[44] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390(2-3):230–247, 2008. doi:10.1016/j.tcs.2007.09.023.
[45] Lutz Schröder and Dirk Pattinson. Description logics and fuzzy probability. In Toby Walsh, editor, International Joint Conference on Artificial Intelligence, IJCAI 2011, pages 1075–1081. IJCAI/AAAI, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-184.
[46] Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115–142, 2005. doi:10.1016/j.tcs.2004.09.035.
[47] Rob J. van Glabbeek. The linear time - branching time spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3–99. North-Holland/Elsevier, 2001. doi:10.1016/b978-044482830-9/50019-9.
[48] Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov and Laura Kovács, editors, Concurrency Theory, CONCUR 2020, volume 171 of LIPIcs, pages 27:1–27:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.27.
[49] Paul Wild and Lutz Schröder. A quantified coalgebraic van Benthem theorem. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, FOSSACS 2021, volume 12650 of LNCS, pages 551–571. Springer, 2021. doi:10.1007/978-3-030-71995-1_28.
[50] Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci., 18(2), 2022. doi:10.46298/lmcs-18(2:19)2022.
[51] Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König. A van Benthem theorem for fuzzy modal logic. In Anuj Dawar and Erich Grädel, editors, Logic in Computer Science, LICS 2018, pages 909–918. ACM, 2018. doi:10.1145/3209108.3209180.
[52] Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Explaining behavioural inequivalence generically in quasilinear time. In Serge Haddad and Daniele Varacca, editors, Concurrency Theory, CONCUR 2021, volume 203 of LIPIcs, pages 32:1–32:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.32.
[53] James Worrell. Coinduction for recursive data types: partial orders, metric spaces and omega-categories. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 337–356. Elsevier, 2000. doi:10.1016/S1571-0661(05)80356-1.
[54] Hengyang Wu, Taolue Chen, Tingting Han, and Yixiang Chen. Bisimulations for fuzzy transition systems revisited. Int. J. Approx. Reason., 99:1–11, 2018. doi:10.1016/j.ijar.2018.04.010.
[55] Hengyang Wu, Yixiang Chen, Tian-Ming Bu, and Yuxin Deng. Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems. Fuzzy Sets Syst., 333:106–123, 2018. doi:10.1016/j.fss.2017.02.008.

[bib.bib1] [1] Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories. John Wiley and Sons, 1990. Reprint: http://www.tac.mta.ca/tac/reprints/articles/17/tr17abs.html.

[bib.bib2] [2] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. doi:10.23638/LMCS-14(3:20)2018.

[bib.bib3] [3] Radim Belohlávek. Determinism and fuzzy automata. Inf. Sci., 143(1-4):205–209, 2002. doi:10.1016/S0020-0255(02)00192-5.

[bib.bib4] [4] Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner theorems via Galois connections. In Bartek Klin and Elaine Pimentel, editors, Computer Science Logic, CSL 2023, volume 252 of LIPIcs, pages 12:1–12:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.CSL.2023.12.

[bib.bib5] [5] Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive quantale-valued logics for coalgebras: An adjunction-based approach. In Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov, editors, Theoretical Aspects of Computer Science, STACS 2024, volume 289 of LIPIcs, pages 10:1–10:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.STACS.2024.10.

[bib.bib6] [6] Marco Bernardo and Stefania Botta. A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems. Math. Struct. Comput. Sci., 18(1):29–55, 2008. doi:10.1017/S0960129507006408.

[bib.bib7] [7] Valentina Castiglioni, Konstantinos Chatzikokolakis, and Catuscia Palamidessi. A logical characterization of differential privacy via behavioral metrics. In Kyungmin Bae and Peter Ölveczky, editors, Formal Aspects of Component Software, FACS 2018, volume 11222 of LNCS, pages 75–96. Springer, 2018. doi:10.1007/978-3-030-02146-7.

[bib.bib8] [8] Valentina Castiglioni, Daniel Gebler, and Simone Tini. Logical characterization of bisimulation metrics. In Mirco Tribastone and Herbert Wiklicky, editors, Quantitative Aspects of Programming Languages and Systems, QAPL 2016, volume 227 of EPTCS, pages 44–62, 2016. doi:10.4204/EPTCS.227.

[bib.bib9] [9] Ivan Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Jos C. M. Baeten and Jan Willem Klop, editors, Theories of Concurrency: Unification and Extension, CONCUR 1990, volume 458 of LNCS, pages 126–140. Springer, 1990. doi:10.1007/BFb0039056.

[bib.bib10] [10] Rance Cleaveland. On automatically explaining bisimulation inequivalence. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer Aided Verification, CAV 1990, volume 531 of LNCS, pages 364–372. Springer, 1990. doi:10.1007/BFB0023750.

[bib.bib11] [11] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Trans. Software Eng., 35(2):258–273, 2009. doi:10.1109/TSE.2008.106.

[bib.bib12] [12] Liliana D’Errico and Michele Loreti. Modeling fuzzy behaviours in concurrent systems. In Giuseppe F. Italiano, Eugenio Moggi, and Luigi Laura, editors, Theoretical Computer Science, 10th Italian Conference, ICTCS 2007, pages 94–105. World Scientific, 2007. doi:10.1142/9789812770998_0012.

[bib.bib13] [13] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323–354, 2004. doi:10.1016/j.tcs.2003.09.013.

[bib.bib14] [14] Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded monads and graded logics for the linear time - branching time spectrum. In Wan J. Fokkink and Rob van Glabbeek, editors, Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 36:1–36:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.CONCUR.2019.36.

[bib.bib15] [15] Uli Fahrenberg and Axel Legay. The quantitative linear-time-branching-time spectrum. Theor. Comput. Sci., 538:54–69, 2014. doi:10.1016/j.tcs.2013.07.030.

[bib.bib16] [16] Uli Fahrenberg, Axel Legay, and Claus Thrane. The quantitative linear-time–branching-time spectrum. In Supratik Chakraborty and Amit Kumar, editors, Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, volume 13 of LIPIcs, pages 103–114. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2011. doi:10.4230/LIPIcs.FSTTCS.2011.103.

[bib.bib17] [17] Ihor Filimonov, Ross Horne, Sjouke Mauw, and Zach Smith. Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity. In Kazue Sako, Steve A. Schneider, and Peter Y. A. Ryan, editors, Computer Security, ESORICS 2019, volume 11735 of LNCS, pages 577–594. Springer, 2019. doi:10.1007/978-3-030-29959-0_28.

[bib.bib18] [18] Melvin Fitting. Many-valued modal logics. Fund. Inform., 15:235–254, 1991. doi:10.3233/FI-1991-153-404.

[bib.bib19] [19] Chase Ford, Stefan Milius, and Lutz Schröder. Behavioural preorders via graded monads. In Logic in Computer Science, LICS 2021, pages 1–13. IEEE, 2021. doi:10.1109/LICS52264.2021.9470517.

[bib.bib20] [20] Chase Ford, Stefan Milius, and Lutz Schröder. Monads on categories of relational structures. In Fabio Gadducci and Alexandra Silva, editors, Algebra and Coalgebra in Computer Science, CALCO 2021, volume 211 of LIPIcs, pages 14:1–14:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.CALCO.2021.14.

[bib.bib21] [21] Chase Ford, Stefan Milius, Lutz Schröder, Harsh Beohar, and Barbara König. Graded monads and behavioural equivalence games. In Christel Baier and Dana Fisman, editors, Logic in Computer Science, LICS 2022, pages 61:1–61:13. ACM, 2022. doi:10.1145/3531130.3533374.

[bib.bib22] [22] Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantitative Hennessy-Milner theorems via notions of density. In Bartek Klin and Elaine Pimentel, editors, Computer Science Logic, CSL 2023, volume 252 of LIPIcs, pages 22:1–22:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.CSL.2023.22.

[bib.bib23] [23] Jonas Forster, Lutz Schröder, and Paul Wild. Quantitative graded semantics and spectra of behavioural metrics. CoRR, abs/2306.01487, 2023. doi:10.48550/arXiv.2306.01487.

[bib.bib24] [24] Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, and Karla Messing. Graded semantics and graded logics for Eilenberg-Moore coalgebras. In Barbara König and Henning Urbat, editors, Coalgebraic Methods in Computer Science, CMCS 2024, volume 14617 of LNCS, pages 114–134. Springer, 2024. doi:10.1007/978-3-031-66438-0_6.

[bib.bib25] [25] Alessandro Giacalone, Chi-Chang Jou, and Scott Smolka. Algebraic reasoning for probabilistic concurrent systems. In Manfred Broy, editor, Programming concepts and methods, PCM 1990, pages 443–458. North-Holland, 1990.

[bib.bib26] [26] Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Kantorovich functors and characteristic logics for behavioural distances. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2023, volume 13992 of LNCS, pages 46–67. Springer, 2023. doi:10.1007/978-3-031-30829-1_3.

[bib.bib27] [27] Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Methods Comput. Sci., 3(4), 2007. doi:10.2168/LMCS-3(4:11)2007.

[bib.bib28] [28] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137–161, 1985. doi:10.1145/2455.2460.

[bib.bib29] [29] Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859–879, 2015. doi:10.1016/j.jcss.2014.12.005.

[bib.bib30] [30] Manisha Jain, Alexandre Madeira, and Manuel A. Martins. A fuzzy modal logic for fuzzy transition systems. In Amy P. Felty and João Marcos, editors, Logical and Semantic Frameworks with Applications, LSFA 2019, volume 348 of ENTCS, pages 85–103. Elsevier, 2019. doi:10.1016/j.entcs.2020.02.006.

[bib.bib31] [31] Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. Log. Methods Comput. Sci., 12(4), 2016. doi:10.2168/LMCS-12(4:10)2016.

[bib.bib32] [32] Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke, Jurriaan Rot, and Ichiro Hasuo. Expressivity of quantitative modal logics : Categorical foundations via codensity and approximation. In Logic in Computer Science, LICS 2021, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470656.

[bib.bib33] [33] Barbara König and Christina Mika-Michalski. (metric) bisimulation games and real-valued modal logics for coalgebras. In Sven Schewe and Lijun Zhang, editors, Concurrency Theory, CONCUR 2018, volume 118 of LIPIcs, pages 37:1–37:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.CONCUR.2018.37.

[bib.bib34] [34] Clemens Kupke and Jurriaan Rot. Expressive logics for coinductive predicates. Log. Methods Comput. Sci., 17(4), 2021. doi:10.46298/lmcs-17(4:19)2021.

[bib.bib35] [35] F. E. J. Linton. Some aspects of equational categories. In S. Eilenberg, D. K. Harrison, S. MacLane, and H. Röhrl, editors, Proceedings of the Conference on Categorical Algebra, pages 84–94. Springer, 1966. doi:10.1007/978-3-642-99902-4_3.

[bib.bib36] [36] Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Logic in Computer Science, LICS 2016, pages 700–709. ACM, 2016. doi:10.1145/2933575.2934518.

[bib.bib37] [37] Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. In Lawrence S. Moss and Pawel Sobocinski, editors, Algebra and Coalgebra in Computer Science, CALCO 2015, volume 35 of LIPIcs, pages 253–269. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPIcs.CALCO.2015.253.

[bib.bib38] [38] Haiyu Pan, Yongming Li, Yongzhi Cao, and Zhanyou Ma. Model checking computation tree logic over finite lattices. Theor. Comput. Sci., 612:45–62, 2016. doi:10.1016/j.tcs.2015.10.014.

[bib.bib39] [39] Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19–33, 2004. doi:10.1305/NDJFL/1094155277.

[bib.bib40] [40] Amgad Rady and Franck van Breugel. Explainability of probabilistic bisimilarity distances for labelled Markov chains. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2023, volume 13992 of LNCS, pages 285–307. Springer, 2023. doi:10.1007/978-3-031-30829-1_14.

[bib.bib41] [41] Jurriaan Rot, Bart Jacobs, and Paul Blain Levy. Steps and traces. J. Log. Comput., 31(6):1482–1525, 2021. doi:10.1093/logcom/exab050.

[bib.bib42] [42] Jan J. M. M. Rutten. Relators and metric bisimulations. In Bart Jacobs, Larry Moss, Horst Reichel, and Jan J. M. M. Rutten, editors, Coalgebraic Methods in Computer Science, CMCS 1998, volume 11 of ENTCS, pages 252–258. Elsevier, 1998. doi:10.1016/S1571-0661(04)00063-5.

[bib.bib43] [43] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.

[bib.bib44] [44] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390(2-3):230–247, 2008. doi:10.1016/j.tcs.2007.09.023.

[bib.bib45] [45] Lutz Schröder and Dirk Pattinson. Description logics and fuzzy probability. In Toby Walsh, editor, International Joint Conference on Artificial Intelligence, IJCAI 2011, pages 1075–1081. IJCAI/AAAI, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-184.

[bib.bib46] [46] Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115–142, 2005. doi:10.1016/j.tcs.2004.09.035.

[bib.bib47] [47] Rob J. van Glabbeek. The linear time - branching time spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3–99. North-Holland/Elsevier, 2001. doi:10.1016/b978-044482830-9/50019-9.

[bib.bib48] [48] Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov and Laura Kovács, editors, Concurrency Theory, CONCUR 2020, volume 171 of LIPIcs, pages 27:1–27:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.27.

[bib.bib49] [49] Paul Wild and Lutz Schröder. A quantified coalgebraic van Benthem theorem. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, FOSSACS 2021, volume 12650 of LNCS, pages 551–571. Springer, 2021. doi:10.1007/978-3-030-71995-1_28.

[bib.bib50] [50] Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci., 18(2), 2022. doi:10.46298/lmcs-18(2:19)2022.

[bib.bib51] [51] Paul Wild, Lutz Schröder, Dirk Pattinson, and Barbara König. A van Benthem theorem for fuzzy modal logic. In Anuj Dawar and Erich Grädel, editors, Logic in Computer Science, LICS 2018, pages 909–918. ACM, 2018. doi:10.1145/3209108.3209180.

[bib.bib52] [52] Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Explaining behavioural inequivalence generically in quasilinear time. In Serge Haddad and Daniele Varacca, editors, Concurrency Theory, CONCUR 2021, volume 203 of LIPIcs, pages 32:1–32:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.32.

[bib.bib53] [53] James Worrell. Coinduction for recursive data types: partial orders, metric spaces and omega-categories. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 337–356. Elsevier, 2000. doi:10.1016/S1571-0661(05)80356-1.

[bib.bib54] [54] Hengyang Wu, Taolue Chen, Tingting Han, and Yixiang Chen. Bisimulations for fuzzy transition systems revisited. Int. J. Approx. Reason., 99:1–11, 2018. doi:10.1016/j.ijar.2018.04.010.

[bib.bib55] [55] Hengyang Wu, Yixiang Chen, Tian-Ming Bu, and Yuxin Deng. Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems. Fuzzy Sets Syst., 333:106–123, 2018. doi:10.1016/j.fss.2017.02.008.