key: cord-0060363-upg37bop
authors: Wild, Paul; Schröder, Lutz
title: A Quantified Coalgebraic van Benthem Theorem
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_28
sha: 14d17dc882c7828d9bf62b510b5e223d48e6979d
doc_id: 60363
cord_uid: upg37bop

The classical van Benthem theorem characterizes modal logic as the bisimulation-invariant fragment of first-order logic; put differently, modal logic is as expressive as full first-order logic on bisimulation-invariant properties. This result has recently been extended to two flavours of quantitative modal logic, viz. fuzzy modal logic and probabilistic modal logic. In both cases, the quantitative van Benthem theorem states that every formula in the respective quantitative variant of first-order logic that is bisimulation-invariant, in the sense of being nonexpansive w.r.t. behavioural distance, can be approximated by quantitative modal formulae of bounded rank. In the present paper, we unify and generalize these results in three directions: We lift them to full coalgebraic generality, thus covering a wide range of system types including, besides fuzzy and probabilistic transition systems as in the existing examples, e.g. also metric transition systems; and we generalize from real-valued to quantale-valued behavioural distances, e.g. nondeterministic behavioural distances on metric transition systems; and we remove the symmetry assumption on behavioural distances, thus covering also quantitative notions of simulation.

Modal logic takes part of its popularity from the fact that it specifies transition systems at what for many purposes may be regarded as the right level of granularity; that is, it is invariant under the standard process-theoretic notion of bisimulation in the sense that bisimilar states satisfy the same modal formulae. There are two quite different well-known converses to this elementary property, which both witness the expressiveness of modal logic: By the Hennessy-Milner theorem [29] , states in finitely branching systems that satisfy the same modal formulae are bisimilar, and by the van Benthem theorem, every first-order definable bisimulation-invariant property is expressible by a modal formula. Since modal logic embeds into first-order logic, the latter result may be phrased as saying that modal logic is the bisimulation-invariant fragment of first-order logic.

In the two-valued setting, there has been increased recent interest in variants and generalizations of this result (e.g. [54, 14, 52, 22, 55, 1] ) For quantitative systems, it has long been realized (e.g. [26, 15, 10] ) that quantitative notions of process equivalence, generally referred to as behavioural metrics (although they are in general only pseudometrics, as distinct but equivalent states have distance zero), are often more appropriate than two-valued bisimilarity. In particular, while two-valued notions of process equivalence just flag small deviations between systems as inequivalence, behavioural metrics can provide more fine-grained information on the degree of similarity of systems. Behavioural metrics are correspondingly used, e.g., in verification [25] , differential privacy [13] , and conformance testing of hybrid systems [36] .

In the same way that two-valued modal logic constitutes a natural specification language for two-valued transition systems, quantitative systems correlate to quantitative modal logics. In this context, bisimulation invariance is read as nonexpansiveness w.r.t. behavioural distance, i.e. two states differ on a modal formula at most by their behavioural distance; we refer to this property as behavioural nonexpansiveness. Notably, van Breugel and Worrell [10] prove a Hennessy-Milner type theorem for a quantitative probabilistic modal logic: They show that on compact state spaces, the formulae of the logic lie dense in the space of behaviourally nonexpansive state properties, which implies that behavioural distance and logical distance coincide.

In the present paper, we are mainly interested in the other converse to behavioural nonexpansiveness, i.e. in quantitative van Benthem theorems. In previous work with Pattinson and König, we have established such theorems for quantitative modal logics of fuzzy [57] and probabilistic [58] transition systems. In the quantitative setting, these theorems take the form of approximability properties, and state that every behaviourally nonexpansive quantitative firstorder property is approximable by quantitative modal formulae of bounded rank. The latter qualification is in fact the key content of the respective theoremswithout it, approximability is closer in flavour to Hennessy-Milner-type theorems, which apply to arbitrary rather than just first-order definable properties (although one should note additionally that our van Benthem theorems do not assume compactness of the state space).

Our present contribution is to unify and generalize these results in three directions: First, we allow for full coalgebraic generality, i.e. we cover system types subsumed under the paradigm of universal coalgebra [49] . Besides the fuzzy and probabilistic systems featuring in the previous concrete instances of our result, this includes a wide range of weighted, game-based, and preferential systems; for illustration, we concentrate on the (comparatively simple) case of metric transition systems [3, 20] in the presentation. Second, we generalize from real-valued to quantale-valued metrics (e.g. [24, 33] ). Using the unit interval quantale, we recover our previous results on real-valued logics as special cases. Beyond this, quantales in particular provide support for what may be termed metrics with effects; we illustrate this on a notion of convex-nondeterministic behavioural distance on metric transition systems, where the behavioural distance gives an interval of possible real-valued distances. Lastly, we remove the assumption that distances need to be symmetric, so that we cover also notions of quantitative simulation. At this level of generality, we prove both a Hennessy-Milner type theorem stating coincidence of logical and behavioural distance, effectively generalizing the existing coalgebraic quantitative Hennessy-Milner theorem [37] to quantale-valued distances; and, as our main result, a quantitative van Benthem theorem stating that all behaviourally non-expansive first-order properties can be modally approximated in bounded rank.

Related Work There is a substantial body of work on two-valued modal characterization theorems, e.g. for logics with frame conditions [14] , coalgebraic modal logics [52] , fragments of XPath [12, 22, 1] , neighbourhood logic [28] , modal logic with team semantics [38] , modal µ-calculi (within monadic second order logics) [35, 19] , PDL (within weak chain logic) [11] , modal first-order logics [6, 54] , and two-dimensional modal logics with an S5-modality [55] . We are not aware of quantitative modal characterization theorems other than the mentioned ones for fuzzy and probabilistic modal logics [57, 58] . Prior to the quantitative Hennessy-Milner theorems mentioned above [10, 37] , Hennessy-Milner theorems have been established for two-valued logics and two-valued bisimilarity over quantitative systems, e.g. on probabilistic transition systems [39, 16, 17] . There is work on Hennessy-Milner theorems for certain Heyting-valued modal logics [21, 18] ; since Heyting algebras are quantales but often fail to meet a continuity assumption needed in our generic Hennessy-Milner theorem, we do not claim to subsume these results.

We briefly recall basic definitions and examples on quantales and universal coalgebra, and fix some data needed throughout the paper. We need some elementary category theory, see, e.g., [2] .

Quantales are order-algebraic structures that serve as objects of truth values in suitable multi-valued logics, and also support a useful notion of generalized (pseudo-)metric space (e.g. [24, 33, 32] ). Our arguments will rely on a certain amount of epsilontics, and hence require more specifically the use of value quantales [24] .

We recall some basic order and lattice theory. A complete lattice is a partially ordered set (V, ≤) having all suprema A for A ⊆ V , equivalently all infima A. We denote binary meets and joins by ∧ and ∨, respectively. Given x, y ∈ V , we say that x is well above y, and write x y, if whenever y ≥ A for some A ⊆ V , then x ≥ a for some a ∈ A. A complete lattice (V, ≤) is completely distributive if all joins in V distribute over all meets, equivalently all meets distribute over all joins [46] . Another equivalent characterization is that (V, ≤) is completely distributive iff

for every y ∈ V [47] .

In the definition of value quantale, we follow Flagg [24] in dualizing the usual continuity condition for quantales in order to avoid having to reverse the order when moving between the general development and basic examples such as the unit interval; deviating from his terminology, we emphasize this by the prefix 'co-': Definition 2.1 ((Value) co-quantales). A (commutative) co-quantale V is a complete lattice (V, ≤) equipped with a commutative monoid structure (0, ⊕) that is meet-continuous:

A co-quantale V is a value co-quantale [24] if 0 is the bottom element of V and moreover (V, ≤) is a value distributive lattice, i.e. a completely distributive complete lattice such that |V | > 1 and for all x, y ∈ V , x, y 0 implies x∧y 0. Correspondingly, we denote the greatest element of V by 1.

(Dually, in a quantale the operation ⊕ is required to be join-continuous.) By meet-continuity, we obtain a further binary operator on a co-quantale V by adjunction, defined by

The operator is sometimes called the internal hom of V [7] . Moreover, in a value co-quantale, we have that for each ε 0, there exists δ 0 such that 2 · δ := δ ⊕ δ ≤ ε [24, Theorem 2.9]. This allows for proofs where an error bound ε 0 needs to be split up into multiple smaller parts.

A simple example of a value co-quantale is the unit interval [0, 1] with the usual ordering, with truncated addition a ⊕ b = min(a + b, 1) as the monoid structure. Correspondingly, the operation is truncated subtraction a b = max(a−b, 0). We have a b iff a > b. We will give further examples in Section 3.

Universal Coalgebra serves as a unified framework for many types of statebased systems [49] , such as nondeterministic, probabilistic, alternating, gamebased, or weighted systems. It is based on encapsulating the system type as a functor T , for our purposes on the category Set of sets and functions; such a T assigns to each set X a set T X, thought of as a type of structured collections over X, and to each map f : X → Y a map T f : T X → T Y , respecting identities and composition. A T -coalgebra (A, α) consists of a set A of states and a transition map α : A → T A, thought of as assigning to each state a structured collection of successors. Taking T to be the covariant powerset functor P, which assigns to each set X its powerset PX, we obtain relational transition systems as T -coalgebras. As a further example, the (discrete) subdistribution functor S assigns to each set X the set SX of discrete probability subdistributions µ on X (i.e. µ(X 0 ) = µ(X) ≤ 1 for some countable subset X 0 ⊆ X), and to each map

S-coalgebras are probabilistic transition systems (or Markov chains) with possible deadlock: They assign to each state a subdistribution over possible successor states, with the gap of the total probability to 1 interpreted as the probability of deadlock. Additional instances are seen in Example 4.4. For the remainder of the paper, we fix a set functor T and require that T ∅ is nonempty (hence our use of subdistributions instead of distributions in the examples). Moreover, we require w.l.o.g. that T is standard, i.e. preserves subset inclusions [5] .

A V-valued relation between sets A and B is a map R : A × B → V , which we also denote by R : A → + B. For fixed A and B, we order the V-valued relations between A and B pointwise:

We compose relations R : A→ + B and S : B → + C using the monoid operation on V:

Given a function f : A → B and ε ∈ V , the ε-graph Gr ε,f is the relation

We also write Gr f = Gr 0,f and, in case of the identity function, ∆ ε,X = Gr ε,id X and ∆ X = ∆ 0,X . The dual of (X, d) is the V-continuity space (X, d * ) where d * (x, y) = d(y, x). The symmetrization of (X, d) is the space (X, d s ) with d s (x, y) = d(x, y) ∨ d * (x, y). We say that (X, d) is symmetric if d = d * .

Remark 3.2. Recall that omission of the metric symmetry axiom d(x, y) = d(y, x) is standardly designated by the prefix 'quasi-' and omission of the antisymmetry axiom d(x, y) = 0 ⇒ x = y by the prefix 'pseudo-'; thus, continuity spaces could be termed generalized pseudo-quasimetric spaces, and symmetric continuity spaces generalized pseudometric spaces.

For any set A, the supremum distance between V-valued maps f, g :

).

The usual notion of nonexpansive map generalizes as expected:

for all x, y ∈ X. We denote the space of nonexpansive maps between (X, d 1 ) and

Ultimately we are interested in defining and reasoning about behavioural distances. Generally speaking, a behavioural distance is a V-continuity space defined on the carrier of a T -coalgebra α : A → T A in such a way that the behaviour defined by the coalgebra map α is incorporated into the distance values of states in A. This is accomplished using relation liftings, which lift V-valued relations giving distances between states to those giving distances between successor structures of states. We specifically generalize the notion of nonexpansive lax extension [56] to the quantale-valued case:

and satisfies the following axioms:

(The notion of lax extension, given by axioms (L1)-(L3), is standard, e.g. [31] ; the axiom (L4), introduced in [56], guarantees nonexpansiveness w.r.t. the supremum metric as shown in Lemma 3.6.)

Lemma 3.6. If L is a nonexpansive lax extension of T , then L is in fact nonexpansive w.r.t. the supremum metric. That is, for R 1 ,

For technical purposes, we will be interested in a generalized version of total boundedness (recall that a standard metric space is compact iff it is complete and totally bounded):

≤ ε} for the (symmetric) ball of radius ε around x ∈ X. A finite ε-cover of (X, d) is a choice of finitely many

We say that (X, d) is totally bounded if X has a finite ε-cover for each ε 0.

Remark 3.8. Note that use of the symmetrization d s is essential in the above definition; e.g. in the unit interval, with d(x, y) = x y, the set {y | d(0, y) ≤ ε} is the whole space, so 0 alone would form an ε-cover of [0, 1] if we replaced d s with d.

Moreover, our main result involves a generalization of the standard notion of density:

Assumption 3.10. Throughout the paper, we fix a value co-quantale V that is totally bounded as a V-continuity space. Moreover, we fix a dense subset V 0 ⊆ V for use as a set of truth constants in the relevant logics, with a view to keeping the syntax countable in the central examples. (The technical development, on the other hand, does not require V 0 to be countable, so we can always take

Example 3.11 ((Value) co-quantales).

1. The set 2 = {0, 1}, with 0 ≤ 1 and with binary join as the monoid structure, is a value co-quantale [24] , and of course totally bounded. 2-Continuities d are just preorders, with y being above x if d(x, y) = 0 (!); symmetric 2continuities are equivalence relations. Notice that 0 0 in 2. The operator is given by a b = 1 iff a = 1 and b = 0.

2. The dual of every locale (e.g. [8] ), in particular the set of closed subsets of any topological space, forms a co-quantale, with binary join as the monoid structure. However, locales are not in general value co-quantales. The dual Ω(R) of the free locale over a set R, described as the lattice of downclosed systems of finite subsets of R (ordered by reverse inclusion of such set systems), does form a value co-quantale [24] , and is totally bounded [30] . Ω(R)-continuity spaces are known as structure spaces [30, 24] .

3. The unit interval [0, 1] is totally bounded. [0, 1]-Continuity spaces coincide with 1-bounded pseudo-quasimetric spaces, and symmetric [0, 1]-continuity spaces with 1-bounded pseudometric spaces in the standard sense (cf. Remark 3.2).

4. Convex-nondeterministic distances: The set I of nonempty closed subintervals (i.e. finitely generated nonempty convex subsets) of [0, 1], written in the

, again with on [0, 1] described as in the previous item. We can think of an I-continuity space as assigning to each pair of points a nondeterministic distance, given as an interval of possible distances.

We next introduce the main objects of study, quantale-valued coalgebraic modal and predicate logics. They will feature modalities interpreted using a quantitative version of predicate liftings [45, 50, 51] . Predicate liftings take their name from the fact that they lift predicates on a base set X to predicates on the set T X (where T is our globally fixed functor representing the system type according to Section 2). We work with V-valued predicates, which are organized in the contravariant V-powerset functor Q given on sets X by QX = X → V and on

Set op is the opposite category of Set). In keeping with the prevalent reading in fuzzy and probabilistic logics (where, typically, V = [0, 1]), we read 0 ∈ V as 'false' and 1 ∈ V as 'true' (opposite choices are also found in the literature, e.g. in modal logics for metric transition systems [3] , where 0 ∈ [0, 1] is interpreted as 'true'). Predicate liftings can have arbitrary finite arities [50] . For brevity, we restrict the presentation to unary modalities and predicate liftings; generalizing to higher arities requires only more indexing.

. For the remainder of the paper, we fix a set Λ of monotone and nonexpansive predicate liftings, which, by abuse of notation, we also use as modalities in the syntax. A basic example is the ♦ modality of quantitative probabilistic modal logic [10] , which denotes expected probability (in the next transition step) and corresponds to a predicate lifting for the (sub-)distribution functor S (Section 2); see Example 4.4.2 for details. The generic syntax of (V-valued) quantitative coalgebraic modal logic is then given by the grammar

The operators ⊕, , ∨, ∧ denote co-quantale operations, the meaning of λ is determined by the associated predicate lifting. As usual, the rank of a formula ϕ is the maximal nesting depth of modalities λ in ϕ. We denote the set of all modal formulae by L Λ and the set of formulae of rank at most n by L Λ n . Formally, the semantics is defined by assigning to each formula ϕ and each T -coalgebra α : A → T A the extension ϕ α : A → V , or just ϕ , of ϕ over α, recursively defined by

c (a) = c λϕ (a) = λ A ( ϕ )(α(a)) Remark 4.3. Fuzzy logics differ widely in their interpretation of propositional connectives (e.g [41] ). In our modal syntax, we necessarily restrict to nonexpansive operations, in order to ensure nonexpansiveness w.r.t. behavioural distance later; this is typical of characteristic logics for behavioural distances (such as quantitative probabilistic modal logic [10] ). The logic hence does not include binary ⊕ or (in the above syntax, we insist that one of the arguments is a constant). In terminology usually applied to V = [0, 1], we thus allow Zadeh connectives (such as ∨, ∧) but not Lukasiewicz connectives, so for V = [0, 1], the above version of quantitative coalgebraic modal logic is essentially the Zadeh fragment of Lukasiewicz fuzzy coalgebraic modal logic [51] .

The syntax does not include negation 1 (−); if V satisfies the De Morgan laws (e.g. these hold in [0, 1]), Λ is closed under duals 1 (λ(1 (−))), and V 0 is closed under negation (i.e. c ∈ V 0 implies 1 c ∈ V 0 ), then negation can be defined via negation normal forms as usual.

As the ambient predicate logic of the above modal logic, we use (V-valued) quantitative coalgebraic predicate logic, a quantitative variant of two-valued coalgebraic predicate logic [40] . Its syntax is given by

where c ∈ V 0 , λ ∈ Λ, and x, y come from a fixed supply Var of (individual) variables. The reading of xλ y : ϕ is the modalized truth degree (according to λ) to which the successors y of a state x satisfy ϕ; e.g. with ♦ as above, x♦ y : ϕ is the expected truth value of ϕ at a random successor y of x. The semantics over (A, α) as above is given by V-valued maps ϕ α , or just ϕ , that are defined on valuations κ : Var → A. The interesting clauses in the definition are

xλ y : ϕ (κ) = λ A ( ϕ (κ[y → · ]))(α(κ(x))) (where κ[y → a] maps y to a and otherwise behaves like κ, and by ϕ (κ[y → · ]) we mean the predicate that maps a to ϕ (κ[y → a])). Moreover, equality is crisp, i.e. x = y (κ) is 1 if κ(x) = κ(y), and 0 otherwise.

We discuss some instances of the above framework.

1. Fuzzy modal logic: Take T to be the covariant V-valued powerset functor,

Then T -coalgebras are equivalent to fuzzy Kripke frames, which consist of a set X and a fuzzy relation R : X × X → V , and ♦ is the natural fuzzification of the standard diamond modality. Fuzzy propositional atoms from a set At can be added by passing to the functor that maps a set X to Q(At) × T X. Instantiating to V = [0, 1], we obtain a basic modal logic of fuzzy relations, or in description logic terminology Zadeh fuzzy ALC [53] . The corresponding instance of quantitative coalgebraic predicate logic is essentially the Zadeh fragment of Novak's Lukasiewicz fuzzy first order logic [43] .

2. Probabilistic modal logic: As indicated in Section 2, coalgebras for the subdistribution functor S are probabilistic transition systems (with possible deadlock). We take V = [0, 1] and Λ = {♦}, interpreted by the predicate lifting

where E µ (A) denotes the expected value of A(x) when x is distributed according to µ. The induced instance of quantitative coalgebraic modal logic is (quantitative) probabilistic modal logic [10] , which may be seen as a quantitative variant of two-valued probabilistic modal logic [39] , and embeds into the probabilistic µcalculus [34, 42] . Propositional atoms are treated analogously as in the previous item (and indeed probabilistic modal logic is trivial without them). The ambient quantitative probabilistic first-order logic arising as the corresponding instance of quantitative coalgebraic predicate logic is a quantitative variant of Halpern's type-1 (i.e. statistical) probabilistic first-order logic [27] . 3. Metric modal logic: In their simplest form, metric transition systems [3] are just transition systems in which states are labelled in a metric space S (numerous variants exist, e.g. with states themselves forming a metric space or with transitions labelled in a metric space [9] ). We work with a generalized version where (S, d S ) is a V-continuity space. Metric transition systems are then coalgebras for the functor T X given on sets by T X = S × PX. We take Λ = {♦} ∪ S. We interpret Λ using predicate liftings

for A ∈ QX, (s, B) ∈ T X, r ∈ S. Note that r ∈ S ignores its argument A, so is effectively a nullary modality. Note also that as per our interpretation of truth values, this nullary modality is read as distinctness from r; in case V = [0, 1], the degree of equality to r can be expressed as 1 r. The induced instance of coalgebraic modal logic is related to characteristic logics for branching-time behavioural distances on metric transition systems [3, 9] . 4. Convex-nondeterministic metric modal logic: We continue to consider metric transition systems as recalled in the previous item, reusing the designators T, S, d S , and taking V = [0, 1] for simplicity. Recall the value co-quantale I of nonempty closed subintervals of [0, 1] from Example 3.11.4. We turn the predicate liftings for r ∈ S defined in the previous item into I-valued predicate liftings by prolonging them along the inclusion ι : 

The behavioural distance between states of a coalgebra α : A → T A is defined as a least fixpoint that arises from an iterative process: Initially, at depth 0, all states are thought of as equivalent and their distance is therefore 0. In order to increase the depth of the behavioural distance from n to n + 1, we lift the depth-n distance on A to a the set T A of successor structures. Formally, this is accomplished using the following quantale-valued version of the coalgebraic Kantorovich lifting [4, 56] :

Definition 5.1 (Kantorovich lifting). Let A and B be sets and R : A → + B. R(x, y) ).

2. For probabilistic modal logic (Example 4.4.2), the restriction of K Λ to distributions coincides, by definition, with the usual (symmetric) Kantorovich-Wasserstein lifting (e.g. [10] ). On subdistributions, one obtains an asymmetric variant, whose symmetrization then coincides with the standard one. (R(x, y) ), x∈A y∈B π 2 (R(x, y)) ] on (s, A) ∈ T X = S × P(X), (t, B) ∈ T Y , and R : X → + Y (recall that the π i are the projections I → [0, 1], and ι : [0, 1] → I denotes the evident injection).

For purposes of lifting V-continuity structures as relations, nonexpansive pairs can be replaced with the more familiar notion of nonexpansive map: (a, b) . Then f ≤ h ≤ g and h ∈ Pred(A, d).

By monotonicity of predicate liftings we get the following alternative formulation for the Kantorovich lifting of a V-continuity structure:

Using the Kantorovich lifting, we can now define a sequence of behavioural distances between states a, b in a T -coalgebras α : A → T A, β : B → T B:

By general fixed point theory, the continuation of this ordinal-indexed sequence past ω eventually stabilizes, that is, there exists some ordinal γ such that d K γ+1 = d K γ . The arising least fixed point is the unbounded behavioural distance d K , alternatively given by

These behavioural distances lead to an appropriate generalization of the notion of bisimulation invariance. A family f of V-valued predicates f α indexed over T -coalgebras α : A → T A -such as the extension of a modal formula or of a first-order formula with a single free variable -is said to be behaviourally nonexpansive if it is nonexpansive with respect to behavioural distance d K , i.e. if for all coalgebras α :

Similarly, f is depth-n behaviourally nonexpansive for finite depth n if f is nonexpansive with respect to depth-n behavioural distance d K n . To match these notions to the classical setting, consider the binary coquantale 2. In the general case, the above notion of behavioural nonexpansiveness should then be thought of as preservation under simulation: States a, b have (asymmetric) distance 0 if b simulates a, and in this case, (1) stipulates that if f is true at a, then f is also true at b. Example 5.6. The behavioural distance arising from the Kantorovich lifting of metric modal logic (Example 5.3.3) is a simulation distance. The value d K (a, b) quantifies the degree to which traces starting at b simulate traces starting at a, where the distance from one trace to another is the supremum over the distances at all time steps.

On the other hand, there are many cases where the behavioural distance d K is symmetric. If V = [0, 1] and the set Λ is closed under duals (Remark 4.3), then we have that K Λ (R * ) = K Λ (R) * for all R and therefore d K is symmetric [56] . In these symmetric cases distance 0 determines a notion of bi similarity, and behavioural nonexpansiveness amounts to the standard notion of bisimulation invariance. Thus, the following straightforward lemma generalizes both bisimulation invariance of modal logic and preservation of positive modal logic (with only diamond modalities) under simulation: Lemma 5.7. All modal formulae are behaviourally nonexpansive, and all modal formulae of rank at most n are depth-n behaviourally nonexpansive.

As expected, coalgebra morphisms preserve behaviour on the nose:

Another way to define distances between states of a coalgebra is in terms of the modal formulae: Definition 5.9 (Logical distance). Let a, b be states in coalgebras α : A → T A, β : B → T B. We define

The relationship between fixpoint-based distances d K and logical distances d L is at the heart of the study of behavioural nonexpansiveness and modal expressiveness. For instance, Lemma 5.7 can equivalently be expressed by the inequalities d L ≤ d K and d L n ≤ d K n , n < ω. In Section 6, we investigate the converse inequalities.

We now establish our first contribution, a quantitative coalgebraic Hennessy-Milner theorem. To this end, we first need to pin down the exact relationship of the two families of distances at finite depth. Theorem 6.1. Let the set Λ of monotone and nonexpansive predicate liftings from Section 4 be finite and let (A, α) be a coalgebra. For all n < ω:

1. We have d K n = d L n =: d n 2. The space (A, d n ) is totally bounded. 3. The set L Λ n is a dense subset of Pred(A, d).

Remark 6.2. The need for assuming that the set Λ of modalities is finite is specific to quantitative Hennessy-Milner theorems (and implicitly present also in the existing [0, 1]-valued version of the theorem [37] ), and not needed in the two-valued case [45, 50] . It relates to the total boundedness claim in Theorem 6.1, and features also in the van Benthem theorem, where in fact it is needed also in the two-valued case [52] ; indeed, proofs of the original van Benthem theorem start by assuming, in that case w.l.o.g., that there are only finitely many propositional atoms and relational modalities. In our running examples, only the ones featuring metric transition systems are affected by this assumption; indeed, for our theorems to apply to such systems, the space of labels needs to be finite.

Theorem 6.1 is proven by induction on n and most of Section 6 is devoted to the inductive step (the base case n = 0 is immediate from d K 0 = d L 0 = 0). We fix a coalgebra α : A → T A and an integer n > 1 and assume as the inductive hypothesis that the three items of Theorem 6.1 have already been proven for all m < n. We show Item 1 in Lemma 6.3, Item 2 in Lemma 6.6, and Item 3 in Lemma 6.7. Lemma 6.3. We have d K n = d L n on A.

Proof (sketch). We use the alternative formula for the Kantorovich lifting as given in Lemma 5.5. By Item 3 of the inductive hypothesis, and because the predicate liftings are nonexpansive, the maps λ(f ) • α with f ∈ Pred(A, d n−1 ) can be approximated using formula expansions λψ with ψ ∈ L Λ n−1 .

Having shown that d K n = d L n , from now on we simply use d n to denote both. To show that d n is totally bounded, we make use of the following version of the Arzelà-Ascoli theorem [23, Theorem 4.13] .

Lemma 6.4 (Arzelà-Ascoli). Let (X, d 1 ) and (Y, d 2 ) be totally bounded Vcontinuity spaces. Then the space (X, d 1 ) → 1 (Y, d 2 ) is also totally bounded.

Using Lemma 6.4, we show that the Kantorovich lifting preserves total boundedness; this generalizes a previous result for the case V = [0, 1] [37, Proposition 29] , which in turn generalizes [57, Lemma 5.6 ].

Lemma 6.5. If the set Λ of predicate liftings is finite and (X, d) is a totally bounded V-continuity space, then (T X, K Λ (d)) is totally bounded.

The following is now an easy consequence: Lemma 6.6. The space (A, d n ) is totally bounded.

Finally, we show that the modal formulae up to depth n form a dense subspace of the space of all nonexpansive properties: Lemma 6.7. Let f ∈ Pred(A, d n ) be a nonexpansive map and let ε 0. Then there exists some modal formula ϕ ∈ L Λ n such that d ∨,s V (f, ϕ ) ≤ ε.

Proof (sketch). We use the fact that for all x, y ∈ A

The latter term can be approximated using formulae of L Λ n , where the infimum over y and the supremum over γ are made finite using ε-covers of A and L Λ n .

Having shown that behavioural distance and logical distance coincide at all finite depths, we are now equipped to prove our first main result, a version of the Hennessy-Milner theorem stating that behavioural distance and logical distance coincide not only at finite depths (Theorem 6.1.1), but in fact also at unbounded depth. In general, this equivalence of distances can only be expected to hold if the functor T in question is finitary, or admits approximation by a finitary subfunctor [56] . The functor T is finitary if for all sets X and all t ∈ T X there exists a finite subset Y ⊆ X such that t = T i(s) for some s ∈ T Y , where i : Y → X is set inclusion. Examples of finitary functors include the finite powerset functor P ω X = {Y ⊆ X | Y finite} and the finite subdistribution functor S ω which maps a set X to the set of finitely supported probability subdistributions on X. König and Mika-Michalski [37] prove a quantitative coalgebraic Hennessy-Milner theorem for the case of the co-quantale [0, 1]. We generalize their result as follows:

Definition 6.8. We say that the value co-quantale V is continuous from below if for every monotone increasing sequence (a n ) n<ω in V and every ε 0, there exists some n such that a n ⊕ ε ≥ n<ω a n .

This condition essentially allows the use of epsilontic arguments also for joins of increasing sequences, while value co-quantales in general allow this only for meets. It holds in all our running examples. Theorem 6.9 (Quantified Hennessy-Milner theorem). Let Λ be a finite set of monotone and nonexpansive predicate liftings, let T be a finitary functor and let V be a totally bounded value co-quantale that is continuous from below. Then we have d K = d L .

Proof (sketch). Because V is continuous from below, we have K Λ (d K ω ) = n<ω K Λ (d K n ) on finite sets, and as T is finitary, this also holds for all sets. This implies that d K ω = d K ω+1 = d K , so that

Besides examples already covered by the [0, 1]-valued version of the theorem [37] , this result instantiates, e.g., to a quantitative Hennessy-Milner theorem for convex-nondeterministic metric modal logic (Example 4.4.4).

We proceed to establish our main result, the quantitative coalgebraic van Benthem theorem. The main tool in the proof of this result is a notion of locality, which characterizes formulae that only depend on the structure of the model in some neighbourhood of the state under consideration. This poses a challenge when it comes to coalgebraic models, as these need not come with a built-in graph structure that could be used to define what it means for two states to be neighbouring. To solve this, we make use of a technique based on supported coalgebras that has previously been used in the proof of a two-valued coalgebraic van Benthem theorem [52] .

Recall from Section 2 that we assume T ∅ = ∅. We fix an element ⊥ ∈ T ∅, and for each set A put ⊥ A = T i(⊥), where i : ∅ → A is the empty map.

Definition 7.1 (Support). Let A be a set. We say that a set B ⊆ A is a support of t ∈ T A if t ∈ T B. A supported coalgebra is a coalgebra α : A → T A together with a map supp α : A → PA such that supp α (a) is a support of α(a) for every a ∈ A.

Every coalgebra can be supported because we can always put supp α (a) = A for all a ∈ A. Supporting a coalgebra equips it with a graph structure: Definition 7.2 (Neighbourhood). Let A = (A, α, supp α ) be a supported coalgebra.

1. The Gaifman graph of A is the undirected graph with vertex set A and edge set {{a, b} | b ∈ supp α (a)}. 2. For any a, b ∈ A, the Gaifman distance D supp (a, b) is the least number of steps to get from a to b in the Gaifman graph (or ∞, if no path from a to b exists). 3. The radius-k neighbourhood of a state a ∈ A is the set U k (a) = {b ∈ A | D supp (a, b) ≤ k}.

For any k < ω and any state a in a supported coalgebra A = (A, α, supp α ), we can define a supported coalgebra A k a = (U k (a), α k , supp α k ) on the radiusk neighbourhood of a. The coalgebra map α k : U k (a) → T (U k (a)) is given by

We note that the latter case only occurs for states on the edge of U k (a), that is when D supp (a, b) = k. Note that ⊥ A has empty support by construction, so that we can put supp α k (b) = ∅ in this latter case and supp α k (b) = supp α (b) otherwise.

Using the neighbourhood around a state and the coalgebra structure defined on it, we can now define our notion of locality: A key step in the proof is the following locality result, which in similar form appears also in proofs of the classical van Benthem theorem [44] , and is proved, in our case, by a game-theoretic method that is related to classical Ehrenfeucht-Fraïssé games:

Lemma 7.5. Let ϕ(x) be a behaviourally nonexpansive formula with qr(ϕ) ≤ n.

Then ϕ is k-local for k = 3 n .

Proof (sketch). Consider a spoiler-duplicator game over n rounds, where both players place a pebble every round and the second player needs to maintain the invariant that if there are m rounds remaining the radius 3 m neighbourhoods around the pebbles need to be isomorphic. One can show that this invariant guarantees equivalence on formulae of rank at most m. We use this game to prove for every supported coalgebra A that ϕ has the same value on A and A k a . Nonexpansiveness of ϕ is used to extend the two coalgebras in such a way that the duplicator always has a suitable response.

We next show that every nonexpansive formula that is local is also nonexpansive at some finite depth. We make use of an unravelling construction, where a coalgebra is enlarged so that the successors of every state in the unravelling (as given by the support relation) form a tree.

Definition 7.6 (Unravelling). The unravelling of a supported coalgebra A = (A, α, supp α ) is the supported coalgebra A * = (A + , α * , supp α * ), where A + is the set of nonempty sequences over A and for a 1 . . . a n ∈ A + we have α (a 1 . . . a n ) = T f (α(a n )) and supp α * (a 1 . . . a n ) = f [supp α (a n )], where f : A → A + , a → a 1 . . . a n a. The mentioned nonexpansiveness at finite depth follows: Lemma 7.8. Let ϕ be behaviourally nonexpansive and k-local. Then ϕ is also depth-k behaviourally nonexpansive.

Proof (sketch). By the assumptions on ϕ we may pass from any supported coalgebra to the radius-k neighbourhood in the unravelling, which is shaped like a tree of depth k. Between any two such tree structures we have d K k = d K , as their behaviour past depth k is fully characterized by the default value ⊥ ∈ T ∅.

The target result then follows by combining the above lemmas with Theorem 6.1 and a final chain argument that allows us to detach the technical development from the choice of a fixed coalgebra: Theorem 7.9 (Quantified van Benthem theorem). Let Λ be a finite set of monotone and nonexpansive predicate liftings, let T be a standard functor with T ∅ = ∅, and let V be a totally bounded value co-quantale. Then for every behaviourally nonexpansive formula ϕ of quantitative coalgebraic predicate logic with quantifier rank at most n and every ε 0 there exists a modal formula ψ ∈ L Λ such that for all coalgebras α : A → T A and all a ∈ A, d s V ( ϕ α (a), ψ α (a)) ≤ ε and the modal rank of ψ is bounded by 3 n .

Proof (sketch). Using the final chain (T n 1) n<ω , where 1 is a singleton set, we can construct a coalgebra (Z, ζ) such that for all (A, α) and all ϕ, ψ we have d ∨,s V ( ϕ α , ψ α ) ≤ d ∨,s V ( ϕ ζ , ψ ζ ). As ϕ is behaviourally nonexpansive, we get that it is also depth-k behaviourally nonexpansive for k = 3 qr(ϕ) by Lemmas 7.5 and 7.8, and by Theorem 6.1.3 for every ε 0 there is ψ ∈ L Λ k such that d ∨,s V ( ϕ ζ , ψ ζ ) ≤ ε.

To our best knowledge, the only previously known instances of this result in the real-valued setting are the ones for [0, 1]-valued fuzzy modal logic [57] and for quantitative probabilistic modal logic [58] . In the two-valued setting, we cover a previous coalgebraic van Benthem result [52] by instantiating to V = 2, and in fact obtain an additional asymmetric version, characterizing fragments that are preserved under simulation. 

We have established a highly general quantitative version of van Benthem's modal characterization theorem, stating that given a value quantale V that is totally bounded and continuous from below, all state properties, in a given type of quantitative systems, that are nonexpansive w.r.t. V-valued behavioural distance and expressible in V-valued coalgebraic (first-order) predicate logic can be approximated by V-valued modal formulae of bounded rank. A key technical tool in the proof are versions of the classical Arzela-Ascoli and Stone-Weierstraß theorems for totally bounded quantale-valued (pseudo-quasi-)metric spaces. Coalgebraic generality implies that this result not only subsumes existing quantitative van-Benthem type theorems for fuzzy [57] and probabilistic [58] systems, but we also obtain new results, e.g. for metric transition systems. Via the additional parametrization over a value quantale, we moreover obtain, e.g., a van Benthem theorem for convex-nondeterministic behavioural distance ('states x, y have distance between a and b') on metric transition systems. Our result complements previous coalgebraic results for two-valued logics [52] . We do leave some open problems, in particular to determine whether the main result can be sharpened to exact modal expressibility instead of approximability, and to obtain a quantitative modal characterization over finite models, in generalization of Rosen's finite-model variant of van Benthem's theorem [48] .

Model theory of XPath on data trees. Part II: Binary bisimulation and definability

available as Reprints Theory Appl

Linear and branching system metrics

Coalgebraic behavioral metrics

Terminal coalgebras in well-founded set theory

Handbook of Philosophical Logic

Relation lifting, with an application to the many-valued cover modality

Handbook of Categorical Algebra

A behavioural pseudometric for metric labelled transition systems

A behavioural pseudometric for probabilistic transition systems

PDL is the bisimulation-invariant fragment of weak chain logic

Some modal aspects of XPath

Generalized bisimulation metrics

Modal characterisation theorems over special classes of frames

Metrics for labelled Markov processes

Bisimulation for labelled markov processes

Stochastic Coalgebraic Logic

Notions of bisimulation for Heytingvalued modal languages

Monadic second-order logic and bisimulation invariance for coalgebras

The quantitative linear-time-branchingtime spectrum

Fuzzy bisimulation for Gödel modal logic

Model theory of XPath on data trees. Part I: Bisimulation and characterization

Continuity spaces: Reconciling domains and metric spaces

Quantales and continuity spaces

Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances

Algebraic reasoning for probabilistic concurrent systems

An analysis of first-order logics of probability

Neighbourhood structures: Bisimilarity and basic model theory

Algebraic laws for non-determinism and concurrency

A general theory of structure spaces with applications to spaces of prime ideals

Topological theories and closed objects

Probabilistic metric spaces as enriched categories

Approximation in quantale-enriched categories

Quantitative analysis and model checking

Automata for the modal µ-calculus and related results

Notions of conformance testing for cyber-physical systems: Overview and roadmap

Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras

A van Benthem theorem for modal team semantics

Bisimulation through probabilistic testing

Coalgebraic predicate logic

Managing uncertainty and vagueness in description logics for the semantic web

A probabilistic temporal calculus based on expectations

First-order fuzzy logic

Elementary proof of the van Benthem-Rosen characterisation theorem

Expressive logics for coalgebras via terminal sequence induction

Completely distributive complete lattices

A subdirect-union representation for completely distributive complete lattices

Modal logic over finite structures

Universal coalgebra: A theory of systems

Expressivity of coalgebraic modal logic: The limits and beyond. Theoret

Description logics and fuzzy probability

A van Benthem/Rosen theorem for coalgebraic predicate logic

A fuzzy description logic

First-order expressivity for S5-models: Modal vs. two-sorted languages

A characterization theorem for a modal description logic

Characteristic logics for behavioural metrics via fuzzy lax extensions

A van Benthem theorem for fuzzy modal logic

A modal characterization theorem for a probabilistic fuzzy description logic

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use

Acknowledgements We wish to thank Barbara König for valuable discussions.