Uli Fahrenberg

Jan Křetínský

Axel Legay

Louis-Marie Traonouez

Compositionality for Quantitative Specifications

We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.

Introduction

Specifications of systems come in two main flavors. Logical specifications are formalized as formulae of modal or temporal logics, such as the modal µ-calculus or LTL. A common way to verify them on a system is to translate them to automata and then analyze the composition of the system and the automaton. In contrast, in the behavioral approach, specifications are given, from the very beginning, in an automata-like formalism. Such properties can be verified using various equivalences and preorders, such as bisimilarity or refinement. Here This paper is based on the conference contribution [START_REF] Fahrenberg | Compositionality for quantitative specifications[END_REF] we focus on the latter approach, but also show connections between the two.

Behavioral formalisms are particularly apt for component-based design. Indeed, specifications can be easily composed as well as separately refined into more concrete ones. The behavioral formalisms we work with here are modal transition systems (MTS) [START_REF] Kim | A modal process logic[END_REF] and their extensions. MTS are like automata, but with two types of transitions: must-transitions represent behavior that has to be present in every implementation; may-transitions represent behavior that is allowed, but not required to be implemented.

A simple example of a vending machine specification, in Fig. 1, describes that any correct implementation must be ready to accept money, then may offer the customer to choose extras and must issue a beverage. While the must-transitions are preserved in the refinement process, the may-transitions can be either implemented and turned into must-transitions, or dropped. work [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Bauer | Weighted modal transition systems[END_REF] Fig. 4 A disjunctive modal transition system νX. [grant, idle, work]X∧

[req]νY.[idle, req]ff ∧ work [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Bauer | Weighted modal transition systems[END_REF] Y ∨ grant [0,5] X Fig. 5 The ν-calculus translation of the DMTS in Fig. 4 This low-level refinement process is, however, insufficient when the designer wants to get more specific about the implemented actions, such as going from the coarse specification just described to the more finegrained specification of Fig. 2. In order to relate such specifications, MTS with structured labels have been introduced [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]. Given a preorder on labels, relating for instance coffee beverage, we can refine a transition label into one which is below, for example implement "beverage" with its refinement "coffee".

This framework can be applied to various preorders. For example, one can use labels with a discrete component carrying the action information and an interval component to model time duration or energy consumption. As an example, consider the simple real-time property in Fig. 3: "after a req(uest), grant has to be executed within 5 time units without the process being idle meanwhile". The transition (grant, [0,[START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]) could be safely refined to (grant, [l, r]) for any 0 ≤ l ≤ r ≤ 5.

We proceed to identify several shortcomings of the current approaches.

Expressive power. The current theory of structured labels [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF][START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF] is available only for the basic MTS. Very often one needs to use richer structures such as disjunctive MTS (DMTS) [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF][START_REF] Kim | Equation solving using modal transition systems[END_REF] or acceptance automata [START_REF] Hennessy | Acceptance trees[END_REF][START_REF] Raclet | Residual for component specifications[END_REF]. While MTS generally cannot express disjunction of properties, DMTS and further related formalisms can and are, in fact, equivalent to the modal ν-calculus [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF].

This allows, for instance, to prohibit deadlocks as in the example in Fig. 4. The disjunctive must, depicted as a branching arrow, requires at least one of the tran- work [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF][START_REF] Bauer | Extending modal transition systems with structured labels[END_REF] Fig. 7 Another DMTS specification sitions to be present. Thus we allow the deadline for grant to be reset if additional work is generated. Note that specifying grant and work as two separate musttransitions would not allow postponing the deadline; and two separate may-transitions would not guarantee any progress, as none of them has to be implemented. We hence propose DMTS with structured labels and also extend the equivalence between DMTS and the modal ν-calculus [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF] to our setting. Figure 5 shows a νcalculus translation of the DMTS in Fig. 4.

Robustness. Consider again the request-grant example in Fig. 4, together with the two labeled transition systems in Fig. 6. While i 1 , issuing grant after precisely 5 time units, is a valid implementation of x, if there is but a small positive drift in the timing, like in i 2 , it is not an implementation anymore. However, this drift might be easily mended or just might be due to measuring errors.

Therefore, when models and specifications contain such quantitative information, the standard Boolean notions of satisfaction and refinement are of limited utility [START_REF] Henzinger | The embedded systems design challenge[END_REF][START_REF] Sifakis | A vision for computer science -the system perspective[END_REF] and should be replaced by notions which are more robust to perturbations. For another example, the DMTS of Fig. 7 is not a refinement of the one in Fig. 4, but for all practical purposes, it is rather close.

One approach to robustness is to employ metric distances instead of Boolean relations; this has been done for example in [18-20, 25, 35, 45, 53, 54, 58, 59] and many other papers. An advantage of behavioral specification formalisms is that models and specifications are closely related, hence distances between models can easily be extended to distances between specifications. We have developed a distance-based approach for MTS in [START_REF] Bauer | Weighted modal transition systems[END_REF][START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF] and shown in [START_REF] Fahrenberg | Generalized quantitative analysis of metric transition systems[END_REF][START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF][START_REF] Fahrenberg | The quantitative lineartime-branching-time spectrum[END_REF] that a good general setting is given by recursively specified trace distances on an abstract quantale. Here we extend this to DMTS.

Compositionality. The framework should be compositional. In the quantitative setting, this in essence means that the operations we define on the systems should behave well with respect not only to satisfaction, but also to the distances. For instance, if s 1 is close to t 1 and s 2 close to t 2 , then also the structural composition s 1 s 2 should be close to t 1 t 2 . We prove this for the usual operations; in particular, we give a construction for such a well-behaved quotient.

The quotient of s by t is the most general specification that, when composed with t, refines s. This operation is thus useful for computing missing parts of a system to be implemented, when we already have several components at our disposal. The construction is complex already in the non-quantitative setting [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] and the extension of the algorithm to structured labels is non-trivial.

Our contribution. To sum up, we extend the framework of structured labels to DMTS and the modal ν-calculus. We equip this framework with distances and give constructions for the structured analogues of the standard operations, so that they behave compositionally with respect to the distances.

Further related work. Refinement of components is a frequently used design approach in various areas, ranging from subtyping [START_REF] Liskov | A behavioral notion of subtyping[END_REF] over the Java modeling language JML [START_REF] Jacobs | A logic for the Java modeling language JML[END_REF] or correct-by-design class diagram operations [START_REF] Fahrenberg | Sound merging and differencing for class diagrams[END_REF] to interface theories close to MTS such as interface automata [START_REF] De Alfaro | Interface automata[END_REF] based on alternating simulation. A variant of alternating simulation called covariantcontravariant simulation has been compared to MTS modal refinement in [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF]. The graphical representability of these variants was studied in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Boudol | Graphical versus logical specifications[END_REF].

Quantitative specifications have been introduced in other settings. At first, the focus was on probabilities [START_REF] Huth | Quantitative analysis and model checking[END_REF][START_REF] Mio | Probabilistic modal mu-calculus with independent product[END_REF][START_REF] Morgan | A probabilistic temporal calculus based on expectations[END_REF], but later, predicates with values in arbitrary metric spaces were also introduced [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF]. Robustness of probabilistic specifications is considered in [START_REF] De | Quantitative verification and control via the mu-calculus[END_REF][START_REF] Luca De Alfaro | Model checking discounted temporal properties[END_REF][START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF]. It is our hope that the close relationship between quantitative DMTS and the quantitative modal ν-calculus which we expose in this paper will aid in the development of theory and tools also for probabilistic specifications.

There are a number of extensions of MTS specifically designed for coping with real-time properties: the timed input-output specifications of [START_REF] David | Realtime specifications[END_REF], the timed interfaces of [START_REF] Luca De Alfaro | Timed interfaces[END_REF], and the modal event-clock specifications of [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF]. Robustness for timed input-output specifications is considered in [START_REF] Kim | Robust specification of real time components[END_REF][START_REF] Kim | Robust synthesis for real-time systems[END_REF][START_REF] Traonouez | A parametric counterexample refinement approach for robust timed specifications[END_REF]. With only little extra work, our notions of distances and robustness can be applied to real-time specifications, see [START_REF] Fahrenberg | A robust specification theory for modal event-clock automata[END_REF] for modal event-clock specifications. Some other extensions of MTS have been developed for probabilistic properties: the constraint Markov chains of [START_REF] Caillaud | Constraint Markov chains[END_REF][START_REF] Delahaye | Consistency and refinement for interval Markov chains[END_REF][START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] and the abstract probabilistic automata of [START_REF] Caillaud | Constraint Markov chains[END_REF]. Distances for such specifications are used in [START_REF] Delahaye | Refinement and difference for probabilistic automata[END_REF], but no work on robustness is available.

Structured Labels

Let Σ be a poset with partial order . We think of as label refinement, so that if a b, then a is less permissive (more restricted) than b.

We say that a label a ∈ Σ is an implementation label if b a implies b = a for all b ∈ Σ, i.e., if a cannot be further refined. The set of implementation labels is denoted Γ , and for a ∈ Σ, we let a = {b ∈ Γ | b a} denote the set of its implementations. Note that a b implies a ⊆ b for all a, b ∈ Σ.

Example 1 A trivial but important example of our label structure is the discrete one in which label refinement is equality (and Γ = Σ). This is equivalent to the "standard" case of unstructured labels.

A typical label set in quantitative applications consists of a discrete component and real-valued weights. For specifications, weights are replaced by (closed) weight intervals, so that

Σ = U × {[l, r] | l ∈ R ∪ {-∞}, r ∈ R∪{∞}, l ≤ r} for a finite set U , cf. [4,5]. Label refine- ment is given by (u 1 , [l 1 , r 1 ]) (u 2 , [l 2 , r 2 ]) iff u 1 = u 2 and [l 1 , r 1 ] ⊆ [l 2 , r 2 ]
, so that labels are more refined if they specify smaller intervals; thus,

Γ = U × {[x, x] | x ∈ R} ≈ U × R.
For a quite general setting, we can instead start with an arbitrary set Γ of implementation labels, let Σ = 2 Γ , the powerset, and = ⊆ be subset inclusion. Then a = a for all a ∈ Σ. (Hence we identify implementation labels with one-element subsets of Σ.)

Label operations

Specification theories come equipped with several standard operations that make compositional software design possible [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]: conjunction for merging viewpoints covering different system's aspects [START_REF] Ben-David | Merging partial behaviour models with different vocabularies[END_REF][START_REF] Uchitel | Merging partial behavioural models[END_REF], structural composition for running components in parallel, and quotient to synthesize missing parts of systems [START_REF] Kim | Equation solving using modal transition systems[END_REF]. In order to provide them for DMTS, we first need the respective atomic operations on their action labels.

We hence assume that Σ comes equipped with a partial conjunction, i.e., an operator : Σ × Σ Σ for which it holds that (1) if a 1 a 2 is defined, then a 1 a 2 a 1 and a 1 a 2 a 2 , and (2) if a 3 a 1 and a 3 a 2 , then a 1 a 2 is defined and a 3 a 1 a 2 .

Note that by these properties, any two partial conjunctions on Σ have to agree on elements for which they are both defined.

Example 2 For discrete labels, the unique conjunction operator is given by

a 1 a 2 = a 1 if a 1 = a 2 ,
undef. otherwise .

Indeed, by property (2), a 1 a 2 must be defined for a 1 = a 2 , and by [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF], if a 1 a 2 = a 3 is defined, then a 3 = a 1 and a 3 = a 2 .

For labels in

U × {[l, r] | l, r ∈ R, l ≤ r}, the unique conjunction is (u 1 , [l 1 , r 1 ]) (u 2 , [l 2 , r 2 ]) = undef. if u 1 = u 2 or [l 1 , r 1 ] ∩ [l 2 , r 2 ] = ∅ , (u 1 , [l 1 , r 1 ] ∩ [l 2 , r 2 ]) otherwise .
To see uniqueness, let

a i = (u i , [l i , r i ]) for i = 1, 2, 3.
Using property (2), we see that a 1 a 2 must be defined when u 1 = u 2 and [l 1 , r 1 ] ∩ [l 2 , r 2 ] = ∅, and by (2), if a 1 a 2 = a 3 is defined, then u 3 = u 1 and u 3 = u 2 , and

[l 3 , r 3 ] ⊆ [l 1 , r 1 ], [l 3 , r 3 ] ⊆ [l 2 , r 2 ] imply [l 1 , r 1 ]∩[l 2 , r 2 ] = ∅.
Finally, for the case of specification labels as sets of implementation labels, the unique conjunction is a 1 a 2 = a 1 ∩ a 2 .

For structural composition and quotient of specifications, we assume a partial label synchronization operator : Σ × Σ Σ which specifies how to compose labels. We assume to be associative and commutative, with the following technical property which we shall need later: For all a 1 , a

2 , b 1 , b 2 ∈ Σ with a 1 a 2 and b 1 b 2 , a 1 b 1 is defined iff a 2 b 2 is, and if both are defined, then a 1 b 1 a 2 b 2 .
Example 3 For discrete labels, the conjunction of Example 2 is the same as CSP-style composition, i.e., a b = a if a = b and undefined otherwise, but other compositions can easily be defined.

For labels in U × {[l, r] | l, r ∈ R, l ≤ r}, several useful label synchronization operators may be defined for different applications. One is given by addition of intervals, i.e.,

(u 1 , [l 1 , r 1 ]) + (u 2 , [l 2 , r 2 ]) = undef. if u 1 = u 2 , (u 1 , [l 1 + l 2 , r 1 + r 2 ]) otherwise ,
for example modeling computation time of actions on a single processor. Another operator, useful in scheduling, uses maximum instead of addition:

(u 1 , [l 1 , r 1 ]) max (u 2 , [l 2 , r 2 ]) = undef. if u 1 = u 2 , (u 1 , [max(l 1 , l 2 ), max(r 1 , r 2 )]) otherwise .
For set-valued specification labels, we may take any synchronization operator given on implementation labels Γ and lift it to one on Σ by a

1 a 2 = {b 1 b 2 | b 1 ∈ a 1 , b 2 ∈ a 2 }.

Specification Formalisms

In this section we introduce the specification formalisms which we use in the rest of the paper. The universe of models for our specifications is the one of standard labeled transition systems. For simplicity of exposition, we work only with finite specifications and implementations, but most of our results extend to the infinite (but finitely branching) case.

A labeled transition system (LTS) is a structure I = (S, s 0 , -→) consisting of a finite set S of states, an initial state s 0 ∈ S, and a transition relation -→ ⊆ S × Γ ×S. We usually write s a -→ t instead of (s, a, t) ∈ -→. Note that transitions are labeled with implementation labels.

Disjunctive Modal Transition Systems

A disjunctive modal transition system (DMTS) is a structure D = (S, S 0 , , -→) consisting of finite sets S ⊇ S 0 of states and initial states, respectively, may-transitions ⊆ S×Σ×S, and disjunctive must-transitions -→ ⊆ S × 2 Σ×S . It is assumed that for all (s, N ) ∈ -→ and (a, t) ∈ N there is (s, b, t) ∈ with a b.

Example 4

The specification x in Fig. 5 has a maytransition to y; from there we have a disjunctive musttransition with identical underlying may-transitions. The intuitive meaning of the transition, that either grant or work must be available, is formalized below using the modal refinement.

Note that we allow multiple (or zero) initial states. We write s a t instead of (s, a, t) ∈ and s -→ N instead of (s, N ) ∈ -→. A DMTS (S, S 0 , , -→) is an implementation if ⊆ S ×Γ ×S, -→ = {(s, {(a, t)}) | s a t}, and S 0 = {s 0 } is a singleton; DMTS implementations are hence isomorphic to LTS.

DMTS were introduced in [START_REF] Kim | Equation solving using modal transition systems[END_REF] in the context of equation solving, or quotient of specifications by processes and are used e.g., in [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF] for LTL model checking. They are a natural extension of modal transition systems [START_REF] Kim | A modal process logic[END_REF], which are DMTS in which all disjunctive must-transitions s -→ N lead to singletons N = {(a, t)}; in fact, DMTS are the closure of MTS under quotient [START_REF] Kim | Equation solving using modal transition systems[END_REF].

We introduce a notion of modal refinement of DMTS with structured labels. For discrete labels, it coincides with the classical definition [START_REF] Kim | Equation solving using modal transition systems[END_REF].

Definition 1 Let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ) and D 2 = (S 2 , S 0 2 , 2 , -→ 2 ) be DMTS. A relation R ⊆ S 1 × S 2 is a modal refinement if it holds for all (s 1 , s 2 ) ∈ R that -for all s 1 a1 1 t
∈ S 0 1 there is s 0 2 ∈ S 0 2 for which (s 0 1 , s 0 2 ) ∈ R.
Note that this definition degrades to the one of [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF][START_REF] Kim | Equation solving using modal transition systems[END_REF] for discrete labels (cf. Example 1).

We write

D 1 ≡ m D 2 if D 1 ≤ m D 2 and D 2 ≤ m D 1 . The implementation semantics of a DMTS D is D = {I ≤ m D | I implementation}.
This is, thus, the set of all LTS which satisfy the specification given by the DMTS D. We say that D 1 thoroughly refines D 2 , and write

D 1 ≤ th D 2 , if D 1 ⊆ D 2 .
The below proposition, which follows directly from transitivity of modal refinement, shows that modal refinement is sound with respect to thorough refinement; in the context of specification theories, this is what one would expect. It can be shown that modal refinement is also complete for deterministic DMTS [START_REF] Beneš | On determinism in modal transition systems[END_REF], but we will not need this here.

Proposition 1 For all DMTS D 1 , D 2 , D 1 ≤ m D 2 im- plies D 1 ≤ th D 2 .

Acceptance automata

A non-deterministic acceptance automaton (NAA) is a structure A = (S, S 0 , Tran), with S ⊇ S 0 finite sets of states and initial states and Tran : S → 2 2 Σ×S an assignment of transition constraints. The intuition is that a transition constraint Tran(s) = {M 1 , . . . , M n } specifies a disjunction of n choices M 1 , . . . , M n as to which transitions from s have to be implemented.

An NAA is an implementation if S 0 = {s 0 } is a singleton and it holds for all s ∈ S that Tran(s) = {M } ⊆ 2 Γ ×S is a singleton; hence NAA implementations are isomorphic to LTS. Acceptance automata were first introduced in [START_REF] Raclet | Residual for component specifications[END_REF], based on the notion of acceptance trees in [START_REF] Hennessy | Acceptance trees[END_REF]; however, there they are restricted to be deterministic. We employ no such restriction here.

Let

A 1 = (S 1 , S 0 1 , Tran 1 ) and A 2 = (S 2 , S 0 2 , Tran 2 ) be NAA. A relation R ⊆ S 1 × S 2 is a modal refinement if it holds for all (s 1 , s 2 ) ∈ R and all M 1 ∈ Tran 1 (s 1 ) that there exists M 2 ∈ Tran 2 (s 2 ) such that ∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 : a 1 a 2 , (t 1 , t 2 ) ∈ R , ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 : a 1 a 2 , (t 1 , t 2 ) ∈ R . (1)
The definition reduces to the one of [START_REF] Raclet | Residual for component specifications[END_REF] in case labels are discrete. We will write

M 1 R M 2 if M 1 , M 2 , R satisfy (1).
In [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF], translations were discovered between DMTS and NAA. For a DMTS D = (S, S 0 , , -→) and s ∈ S, let Tran(s

) = {M ⊆ Σ × S | ∀(a, t) ∈ M : s a t, ∀s -→ N : N ∩ M = ∅} and define the NAA da(D) = (S, S 0 , Tran). For an NAA A = (S, S 0 , Tran), define the DMTS ad(A) = (D, D 0 , , -→) by D = {M ∈ Tran(s) | s ∈ S} , D 0 = {M 0 ∈ Tran(s 0 ) | s 0 ∈ S 0 } , -→ = M, {(a, M ) | M ∈ Tran(t)} (a, t) ∈ M , = {(M, a, M ) | ∃M -→ N : (a, M ) ∈ N } .
Similarly to a theorem of [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF], we can now show the following:

Theorem 1 For all DMTS D 1 , D 2 and NAA A 1 , A 2 , D 1 ≤ m D 2 iff da(D 1 ) ≤ m da(D 2 ) and A 1 ≤ m A 2 iff ad(A 1 ) ≤ m ad(A 2 ).
This structural equivalence will allow us to freely translate forth and back between DMTS and NAA in the rest of the paper. Note, however, that the state spaces of A and ad(A) are not the same; the one of ad(A) may be exponentially larger. [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF] shows that this blow-up is unavoidable.

From a practical point of view, DMTS are a somewhat more useful specification formalism than NAA. This is because they are usually more compact and easily drawn and due to their close relation to the modal ν-calculus, see below.

The Modal ν-Calculus

In [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF], translations were discovered between DMTS and the modal ν-calculus, and refining the translations in [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF], we could show that for discrete labels, these formalisms are structurally equivalent. We use the representation of the modal ν-calculus by equation systems in Hennessy-Milner logic developed in [START_REF] Kim | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF].

For a finite set X of variables, let H(X) be the set of Hennessy-Milner formulae, generated by the abstract syntax H(X) φ ::

= tt | ff | x | a φ | [a]φ | φ ∧ φ | φ ∨ φ, for a ∈ Σ and x ∈ X. A ν-calculus expression is a structure N = (X, X 0 , ∆), with X 0 ⊆ X sets of variables and ∆ : X → H(X) a declaration.
We recall the greatest fixed point semantics of νcalculus expressions from [START_REF] Kim | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF], but extend it to structured labels. Let (S, S 0 , -→) be an LTS, then an assignment is a mapping σ : X → 2 S . The set of assignments forms a complete lattice with order σ 1 σ 2 iff σ 1 (x) ⊆ σ 2 (x) for all x ∈ X and lowest upper bound

i∈I σ i (x) = i∈I σ i (x).
The semantics of a formula in H(X) is a function from assignments to subsets of S defined as follows:

tt σ = S, ff σ = ∅, x σ = σ(x), φ ∧ ψ σ = φ σ ∩ ψ σ, φ ∨ ψ σ = φ σ ∪ ψ σ, and
a φ σ = {s ∈ S | ∃s b -→ t : b ∈ a , t ∈ φ σ}, [a]φ σ = {s ∈ S | ∀s b -→ t : b ∈ a =⇒ t ∈ φ σ}.
The semantics of a declaration ∆ is then the assignment defined by ∆ = {σ : X → 2 S | ∀x ∈ X : σ(x) ⊆ ∆(x) σ}; the greatest (pre)fixed point of ∆.

An LTS I = (S, s 0 , -→) implements (or models) the expression N , denoted I |= N , if there is x 0 ∈ X 0 such that s 0 ∈ ∆ (x 0 ).

In [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF] we have introduced another semantics for ν-calculus expressions, which is given by a notion of refinement, like for DMTS and NAA. For this we need a normal form for ν-calculus expressions:

Lemma 1 ([32]) For any ν-calculus expression N 1 = (X 1 , X 0 1 , ∆ 1 ), there exists another N 2 = (X 2 , X 0 2 , ∆ 2 ) with N 1 = N 2 and such that for any x ∈ X, ∆ 2 (x) is of the form ∆ 2 (x) = i∈I j∈Ji a ij x ij ∧ a∈Σ [a] j∈Ja y a,j
for finite (possibly empty) index sets I, J i , J a and all x ij , y a,j ∈ X 2 .

As this is a type of conjunctive normal form, it is clear that translating a ν-calculus expression into normal form may incur an exponential blow-up. We introduce some notation for ν-calculus expressions in normal form. Let N = (X, X 0 , ∆) be such an expression and x ∈ X, with

∆(x) = i∈I j∈Ji a ij x ij ∧ a∈Σ [a] j∈Ja y a,j as in the lemma. Define ♦(x) = {{(a ij , x ij ) | j ∈ J i } | i ∈ I} and, for each a ∈ Σ, a (x) = {y a,j | j ∈ J a }. Intuitively, ♦(x)
collects all a -requirements from x, whereas a (x) specifies the disjunction of [a]-properties which must hold from x. Note that now,

∆(x) = N ∈♦(x) (a,y)∈N a y ∧ a∈Σ [a] y∈ a (x) y . (2) Let N 1 = (X 1 , X 0 1 , ∆ 1 ), N 2 = (X 2 , X 0 2 , ∆ 2 ) be ν- calculus expressions in normal form and R ⊆ X 1 × X 2 . The relation R is a modal refinement if it holds for all (x 1 , x 2 ) ∈ R that -for all a 1 ∈ Σ and y 1 ∈ a1 1 (x 1 ) there is a 2 ∈ Σ and y 2 ∈ a2 2 (x 2 )
with a 1 a 2 and (y 1 , y 2 ) ∈ R, and for all

N 2 ∈ ♦ 2 (x 2 ) there is N 1 ∈ ♦ 1 (x 1 ) such that
for all (a 1 , y 1 ) ∈ N 1 there exists (a 2 , y 2 ) ∈ N 2 with a 1 a 2 and (y 1 , y 2 ) ∈ R.

We say that a ν-calculus expression (X,

X 0 , ∆) in normal form is an implementation if X 0 = {x 0 } is a singleton, ♦(x) = {{(a, y)} | y ∈ a (x), a ∈ Σ} and a (x) = ∅ for all a / ∈ Γ , for all x ∈ X.
We can translate a LTS (S, S 0 , -→) to a ν-calculus expression (S, S 0 , ∆) in normal form by setting

♦(s) = {{(a, t)} | s a -→ t} and a (s) = {t | s a -→
t} for all s ∈ S, a ∈ Σ. This defines a bijection between LTS and ν-calculus implementations, hence, like for DMTS and NAA, an embedding of LTS into ν-calculus.

One of the main results of [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF] is that for discrete labels, the refinement semantics and the fixed point semantics of the modal ν-calculus agree; the proof can easily be extended to our case of structured labels: For a ν-calculus expression N = (X, X 0 , ∆) in normal form, let

= {(x, a, y) ∈ X × Σ × X | y ∈ a (x)}, -→ = {(x, N ) | x ∈ X, N ∈ ♦(x)} and define the DMTS nd(N ) = (X, X 0 , , -→).
Given that these translations are entirely syntactic, the following theorem is not a surprise:

Theorem 3 For DMTS D 1 , D 2 and ν-calculus expres- sions N 1 , N 2 , D 1 ≤ m D 2 iff dn(D 1 ) ≤ m dn(D 2 ) and N 1 ≤ m N 2 iff nd(N 1 ) ≤ m nd(N 2 ).

Specification theory

Structural specifications typically come equipped with operations which permit compositional reasoning, viz. conjunction, structural composition, and quotient, cf. [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF].

On deterministic MTS, these operations can be given easily using simple structural operational rules (for such semantics of weighted systems, see for instance [START_REF] Klin | Structural operational semantics for stochastic and weighted transition systems[END_REF]). For non-deterministic specifications this is significantly harder; in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] it is shown that DMTS and NAA permit these operations and, additionally but trivially, disjunction. Here we show how to extend these operations on non-deterministic systems to our quantitative setting with structured labels.

We remark that structural composition and quotient operators are well-known from some logics, such as, e.g., linear [START_REF] Girard | Linear logic[END_REF] or spatial logic [START_REF] Caires | A spatial logic for concurrency (part I)[END_REF], and were extended to quite general contexts [START_REF] Cardelli | Modular Markovian logic[END_REF]. However, whereas these operators are part of the formal syntax in those logics, for us they are simply operations on logical expressions (or DMTS, or NAA). Consequently [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF], structural composition is generally only a sound over-approximation of the semantic composition.

Given the equivalence of DMTS, NAA and the modal ν-calculus exposed in the previous section, we will often state properties for all three types of specifications at the same time, letting S stand for any of the three types.

Disjunction and conjunction

Disjunction of specifications is easily defined, as we allow for multiple initial states. For two DMTS D

1 = (S 1 , S 0 1 , 1 , -→ 1 ) and D 2 = (S 2 , S 0 2 , 2 , -→ 2 ), we can hence define D 1 ∨ D 2 = (S 1 ∪ S 2 , S 0 1 ∪ S 0 2 , 1 ∪ 2 , -→ 1 ∪ -→ 2 ) (with all unions disjoint). For conjunction, we let D 1 ∧ D 2 = (S 1 × S 2 , S 0 1 × S 0 2 , , -→), with -(s 1 , s 2 ) a1 a2 (t 1 , t 2 ) whenever s 1 a1 1 t 1 , s 2 a2 2 t 2 and a 1 a 2 is defined, -for all s 1 -→ N 1 , (s 1 , s 2 ) -→ {(a 1 a 2 , (t 1 , t 2 )) | (a 1 , t 1 ) ∈ N 1 , s 2 a2 2 t 2 , a 1 a 2 defined}, -for all s 2 -→ N 2 , (s 1 , s 2 ) -→ {(a 1 a 2 , (t 1 , t 2 )) | (a 2 , t 2 ) ∈ N 2 , s 1 a1 1 t 1 , a 1 a 2 defined}.
Theorem 4 For all specifications S 1 , S 2 , S 3 ,

-S 1 ∨ S 2 ≤ m S 3 iff S 1 ≤ m S 3 and S 2 ≤ m S 3 , -S 1 ≤ m S 2 ∧ S 3 iff S 1 ≤ m S 2 and S 1 ≤ m S 3 , -S 1 ∨ S 2 = S 1 ∪ S 2 , and S 1 ∧ S 2 = S 1 ∩ S 2 . Proof The proof that S 1 ∨ S 2 ≤ m S 3 iff S 1 ≤ m S 3 and S 2 ≤ m S 3 is trivial: any modal refinement R ⊆ (S 1 ∪ S 2 ) × S 3 splits into two refinements R 1 ⊆ S 1 × S 3 , R 2 ⊆ S 2 × S 3 and vice versa.
For the proof of the second claim, which we show for DMTS, we prove the back direction first. Let Assume that (s 2 , s 3 ) -→ N . Without loss of generality we can assume that there is

R 2 ⊆ S 1 × S 2 , R 3 ⊆ S 1 × S 3 be initialized (DMTS) modal refinements and define R = {(s 1 , (s 2 , s 3 )) | (s 1 , s 2 ) ∈ R 2 , (s 1 , s 3 ) ∈ R 3 } ⊆ S 1 × (S 2 × S 3 ). Then R is initial- ized. Now let (s 1 , (s 2 , s 3 )) ∈ R, then (s 1 , s 2 ) ∈ R 2 and (s 1 , s 3 ) ∈ R 3 . Assume that s 1 a1 1 t 1 , then by S 1 ≤ m S 2 ,
s 2 -→ 2 N 2 such that N = {(a 2 a 3 , (t 2 , t 3 )) | (a 2 , t 2 ) ∈ N 2 , s 3 a3 3 t 3 }. By S 1 ≤ m S 2 , we have s 1 -→ 1 N 1 such that ∀(a 1 , t 1 ) ∈ N 1 : ∃(a 2 , t 2 ) ∈ N 2 : a 1 a 2 , (t 1 , t 2 ) ∈ R 2 .
Let (a 1 , t 1 ) ∈ N 1 , then also s 1 a1 1 t 1 , so by S 1 ≤ m S 3 , there is s 3 a3 3 t 3 with a 1 a 3 and (t 1 , t 3 ) ∈ R 3 . By the above, we also have (a 2 , t 2 ) ∈ N 2 such that a 1 a 2 and (t 1 , t 2 ) ∈ R 2 , but then (a 2 a 3 , (t 2 , t 3 )) ∈ N , a 1 a 2 ∧ a 3 , and (t 1 , (t 2 , t 3 )) ∈ R.

For the other direction of the second claim, let R ⊆ S 1 × (S 2 × S 3 ) be an initialized (DMTS) modal refinement. We show that S 1 ≤ m S 2 , the proof of

S 1 ≤ m S 3 being entirely analogous. Define R 2 = {(s 1 , s 2 ) | ∃s 3 ∈ S 3 : (s 1 , (s 2 , s 3 )) ∈ R} ⊆ S 1 × S 2 , then R 2 is initialized. Let (s 1 , s 2 ) ∈ R 2 , then we must have s 3 ∈ S 3 such that (s 1 , (s 2 , s 3 )) ∈ R. Assume that s 1 a1 1 t 1 , then also (s 2 , s 3 )
a (t 2 , t 3 ) for some a with a 1 a and (t 1 , (t 2 , t 3 )) ∈ R. By construction we have s 2 a2 2 t 2 and s 3 a3 3 t 3 such that a = a 2 a 3 , but then a 1 a 2 a 3 a 2 and (t 1 , t 2 ) ∈ R 2 .

Assume that s 2 -→ 2 N 2 , then by construction we have (s

2 , s 3 ) -→ N = {(a 2 a 3 , (t 2 , t 3 )) | (a 2 , t 2 ) ∈ N 2 , s 3 a3 3 t 3 }. By S 1 ≤ m S 2 ∧ S 3 , there is s 1 -→ 1 N 1 such that ∀(a 1 , t 1 ) ∈ N 1 : ∃(a, (t 2 , t 3 )) ∈ N : a 1 a, (t 1 , (t 2 , t 3 )) ∈ R.
Let (a 1 , t 1 ) ∈ N 1 , then we have (a, (t 2 , t 3 )) ∈ N for which a 1 a and (t 1 , (t 2 , t 3 )) ∈ R. By construction of N , this implies that there are (a 2 , t 2 ) ∈ N 2 and s 3

a3 3 t 3 such that a = a 2 a 3 , but then a 1 a 2 a 3 a 2 and (t 1 , t 2 ) ∈ R.
As to the last claims of the theorem, S 1 ∧ S 2 = S 1 ∩ S 2 is clear from what we just proved: for all implementations I, I ≤ m S 1 ∧ S 2 iff I ≤ m S 1 and I ≤ m S 2 . For the other part, it is clear by construction that for any implementation I, any witness R for I ≤ m S 1 is also a witness for I ≤ m S 1 ∨ S 2 , and similarly for S 2 , hence S 1 ∪ S 2 ⊆ S 1 ∨ S 2 .

To show that also S 1 ∪ S 2 ⊇ S 1 ∨ S 2 , we note that an initialized refinement R witnessing I ≤ m S 1 ∨S 2 must relate the initial state of I either to an initial state of S 1 or to an initial state of S 2 . In the first case, and

Structural composition

For NAA A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), their structural composition is A 1 A 2 = (S 1 × S 2 , S 0 1 × S 0 2 , Tran), with Tran((s 1 , s 2 )) = {M 1 M 2 | M 1 ∈ Tran 1 (s 1 ), M 2 ∈ Tran 2 (s 2 )} for all s 1 ∈ S 1 , s 2 ∈ S 2 , where M 1 M 2 = {(a 1 a 2 , (t 1 , t 2 )) | (a 1 , t 1 ) ∈ M 1 , (a 2 , t 2 ) ∈ M 2 , a 1 a 2 defined}.
Remark a subtle difference between conjunction and structural composition, which we expose for discrete labels and CSP-style composition: for the DMTS D 1 , D 2 shown in Fig. 8, both D 1 ∧ D 2 and D 1 D 2 have only one state, but Tran(s 1 ∧ t 1 ) = ∅ and Tran(s

1 t 1 ) = {∅}, so that D 1 ∧ D 2 is inconsistent, whereas D 1 D 2 is not.
This definition extends the structural composition defined for modal transition systems, with structured labels, in [START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF]. For DMTS specifications (and hence also for ν-calculus expressions), the back translation from NAA to DMTS entails an exponential explosion.

Theorem 5 Up to ≡ m , the operator is associative, commutative and monotone.

Proof Associativity and commutativity are clear by associativity and commutativity of . Monotonicity is equivalent to the assertion that (up to ≡ m ) distributes over the least upper bound ∨; one easily sees that for all specifications S 1 , S 2 , S 3 , the identity is a two-sided modal refinement

S 1 (S 2 ∨ S 3 ) ≡ m S 1 S 2 ∨ S 1 S 3 .
Corollary 1 (Independent implementability) For all specifications S 1 , S 2 , S 3 , S 4 , S 1 ≤ m S 3 and S 2 ≤ m S 4 imply S 1 S 2 ≤ m S 3 S 4 .

Quotient

Because of non-determinism, we have to use a power set construction for the quotient, as opposed to conjunction and structural composition where product is sufficient.

For NAA A 3 = (S 3 , S 0 3 , Tran 3 ), A 1 = (S 1 , S 0 1 , Tran 1 ), the quotient is A 3 /A 1 = (S, {s 0 }, Tran), with S = 2 S3×S1 and s 0 = {(s 0 3 , s 0 1 ) | s 0 3 ∈ S 0 3 , s 0 1 ∈ S 0 1 }.
States in S will be written {s 1 3 /s 1 1 , . . . , s n 3 /s n 1 )}. Intuitively, this denotes that such state when composed with s i 1 conforms to s i 3 for each i; we call this consistency here. We now define Tran. First, Tran(∅) = 2 Σ×{∅} , so ∅ is universal. For any other state s = {s 1 3 /s 1 1 , . . . , s n 3 /s n 1 } ∈ S, its set of permissible labels is defined by

pl(s) = a 2 ∈ Σ ∀i = 1, . . . , n : ∀(a 1 , t 1 ) ∈∈ Tran 1 (s i 1 ) : ∃(a 3 , t 3 ) ∈∈ Tran 3 (s i 3 ) : a 1 a 2 a 3 ,
that is, a label is permissible iff it cannot violate consistency. Here we use the notation x ∈∈ z as a shortcut for ∃y : x ∈ y ∈ z. Now for each a ∈ pl(s) and each i ∈ {1, . . . , n}, let

{t 1 ∈ S 1 | (a, t 1 ) ∈∈ Tran 1 (t i 1 )} = {t i,1 1 , . . . , t i,mi 1
} be an enumeration of all the possible states in S 1 after an a-transition. Then we define the set of all sets of possible assignments of next-a states from s i 3 to next-a states from s i 1 :

pt a (s) = {(t i,j 3 , t i,j 1 ) | i = 1, . . . , n, j = 1, . . . , m i } ∀i : ∀j : (a, t i,j 3 ) ∈∈ Tran 3 (s i 3 )
These are all possible next-state assignments which preserve consistency. Now let pt(s) = a∈pl(s) pt a (s) and define Tran(s) = M ⊆ pt(s) ∀i = 1, . . . , n :

∀M 1 ∈ Tran 1 (s i 1 ) : ∃M 3 ∈ Tran 3 (s i 3 ) : M M 1 R M 3 , where M M 1 = {(a 1 a, t i 3 ) | (a, {t 1 3 /t 1 1 , . . . , t k 3 /t k 1 )}) ∈ M, (a 1 , t i 1 )
∈ M 1 }, to guarantee consistency no matter which element of Tran 1 (s i 1 ), s is composed with.

Example 5 Fig. 9 shows two simple specifications and their quotient under + , i.e., using addition of intervals for label synchronization. Note that in order to have a finite representation of the quotient, we have to extend the label set to allow intervals which are not closed; for instance, the may-transition (send, ]1, ∞]) from {s 0 /t 0 } to ∅ comprises the fact that pt a ({s 0 /t 0 }) = ∅ for all a = (send, [x, ∞]) with x > 1.

Theorem 6 For all specifications S 1 , S 2 , S 3 ,

S 1 S 2 ≤ m S 3 iff S 2 ≤ m S 3 /S 1 .
Proof We show the proof for NAA; for DMTS and νcalculus expressions it will follow through the translations. Let We assume that the elements of Tran 1 (s 1 ) are pairwise disjoint for each s 1 ∈ S 1 ; this can be achieved by, if necessary, splitting states.

A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), A 3 = (S 3 , S 0 3 , Tran 3 ); we show that A 1 A 2 ≤ m A 3 iff A 2 ≤ m A 3 /A 1 . s 0 s 1 (send, [1, 2]) s 2 (send, [2, 3]) • early • late t 0 t 1 (send, [1, 2]) • early late early {s 0 /t 0 } {s 1 /t 1 } {s 2 /t 1 } ∅ Σ (send, [0, 0]) (send, [1, 1]) late, (send, ]0, 1[), (send, ]1, ∞]) Σ \ {late}
First we note that by construction, s ⊇ t implies s ≤ m t for all s, t ∈ S.

Assume that

A 2 ≤ m A 3 /A 1 and let R = {(s 1 s 2 , s 3 ) | s 2 ≤ m s 3 /s 1 }; we show that R is a witness for A 1 A 2 ≤ m A 3 . Let (s 1 s 2 , s 3 ) ∈ R and M ∈ Tran (s 1 s 2 ). Then M = M 1 M 2 with M 1 ∈ Tran 1 (s 1 ) and M 2 ∈ Tran 2 (s 2 ).
As s 2 ≤ m s 3 /s 1 , we can pair M 2 with a set M / ∈ Tran / (s 3 /s 1 ), i.e., such that the conditions in (1) are satisfied.

Let M 3 = M / M 1 . We show that (1) holds for the pair M , M 3 :

-Let (a, t 1 t 2 ) ∈ M , then there are a 1 , a 2 ∈ Σ with a = a 1 a 2 and (a 1 , t

Assume, for the other direction of the proof, that

A 1 A 2 ≤ m A 3 . Define R ⊆ S 2 × 2 S3×S1 by R = (s 2 , {s 1 3 /s 1 1 , . . . , s n 3 /s n 1 }) ∀i = 1, . . . , n : s i 1 s 2 ≤ m s i 3 } ;
we show that R is a witness for A 2 ≤ m A 3 /A 1 . Let (s 2 , s) ∈ R, with s = {s 1 3 /s 1 1 , . . . , s n 3 /s n 1 }, and M 2 ∈ Tran 2 (s 2 ).

For every i = 1, . . . , n, write the set Tran 1 (s

i 1 ) = {M i,1 1 , . . . , M i,mi 1 }. By assumption, M i,j1 1 ∩ M i,j2 1 = ∅ for j 1 = j 2 , hence every (a 1 , t 1 ) ∈∈ Tran 1 (s i 1 ) is con- tained in a unique M i,δi(a1,t1) 1 ∈ Tran 1 (s i 1 ). For every j = 1, . . . , m i , let M i,j = M i,j 1 M 2 ∈ Tran (s i 1 s 2 ). By s i 1 s 2 ≤ m s i 3 , we have M i,j 3 ∈ Tran 3 (s i
3 ) such that (1) holds for the pair M i,j , M i,j

3 . Now define

M = (a 2 , t) ∃(a 2 , t 2 ) ∈ M 2 : ∀t 3 /t 1 ∈ t : ∃i, a 1 , a 3 : (a 1 , t 1 ) ∈∈ Tran 1 (s i 1 ), (3)
(a 3 , t 3 ) ∈ M i,δi(a1,t1) 3 , a 1 a 2 a 3 , t 1 t 2 ≤ m t 3 } .
We need to show that M ∈ Tran / (s). Let i ∈ {1, . . . , n} and M i,j

1 ∈ Tran 1 (s i 1 ); we claim that M M i,j 1 R M i,j 3 . Let (a 3 , t 3 ) ∈ M M i,j 1 , then a 3 = a 1
a 2 for some a 1 , a 2 such that t 3 /t 1 ∈ t, (a 1 , t 1 ) ∈ M i,j 1 and (a 2 , t) ∈ M . By disjointness, j = δ i (a 1 , t 1 ), hence by definition of M , (a 3 , t 3 ) ∈ M i,j 3 as was to be shown.

For the reverse inclusion, let (a 3 , t 3 ) ∈ M i,j 3 . By (1) and definition of M i,j , there are (a 1 , t 1 ) ∈ M i,j 1 and (a 2 , t 2 ) ∈ M 2 for which a 1 a 2 a 3 and t 1 t 2 ≤ m t 3 . Thus j = δ i (a 1 , t 1 ), so that there must be (a 2 , t) ∈ M for which t 3 /t 1 ∈ t, but then also (a 1 a 2 , t 3 ) ∈ M M i,j 1 .

We show that M 2 R M .

-Let (a 2 , t 2 ) ∈ M 2 . For every i = 1, . . . , n and every (a 1 , t 1 ) ∈∈ Tran 1 (t i 1 ), we can use (1) to choose an element

(η i (a 1 , t 1 ), τ i (a 1 , t 1 )) ∈ M i,δi(a1,t1) 3 for which t 1 t 2 ≤ m τ i (a 1 , t 1 ) and a 1 a 2 η i (a 1 , t 1 ). Let t = {τ i (a 1 , t 1 )/t 1 | i = 1, . . . , n, (a 1 , t 1 ) ∈∈ Tran 1 (t i 1 )}, then (a 2 , t) ∈ M and (t 2 , t) ∈ R.
-Let (a 2 , t) ∈ M , then we have (a 2 , t 2 ) ∈ M 2 satisfying the conditions in (3). Hence t 1 t 2 ≤ m t 3 for all t 3 /t 1 ∈ t, so that (t 2 , t) ∈ R.

Robust Specification Theories

We proceed to lift the results of the previous sections to a quantitative setting, where the Boolean notions of modal and thorough refinement are replaced by refinement distances. We have shown in [START_REF] Fahrenberg | Generalized quantitative analysis of metric transition systems[END_REF][START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF][START_REF] Fahrenberg | The quantitative lineartime-branching-time spectrum[END_REF] that a good setting for quantitative analysis is given by the one of recursively specified trace distances on an abstract commutative quantale as defined below; we refer to the above-cited papers for a detailed exposition of how this framework covers all common approaches to quantitative analysis. Denote by Σ ∞ = Σ * ∪ Σ ω the set of finite and infinite traces over Σ.

Recursively specified trace distances

Recall that a (commutative) quantale consists of a complete lattice (L, L ) and a commutative, associative addition operation L which distributes over arbitrary suprema; we denote by ⊥ L , L the bottom and top elements of L. We call a function d : X × X → L, for a set X and a quantale L, an L-hemimetric if it satisfies d(x, x) = ⊥ L for all x ∈ X and d(x, z) L d(x, y) L d(y, z) for all x, y, z ∈ X.

L-hemimetrics are generalizations of distances: for L = R ≥0 ∪{∞} the extended real line, an (R ≥0 ∪{∞})hemimetric is simply an extended hemimetric, and a symmetric extended hemimetric which satisfies indiscernibility of identicals, i.e., for which d(x, y) = 0 implies x = y, is an extended metric. (These are called "extended" because they can take on the value ∞; usually, only non-negative real values are allowed for a (hemi)metric, but adding ∞ does not change much and gives nicer algebraic properties, cf. F is to specify d L tr recursively in the sense that for all a, b ∈ Σ and all σ, τ ∈ Σ ∞ (and with "." denoting concatenation),

d L tr (a.σ, b.τ ) = F (a, b, d L tr (σ, τ )) . ( 4
)
The trace distance associated with such a distance spec-

ification is d tr : Σ ∞ × Σ ∞ → R ≥0 given by d tr = eval • d L tr .
Note that d L tr specializes to a distance on labels (because Σ ⊆ Σ ∞ ); we require that this is compatible with label refinement in the sense that a b implies d L tr (a, b) = ⊥ L . Then (4) implies that whenever a b, then F (a, b, ⊥ L ) = d L tr (a, b) = ⊥ L . As an inverse prop- erty, we say that F is recursively separating if F (a, b, α) = ⊥ L implies that a b and α = ⊥ L .

Example 6 It is shown in [START_REF] Fahrenberg | Generalized quantitative analysis of metric transition systems[END_REF][START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF][START_REF] Fahrenberg | The quantitative lineartime-branching-time spectrum[END_REF] that all commonly used trace distances obey recursive characterizations as above. We give a few examples, all of which are recursively separating:

The point-wise distance from [START_REF] Luca De Alfaro | Model checking discounted temporal properties[END_REF], for example, has

L = R ≥0 ∪ {∞}, eval = id and d L tr (a.σ, b.τ ) = max(d(a, b), d L tr (σ, τ )) ,
where d : Σ×Σ → R ≥0 ∪{∞} is a hemimetric on labels.

For the label set

Σ = U × {[l, r] | l ∈ R ∪ {-∞}, r ∈ R ∪ {∞}, l ≤ r} from Example 1, one useful example of such a hemimetric is d((u 1 , [l 1 , r 1 ]), (u 2 , [l 2 , r 2 ])) = sup x1∈[l1,r1] inf x2∈[l2,r2] |x 1 -x 2 | = max(l 2 -l 1 , r 1 -r 2 , 0) if u 1 = u 2 and ∞ otherwise, cf. [4].
The discounting distance, also used in [START_REF] Luca De Alfaro | Model checking discounted temporal properties[END_REF], again uses L = R ≥0 ∪ {∞} and eval = id, but

d L tr (a.σ, b.τ ) = d(a, b) + λd L tr (σ, τ ) for a constant λ ∈ [0, 1[.
For the limit-average distance used in [START_REF] Černý | and Arjun Radhakrishna. Simulation distances[END_REF] and other For the rest of this paper, we fix a recursively specified trace distance.

papers, L = (R ≥0 ∪ {∞}) N , eval(α) = lim inf j∈N α(j),

Refinement distances

We lift the notions of modal refinement, for all our formalisms, to distances. Conceptually, this is done by replacing "∀" quantifiers by "sup" and "∃" by "inf" in the definitions, and then using the distance iterator to introduce a recursive functional whose least fixed point is the distance.

Definition 2

The lifted refinement distance on the states of DMTS

D 1 = (S 1 , S 0 1 , 1 , -→ 1 ) and D 2 = (S 2 , S 0 2 , 2 , -→ 2 )
is the least fixed point to the equations

d L m (s 1 , s 2 ) = max              sup s1 a 1 t1 inf s2 a 2 t2 F (a 1 , a 2 , d L m (t 1 , t 2 )) , sup s2-→N2 inf s1-→N1 sup (a1,t1)∈N1 inf (a2,t2)∈N2 F (a 1 , a 2 , d L m (t 1 , t 2 )) . for s 1 ∈ S 1 , s 2 ∈ S 2 . For NAA A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), the right-hand side is replaced by sup M1∈Tran1(s1) inf M2∈Tran2(s2) max      sup (a1,t1)∈M1 inf (a2,t2)∈M2 F (a 1 , a 2 , d L m (t 1 , t 2 )) , sup (a2,t2)∈M2 inf (a1,t1)∈M1 F (a 1 , a 2 , d L m (t 1 , t 2 )) ,
and for ν-calculus expressions

N 1 = (X 1 , X 0 1 , ∆ 1 ), N 2 = (X 2 , X 0 2 , ∆ 2 ) in normal form, it is max                  sup a1∈Σ,y1∈ a 1 1 (x1) inf a2∈Σ,y2∈ a 2 2 (x2) F (a 1 , a 2 , d L m (y 1 , y 2 )) , sup N2∈♦2(x2) inf N1∈♦1(x1) sup (a1,y1)∈N1 inf (a2,y2)∈N2 F (a 1 , a 2 , d L m (y 1 , y 2 )) .
Using Tarski's fixed point theorem, one easily sees that the lifted refinement distances are indeed welldefined. (Here one needs monotonicity of F in the third coordinate, together with the fact that sup and inf are monotonic.)

Note that we define the distances using least fixed points, as opposed to the greatest fixed point definition of standard refinement. Informally, this is because our order is reversed: we are not interested in maximizing refinement relations, but in minimizing refinement distance.

The lifted refinement distance between specifications is defined by

d L m (S 1 , S 2 ) = sup s 0 1 ∈S 0 1 inf s 0 2 ∈S 0 2 d L m (s 0 1 , s 0 2 ) .
Analogously to thorough refinement, there is also a

lifted thorough refinement distance, given by d L th (S 1 , S 2 ) = sup I1∈ S1 inf I2∈ S2 d L m (I 1 , I 2 ). Using the eval function, one gets distances d m = eval • d L m and d th = eval • d L th , with values in R ≥0 ∪ {∞},
which will be the ones one is interested in for concrete applications.

Example 7 We compute the discounting refinement distance between the DMTS x and x in Figs. 4 and7 on page 2, assuming sup-inf distance on quantitative labels (see Example 6). We have

d m (x, x ) = max(0 + λd m (x, x ), 0 + λd m (y, y )) , d m (y, y ) = max(0 + λd m (x, x ), 1 + λd m (y, y ) , the least fixed point of which is seen to be d m (x, x ) = λ 1-λ . Similarly, d m (x , x) = λ 1-λ . Note that x ≤ m x and x ≤ m x.
We recall the notion of refinement family from [START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF] and extend it to specifications. We give the definition for NAA only; for DMTS and the modal ν-calculus it is similar.

Definition 3 A refinement family from A 1 to A 2 , for NAA A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), is an L-indexed family of relations R = {R α ⊆ S 1 × S 2 |
α ∈ L} with the property that for all α ∈ L with α = L , all (s 1 , s 2 ) ∈ R α , and all M 1 ∈ Tran 1 (s 1 ),

there is M 2 ∈ Tran 2 (s 2 ) such that -∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 , β ∈ L : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) α, -∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 , β ∈ L : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) α.
Lemma 2 For all NAA A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), there exists a refinement family R from A 1 to A 2 such that for all s 0 1 ∈ S 0 1 , there is

s 0 2 ∈ S 0 2 for which (s 0 1 , s 0 2 ) ∈ R d L m (A1,A2
) . We say that a refinement family as in the lemma

witnesses d L m (A 1 , A 2 ). Proof Define R by R α = {(s 1 , s 2 ) | d L m (s 1 , s 2 ) L α}.
First, as

(s 0 1 , s 0 2 ) ∈ R d L m (s 0 1 ,s 0
2 ) for all s 0 1 ∈ S 0 1 , s 0 2 ∈ S 0 2 , it is indeed the case that for all s 0 1 ∈ S 0 1 , there is s 0 2 ∈ S 0 2 for which

(s 0 1 , s 0 2 ) ∈ R d L m (A1,A2) = R max s 0 1 ∈S 0 1 min s 0 2 ∈S 0 2 d L m (s 0 1 ,s 0 2 ) . Now let α ∈ L with α = L and (s 1 , s 2 ) ∈ R α . Let M 1 ∈ Tran 1 (s 1 ). We have d L m (s 1 , s 2 ) L α, hence there is M 2 ∈ Tran 2 (s 2 ) such that α L max      sup (a1,t1)∈M1 inf (a2,t2)∈M2 F (a 1 , a 2 , d L m (t 1 , t 2 )) , sup (a2,t2)∈M2 inf (a1,t1)∈M1 F (a 1 , a 2 , d L m (t 1 , t 2 )) .
But this entails that for all (a 1 , t 1 ) ∈ M 1 , there is

(a 2 , t 2 ) ∈ M 2 and β = d L m (t 1 , t 2 ) with F (a 1 , a 2 , β) L α, and that for all (a 2 , t 2 ) ∈ M 2 , there is (a 1 , t 1 ) ∈ M 1 and β = d L m (t 1 , t 2 ) such that F (a 1 , a 2 , β) L α.
The following quantitative extension of Theorems 1 and 3 shows that our translations preserve and reflect refinement distances. Its proof is rather long and tedious, hence we present it in a separate appendix to this paper.

Theorem 7 For all DMTS D 1 , D 2 , all NAA A 1 , A 2 and all ν-calculus expressions N 1 , N 2 : d L m (D 1 , D 2 ) = d L m (da(D 1 ), da(D 2 )) d L m (A 1 , A 2 ) = d L m (ad(A 1 ), ad(A 2 )) d L m (D 1 , D 2 ) = d L m (dn(D 1 ), dn(D 2 )) d L m (N 1 , N 2 ) = d L m (nd(N 1 ), nd(N 2 ))

Properties

We sum up some important properties of our distances.

Proposition 2 For all specifications S 1 , S 2 , S 1 ≤ m S 2 implies d L m (S 1 , S 2 ) = ⊥ L , and S 1 ≤ th S 2 implies d L th (S 1 , S 2 ) = ⊥ L . If F is recursively separating, then d L m (S 1 , S 2 ) = ⊥ L implies S 1 ≤ m S 2 .
Proof We show the proposition for NAA. First, if

A 1 ≤ m A 2 , with A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), then there is an initialized refinement relation R ⊆ S 1 × S 2 , i.e., such that for all (s 1 , s 2 ) ∈ R and all M 1 ∈ Tran 1 (s 1 ), there is M 2 ∈ Tran 2 (s 2 ) for which -∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 : a 1 a 2 , (t 1 , t 2 ) ∈ R and -∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 : a 1 a 2 , (t 1 , t 2 ) ∈ R. Defining R = {R α | α ∈ L} by R α = R for all α ∈ L, we see that R is an initialized refinement family which witnesses d L m (A 1 , A 2 ) = ⊥ L . We have shown that A 1 ≤ m A 2 implies d L m (A 1 , A 2 ) = ⊥ L . Now if A 1 ≤ th A 2 instead, then for all I ∈ A 1 , also I ∈ A 2 , hence d L th (A 1 , A 2 ) = ⊥ L .
To show the last property, assume F to be recur-

sively separating. Define R ⊆ S 1 × S 2 by R = {(s 1 , s 2 ) | d L m (s 1 , s 2 ) = ⊥ L }; we show that R is a witness for A 1 ≤ m A 2 . By d L m (A 1 , A 2 ) = ⊥ L , R is initialized.
Let (s 1 , s 2 ) ∈ R and M 1 ∈ Tran 1 (s 1 ), then there is

M 2 ∈ Tran 2 (s 2 ) such that ∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 , β 1 ∈ L : d L m (t 1 , t 2 ) L β 1 , F (a 1 , a 2 , β 1 ) = ⊥ L , ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 , β 1 ∈ L : d L m (t 1 , t 2 ) L β 1 , F (a 1 , a 2 , β 1 ) = ⊥ L .
As F is recursively separating, we must have a 1 a 2 in both these equations and

β 1 = β 2 = ⊥ L . But then (t 1 , t 2 ) ∈ R, hence R is indeed a witness for A 1 ≤ m A 2 .
R 1 = {R 1 α ⊆ S 1 × S 2 | α ∈ L}, R 2 = {R 2 α ⊆ S 2 × S 3 | α ∈ L} refinement families such that ∀s 0 1 ∈ S 0 1 : ∃s 0 2 ∈ S 0 2 : (s 0 1 , s 0 2 ) ∈ R 1 d L m (A1,A2)
and ∀s 0 2 ∈ S 0 2 : ∃s 0 3 ∈ S 0 3 : (s 0 2 , s 0

3 ) ∈ R 2 d L m (A2,A3) . Define R = {R α ⊆ S 1 × S 3 | α ∈ L} by R α = (s 1 , s 3 ) ∃α 1 , α 2 ∈ L, s 2 ∈ S 2 : (s 1 , s 2 ) ∈ R 1 α1 , (s 2 , s 3 ) ∈ R 2 α2 , α 1 L α 2 = α .
We see that for all s 0 1 ∈ S 0 1 , there is s 0 3 ∈ S 0 3 such that

(s 0 1 , s 0 3 ) ∈ R d L m (A1,A2) L d L m (A2,A3) ; we show that R is a refinement family from A 1 to A 2 . Let α ∈ L and (s 1 , s 3 ) ∈ R α , then we have α 1 , α 2 ∈ L and s 2 ∈ S 2 such that α 1 L α 2 = α, (s 1 , s 2 ) ∈ R 1 α1 and (s 2 , s 3 ) ∈ R 2 α2 . Let M 1 ∈ Tran 1 (s 1 ), then we have M 2 ∈ Tran 2 (s 2 ) such that ∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 , β 1 ∈ L : (t 1 , t 2 ) ∈ R 1 β1 , F (a 1 , a 2 , β 1 ) L α 1 , (5) ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 , β 1 ∈ L : (t 1 , t 2 ) ∈ R 1 β1 , F (a 1 , a 2 , β 1 ) L α 1 . (6)
This in turn implies that there is

M 3 ∈ Tran 3 (s 3 ) with ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 3 , t 3 ) ∈ M 3 , β 2 ∈ L : (t 2 , t 3 ) ∈ R 2 β2 , F (a 2 , a 3 , β 2 ) L α 2 , (7) ∀(a 3 , t 3 ) ∈ M 3 : ∃(a 2 , t 2 ) ∈ M 2 , β 2 ∈ L : (t 2 , t 3 ) ∈ R 2 β2 , F (a 2 , a 3 , β 2 ) L α 2 . (8)
Now let (a 1 , t 1 ) ∈ M 1 , then we get (a 2 , t 2 ) ∈ M 2 , (a 3 , t 3 ) ∈ M 3 and β 1 , β 2 ∈ L as in ( 5) and [START_REF] Ben-David | Merging partial behaviour models with different vocabularies[END_REF]. Let β = β 1 L β 2 , then (t 1 , t 3 ) ∈ R β , and by the extended tri- angle inequality for F , F (a

1 , a 3 , β) L F (a 1 , a 2 , β 1 ) L F (a 2 , a 3 , β 2 ) L α 1 L α 2 = α.
Similarly, given (a 3 , t 3 ) ∈ M 3 , we can apply [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] and [START_REF] Bauer | Foundations of Interface Technologies[END_REF] to get (a 1 , t 1 ) ∈ M 1 and β ∈ L such that (t 1 , t 3 ) ∈ R β and F (a 1 , a 3 , β) L α.

We have shown that d L m and d L tr are L-hemimetrics.

Using monotonicity of the eval function, it follows that d m and d tr are hemimetrics.

Proposition 4 For the discrete distances, d m (S 1 , S 2 ) = 0 if S 1 ≤ m S 2 and ∞ otherwise. Similarly, d th (S 1 , S 2 ) = 0 if S 1 ≤ th S 2 and ∞ otherwise.
Proof We show the proposition for NAA. We already know that, also for the discrete distances,

A 1 ≤ m A 2 implies d m (A 1 , A 2 ) = 0 and that A 1 ≤ th A 2 implies d th (A 1 , A 2 ) = 0. We show that d m (A 1 , A 2 ) = 0 implies A 1 ≤ m A 2 . Let R = {R α ⊆ S 1 × S 2 | α ∈ L} be
a refinement family such that ∀s 0 1 ∈ S 0 1 : ∃s 0 2 ∈ S 0 2 : (s 0 1 , s 0 2 ) ∈ R 0 . We show that R 0 is a witness for A 1 ≤ m A 2 ; it is clearly initialized.

Let (s 1 , s 2 ) ∈ R 0 and M 1 ∈ Tran 1 (s 1 ), then we have

M 2 ∈ Tran 2 (s 2 ) such that ∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 , β ∈ L : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) = 0 , ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 , β ∈ L : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) = 0 . (9)
Using the definition of the distance, we see that the condition F (a 1 , a 2 , β) = 0 is equivalent to a 1 a 2 and β = 0, hence (9) degenerates to

∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 : (t 1 , t 2 ) ∈ R 0 , a 1 a 2 , ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R 0 , a 1 a 2 ,
which are exactly the conditions for R 0 to be a modal refinement.

Again by definition, we see that for any NAA

A 1 , A 2 , either d m (A 1 , A 2 ) = 0 or d m (A 1 , A 2 ) = ∞, hence A 1 ≤ m A 2 implies that d m (A 1 , A 2 ) = ∞.
To show the last part of the proposition, we notice that

d th (A 1 , A 2 ) = sup I1∈ A1 inf I2∈ A2 d m (I 1 , I 2 ) = 0 if ∀I 1 ∈ A 1 : ∃I 2 ∈ A 2 : I 1 ≤ m I 2 , ∞ otherwise , = 0 if A 1 ⊆ A 2 , ∞ otherwise . Hence d th (A 1 , A 2 ) = 0 if A 1 ≤ th A 2 and d th (A 1 , A 2 ) = ∞ otherwise.
As a quantitative analogy to the implication from (Boolean) modal refinement to thorough refinement (see Proposition 1), the next theorem shows that thorough refinement distance is bounded above by modal refinement distance. Note that for the discrete trace distance (and using Proposition 4), this is equivalent to the Boolean statement.

Theorem 8 For all specifications S 1 , S 2 , d L th (S 1 , S 2 ) L d L m (S 1 , S 2 ).
Proof We prove the statement for NAA; for DMTS and ν-calculus expressions it then follows from Theorem 7.

Let

A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ). We have a refinement family R = {R α ⊆ S 1 × S 2 | α ∈ L} such that for all s 0 1 ∈ S 0 1 , there is s 0 2 ∈ S 0 2 with (s 0 1 , s 0 2 ) ∈ R d L m (A1,A2) . Let I = (S, S 0 , T ) ∈ A 1 , i.e., I ≤ m A 1 .
Let R 1 ⊆ S × S 1 be an initialized modal refinement, and define a relation family

R 2 = {R 2 α ⊆ S × S 2 | α ∈ L} by R 2 α = R 1 • R α = {(s, s 2 ) | ∃s 1 ∈ S : (s, s 1 ) ∈ R 1 , (s 1 , s 2 ) ∈ R α . We define a LTS I 2 = (S 2 , S 0 2 , T 2 ) as follows: For all α ∈ L with α = L and (s, s 2 ) ∈ R 2 α : We must have s 1 ∈ S 1 with (s, s 1 ) ∈ R 1 and (s 1 , s 2 ) ∈ R α . Then there is M 1 ∈ Tran 1 (s 1 ) such that -for all s a -→ t, there is (a, t 1 ) ∈ M 1 with (t, t 1 ) ∈ R 1 , -for all (a 1 , t 1 ) ∈ M 1 , there is s a -→ t with (t, t 1 ) ∈ R 1 .
This in turn implies that there is M 2 ∈ Tran 2 (s 2 ) satisfying the conditions in Definition 3. For all (a 2 , t 2 ) ∈ M 2 : add a transition s 2 a2 -→ t 2 to T 2 . We show that the identity relation -→ t 2 . By construction, there is an M 2 ∈ Tran 2 (s 2 ) with (a 2 , t 2 ) ∈ M 2 . This implies that there is M 1 ∈ Tran 1 (s 1 ), β ∈ L and (a 1 , t 1 ) ∈ M 1 with (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) α. But then there is also s a1 -→ t with (t, t 1 ) ∈ R 1 , hence (t, t 2 ) ∈ R 2 β .

{(s 2 , s 2 ) | s 2 ∈ S 2 } is a witness for I 2 ≤ m A 2 . Let s 2 ∈ S 2 and s 2 a2 -→ t 2 . By construction, there is an M 2 ∈ Tran 2 (s 2 ) with (a 2 , t 2 ) ∈ M 2 , and for all (a 2 , t 2 ) ∈ M 2 , s 2 a 2 -→ t 2 . We show that R 2 is a witness for d L m (I, I 2 ); clearly, R 2 is initialized. Let α ∈ L with α = L and (s, s 2 ) ∈ R 2 α , then there is s 1 ∈ S 1 with (s, s 1 ) ∈ R 1 and (s 1 , s 2 ) ∈ R α . We also have M 1 ∈ Tran 1 (s 1 ) such that -for all s a -→ t, there is (a, t 1 ) ∈ M 1 with (t, t 1 ) ∈ R 1 , -for all (a, t 1 ) ∈ M 1 , there is s a -→ t with (t, t 1 ) ∈ R 1 and thus M 2 ∈ Tran 2 (s 2 ) satisfying the conditions in Definition 3. Let s a -→ t, then there is (a, t 1 ) ∈ M 1 with (t, t 1 ) ∈ R 1 , hence also (a 2 , t 2 ) ∈ M 2 and β ∈ L with (t 1 , t 2 ) ∈ R β and F (a, a 2 , β) L α. But then (t, t 2 ) ∈ R 2 β ,

Disjunction and conjunction

In order to generalize the properties of Theorem 4 to our quantitative setting, we introduce a notion of relaxed implementation semantics:

Definition 4 The α-relaxed implementation semantics of S, for a specification S and α ∈ L, is

S α = {I implementation | d L m (I, S) α} .
Hence, S α comprises all labeled transition systems which are implementations of S up to α. Note that by Proposition 2 and for F recursively separating, S ⊥ L = S .

Theorem 9 For all specifications S 1 , S 2 , S 3 and α ∈ L,

-d L m (S 1 ∨ S 2 , S 3 ) = max(d L m (S 1 , S 3 ), d L m (S 2 , S 3 )), -d L m (S 1 , S 2 ∧ S 3 ) L max(d L m (S 1 , S 2 ), d L m (S 1 , S 3 )), -S 1 ∨ S 2 α = S 1 α ∪ S 2 α , and -S 1 ∧ S 2 α ⊆ S 1 α ∩ S 2 α .
Proof We show the proof for DMTS.

The proof that d L To show that d L

m (D 1 ∨ D 2 , D 3 ) = max(d L m (D 1 , D 3 ), d L m (D 2 , D 3
m (D 1 , D 2 ∧ D 3 ) L max(d L m (D 1 , D 2 ), d L m (D 1 , D 3 )), let R = {R α ⊆ S 1 × (S 2 × S 3 ) | α ∈ L} be a witness for d L m (D 1 , D 2 ∧ D 3 ) and define R 2 = {R 2 α ⊆ S 1 × S 2 | α ∈ L} by R 2 α = {(s 1 , s 2 ) | ∃s 3 ∈ S 3 : (s 1 , (s 2 , s 3 )) ∈ R α } for all α ∈ L. Let s 0 1 ∈ S 0 1 , then we have (s 0 2 , s 0 3 ) ∈ S 0 2 × S 0 3 so that (s 0 1 , (s 0 2 , s 0 3 )) ∈ R d L m (D1,D2∧D3) , hence also (s 0 1 , s 0 2 ) ∈ R 2 d L m (D1,D2∧D3) . Let α ∈ L and (s 1 , s 2 ) ∈ R 2 α , then we have s 3 ∈ S 3 for which (s 1 , (s 2 , s 3 )) ∈ R α . Assume first that s 1 a1 t 1 , then there is (s 2 , s 3 ) a (t 2 , t 3 ) and β ∈ L such that F (a 1 , a, β) L α and (t 1 , (t 2 , t 3 )) ∈ R β , hence (t 1 , t 2 ) ∈ R 2 β . By construction of D 2 ∧ D 3 , there are s 2 a2 t 2
and s 3 a3 t 3 such that a = a 2 a 3 , but then by anti-

monotonicity, F (a 1 , a 2 , β) L F (a 1 , a, β) α. Now assume s 2 -→ N 2 , then, by construction, (s 2 , s 3 ) -→ N = {(a 2 a 3 , (t 2 , t 3 )) | (a 2 , t 2 ) ∈ N 2 , s 3 a3 3 t 3 }. Hence we have s 1 -→ 1 N 1 such that ∀(a 1 , t 1 ) ∈ N 1 : ∃(a, (t 2 , t 3 )) ∈ N, β ∈ L : F (a 1 , a, β) α, (t 1 , (t 2 , t 3 )) ∈ R β .
Let (a 1 , t 1 ) ∈ N 1 , then we have (a, (t 2 , t 3 )) ∈ N and

β ∈ L for which F (a 1 , a, β) L α and (t 1 , (t 2 , t 3 )) ∈ R β , hence (t 1 , t 2 ) ∈ R 2 β
. By construction of N , this implies that there are (a 2 , t 2 ) ∈ N 2 and s 3 a3 3 t 3 such that a = a 2 a 3 , but then by anti-monotonicity, F (a 1 , a 2 , β) L F (a 1 , a, β) α. The below example shows why the inclusions above cannot be replaced by equalities. To sum up, disjunction is quantitatively sound and complete, whereas conjunction is only quantitatively sound.

We have shown that

d L m (D 1 , D 2 ∧D 3 ) L d L m (D 1 , D 2 ); the proof of d L m (D 1 , D 2 ∧ D 3 ) L d L m (D 1 , D 3 ) is entirely analogous. The inclusion D 1 ∧ D 2 α ⊆ D 1 α ∩ D 2 α is clear now: If I ∈ D 1 ∧ D 2 α , i.e., d L m (I, D 1 ∧ D 2 ) L α, then also d L m (I, D 1 ) L α and d L m (I, D 2 ) L α, thus I ∈ D 1 α ∩ D 2 α . To show that D 1 ∨ D 2 α = D 1 α ∪ D 2 α ,

Structural composition and quotient

We proceed to devise a quantitative generalization of the properties of structural composition and quotient exposed in Section 4. To this end, we need to use a uniform composition bound on labels:

Let P : L×L → L be a function which is monotone in both coordinates, has P (α, ⊥ L ) = P (⊥ L , α) = α and P (α, L ) = P ( L , α) = L for all α ∈ L. We require that for all a L P (F (a 1 , a 2 , α), F (b 1 , b 2 , β)) . (10) Note that [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF] . Hence P provides a uniform bound on distances between synchronized labels, 1 and (10) extends this property so that it holds recursively. Also, this is a generalization of the condition that we imposed on in Section 2; it is shown in [START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF] that it holds for all common label synchronizations.

The following theorems show that composition is uniformly continuous (i.e., a quantitative generalization of independent implementability; Corollary 1) and that quotient preserves and reflects refinement distance (a quantitative generalization of Theorem 6). Proof We show the proof for NAA. For i = 1, 2, 3, 4, let 1 Indeed, P bears some similarity to the concept of modulus of continuity used in analysis.

A i = (S i , S 0 i , Tran i ). Let R 1 = {R 1 α ⊆ S 1 ×S 3 | α ∈ L},

Tran 3 (s i

3 ) such that the conditions in Definition 3 hold for the pair M i,j , M i,j 3 . Now define M = (a 2 , t) ∃(a 2 , t 2 ) ∈ M 2 : ∀t 3 /t 1 ∈ t : ∃i, a 1 , a 3 , β : (a 1 , t 1 ) ∈∈ Tran 1 (s i 1 ), (a 3 , t 3 ) ∈ M i,δi(a1,t1) 3

, F (a 1 a 2 , a 3 , β) L α, d L m (t 1 t 2 , t 3 ) L β . (15) We need to show that M ∈ Tran / (s).

Let i ∈ {1, . . . , n} and M i,j 1 ∈ Tran 1 (s i 1 ); we claim that M M i,j 1 R M i,j

3 . Let (a 3 , t 3 ) ∈ M M i,j 1 , then a 3 = a 1 a 2 for some a 1 , a 2 such that t 3 /t 1 ∈ t, (a 1 , t 1 ) ∈ M i,j 1 and (a 2 , t) ∈ M . By disjointness, j = δ i (a 1 , t 1 ), hence by definition of M , (a 3 , t 3 ) ∈ M i,j

3 as was to be shown.

For the reverse inclusion, let (a 3 , t 3 ) ∈ M i,j 3 . By definition of M i,j , there are (a 1 , t 1 ) ∈ M i,j 1 , (a 2 , t 2 ) ∈ M 2 and β ∈ L for which F (a 1 a 2 , a 3 , β) L α and d L m (t 1 t 2 , t 3 ) L β. Thus j = δ i (a 1 , t 1 ), so that there must be (a 2 , t) ∈ M for which t 3 /t 1 ∈ t, but then also (a 1 a 2 , t 3 ) ∈ M M i,j 1 . We show that the pair M 2 , M satisfies the conditions of Definition 3.

-Let (a 2 , t 2 ) ∈ M 2 . For every i = 1, . . . , n and every (a 1 , t 1 ) ∈∈ Tran 1 (t i 1 ), we can use Definition 3 applied to the pair M i,δi(a1,t1) 1 M 2 , M i,δi(a1,t1) 3 to choose an element (η i (a 1 , t 1 ), τ i (a 1 , t 1 )) ∈ M i,δi(a1,t1) 3 and β i (a 1 , t 1 ) ∈ L for which d L m (t 1 t 2 , τ i (a 1 , t 1 )) L β i (a 1 , t 1 ) and F (a 1 a 2 , η i (a 1 , t 1 ), β i (a 1 , t 1 )) L α.

Let t = {τ i (a 1 , t 1 )/t 1 | i = 1, . . . , n, (a 1 , t 1 ) ∈∈ Tran 1 (t i 1 )}, then (a 2 , t) ∈ M and (t 2 , t) ∈ R β . -Let (a 2 , t) ∈ M , then we have (a 2 , t 2 ) ∈ M 2 satisfying the conditions in [START_REF] Cardelli | Modular Markovian logic[END_REF]. Hence for all t 3 /t 1 ∈ t, there are i, a 1 , a 3 , and β(t 3 /t 1 ) such that (a 3 , t 3 ) ∈ M i,δi(a1,t1) 3

, F (a 1 a 2 , a 3 , β(t 3 /t 1 ))

L α and d L m (t 1 t 2 , t 3 ) L β(t 3 /t 1 ). Let β = sup{β(t 3 /t 1 ) | t 3 /t 1 ∈ t}, then d L m (t 1 t 2 , t 3 ) L β for all t 3 /t 1 ∈ t, hence (t 2 , t) ∈ R β .

Conclusion

We have presented a framework for compositional and iterative design and verification of systems which supports quantities and system and action refinement. Moreover, it is robust, in that it uses distances to measure quantitative refinement and the operations preserve distances.

The framework is very general. It can be applied to a large variety of quantities (energy, time, resource consumption etc.) and implement the robustness notions associated with them. It is also agnostic with respect to the type of specifications used, as it applies equally to behavioral and logical specifications. This means that logical and behavioral quantitative specifications can be freely combined in quantitative system development.

As to future work, we believe that that the close relationship between DMTS and the modal ν-calculus which we expose here should be helpful for relating our robust semantics of the modal ν-calculus to other quantitative logics [START_REF] De | Quantitative verification and control via the mu-calculus[END_REF][START_REF] Huth | Quantitative analysis and model checking[END_REF][START_REF] Mio | Probabilistic modal mu-calculus with independent product[END_REF]. We also plan to implement the operations detailed here within the graphical tool Mo-TraS [START_REF] Křetínský | MoTraS: A tool for modal transition systems and their extensions[END_REF].

Fig. 1 Fig. 2

 12 Fig. 1 Specification of a simple vending machine

Fig. 3 A

 3 Fig. 3 A simple real-time specification

Fig. 6

 6 Fig. 6 Two implementations

Theorem 2

 2 For any LTS I and any ν-calculus expression N in normal form, I |= N iff I ≤ m N . For a DMTS D = (S, S 0 , , -→) and all s ∈ S, let ♦(s) = {N | s -→ N } and, for each a ∈ Σ, a (s) = {t | s a t}. Define the (normal-form) ν-calculus expression dn(D) = (S, S 0 , ∆), with ∆ given as in (2).

Fig. 8

 8 Fig. 8 Two simple DMTS

early Σ \ {early} late Fig. 9

 late9 Fig. 9 Two DMTS (top and center) and their quotient (bottom)

  [START_REF] Lawvere | Metric spaces, generalized logic, and closed categories[END_REF].)A recursive trace distance specification (L, eval, d L tr , F ) consists of a quantale L, a quantale morphism eval :L → R ≥0 ∪ {∞}, an L-hemimetric d L tr : Σ ∞ × Σ ∞ → L (calledlifted trace distance), and a distance iterator function F : Σ×Σ×L → L. F must be monotone in the third and anti-monotone in the second coordinate and satisfy an extended triangle inequality: for all a, b, c ∈ Σ and α, β ∈ L, F (a, b, α) L F (b, c, β) L F (a, c, α L β).

  tr (a.σ, b.τ )(j) = 1 j+1 d(a, b) + j j+1 d L tr (σ, τ )(j -1) . The discrete trace distance is given by d tr (σ, τ ) = 0 if σ τ and ∞ otherwise (here we have extended to traces in the obvious way). It has a recursive characterization with L = R ≥0 ∪ {∞}, eval = id, and d tr (a.σ, b.τ ) = d tr (σ, τ ) if a b and ∞ otherwise.

Proposition 3 2 . 1 , 2 , 3 ,

 32123 The functions d L m and d L th are L-hemimetrics, and d m , d th are hemimetrics. Proof We show the proof for NAA. The properties that d L m (A, A) = ⊥ L and d L th (A, A) = ⊥ L follow from propo- sition We show the triangle inequality for d L m . The triangle inequality for d L th will then follow from standard arguments used to show that the Hausdorff metric satisfies the triangle inequality, see e.g., [2, Lemma 3.72]. Let A 1 = (S 1 , S 0 Tran 1 ), A 2 = (S 2 , S 0 Tran 2 ), A 3 = (S 3 , S 0 Tran 3 ) be NAA and

  )) is trivial: any refinement family witnessing d L m (D 1 ∨ D 2 , D 3 ) splits into two families witnessing d L m (D 1 , D 3 ) and d L m (D 2 , D 3 ) and vice versa.

  one notices, like in the proof of Theorem 4, that for any LTS I, any refinement family witnessing d L m (I, D 1 ) or d L m (I, D 2 ) is also a witness for d L m (I, D 1 ∨ D 2 ) and vice versa.

2 Fig. 10 LTSExample 8

 2108 Fig. 10 LTS I together with DMTS D 1 , D 2 and their conjunction. For the point-wise or discounting distances, dm(I, D 1 ) = dm(I, D 2 ) = 1, but dm(I, D 1 ∧ D 2 ) = ∞

1 , b 1 , a 2 , b 2 ∈

 1122 Σ and α, β ∈ L withF (a 1 , a 2 , α) = and F (b 1 , b 2 , β) = , a 1 b 1 is defined iffa 2 b 2 is, and if both are defined, then F (a 1 b 1 , a 2 b 2 , P (α, β))

  implies that d tr (a 1 a 2 , b 1 b 2 ) L P (d tr (a 1 , b 1 ), d tr (a 2 , b 2 ))

Theorem 10 For all specifications S 1 , S 2 , S 3 ,

 10123 S 4 , d L m (S 1 S 2 , S 3 S 4 ) L P (d L m (S 1 , S 3 ), d L m (S 2 , S4)).

R 2 = {R 2 α ⊆ S 2 ×

 22 S 4 | α ∈ L} be refinement families such that ∀s 0 1 ∈ S 0 1 : ∃s 0 3 ∈ S 0 3 : (s 0 1 , s 0 3 ) ∈ R 1 d L m (A1,A3)

  1 there is s 2 a2 2 t 2 such that a 1 a 2 and (t 1 , t 2 ) ∈ R, and for all s 2 -→ 2 N 2 there is s 1 -→ 1 N 1 such that for all (a 1 , t 1 ) ∈ N 1 there is (a 2 , t 2 ) ∈ N 2 with a 1 a 2 and (t 1 , t 2 ) ∈ R. D 1 refines D 2 , denoted D 1 ≤ m D 2 , if there exists an initialized modal refinement R, i.e., one for which it holds that for every s 0 1

  we have s 2 a2 2 t 2 with a 1 a 2 and (t 1 , t 2 ) ∈ R 2 . Similarly, by S 1 ≤ m S 3 , we have s 3 a3 3 t 3 with a 1 a 3 and (t 1 , t 3 ) ∈ R 3 . But then also a 1 a 2 a 3 and (t 1 , (t 2 , t 3 )) ∈ R, and (s 2 , s 3 ) a2 a3 (t 2 , t 3 ) by definition.

  1 ) ∈ M 1 , (a 2 , t 2 ) ∈ M 2 . By (1), there is (a 2 , t) ∈ M / such that a 2 a 2 and t 2 ≤ m t.Note that a 3 = a 1 a 2 is defined and a a 3 . Write , t 3 ) ∈ R.-Let (a 3 , t 3 ) ∈ M 3 , then there are (a 2 , t) ∈ M / and (a 1 , t 1 ) ∈ M 1 such that a 3 = a 1 a 2 and t 3 /t 1 ∈ t.

	t = {t 1 3 /t 1 1 , . . . , t n 3 /t n 1 }. By construction, there is an
	index i for which t i 1 = t 1 , hence (a 3 , t i 3 ) ∈ M 3 . Also,
	t ⊇ {t i 3 /t i 1 }, hence t 2 ≤ m t i 3 /t i 1 and consequently
	(t 1 t 2

By

[START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF]

, there is (a 2 , t 2 ) ∈ M 2 for which a 2 a 2 and t 2 ≤ m t. Note that a = a 1 a 2 is defined and a a 3 . Thus (a, t 1 t 2 ) ∈ M , and by t ⊇ {t 3 /t 1 }, t 2 ≤ m t 3 /t 1 .

and ∀s 0 2 ∈ S 0 2 : ∃s 0 4 ∈ S 0 4 : (s 0 2 , s 0 4 ) ∈ R 2 d L m (A2,A4) . Define R = {R α ⊆ (S 1 × S 2 ) × (S 3 × S 4 ) | α ∈ } by R α = ((s 1 , s 2 ), (s 3 , s 4 )) ∃α 1 , α 2 ∈ L :

then it is clear that ∀(s 0 1 , s 0 2 ) ∈ S 0 1 × S 0 2 : ∃(s 0 3 , s 0 4 ) ∈ S 0 3 × S 0 4 : ((s 0 1 , s 0 2 ), (s 0 3 , s 0 4 )) ∈ R P (d L m (A1,A3),d L m (A2,A4)) . We show that R is a refinement family from A 1 A 2 to A 3 A 4 .

Let α ∈ L and ((s 1 , s 2 ), (s 3 , s 4 )) ∈ R α , then we have α 1 , α 2 ∈ L with (s 1 , s 3 ) ∈ R 1 α1 , (s 2 , s 4 ) ∈ R 2 α2 and P (α 1 , α 2 ) L α. Let M 12 ∈ Tran((s 1 , s 2 )), then there must be M 1 ∈ Tran 1 (s 1 ), M 2 ∈ Tran 2 (s 2 ) for which

Thus we also have M 3 ∈ Tran 3 (s 3 ) and M 4 ∈ Tran 4 (s 4 ) such that ∀(a 1 , t 1 ) ∈ M 1 : ∃(a 3 , t 3 ) ∈ M 3 , β 1 ∈ L :

∀(a 3 , t 3 ) ∈ M 3 : ∃(a 1 , t 1 ) ∈ M 1 , β 1 ∈ L :

∀(a 2 , t 2 ) ∈ M 2 : ∃(a 4 , t 4 ) ∈ M 4 , β 2 ∈ L :

∀(a 4 , t 4 ) ∈ M 4 : ∃(a 2 , t 2 ) ∈ M 2 , β 2 ∈ L :

Let M 34 = M 3 M 4 , then M 34 ∈ Tran((s 3 , s 4 )). Let (a 12 , (t 1 , t 2 )) ∈ M 12 , then there are (a 1 , t 1 ) ∈ M 1 and (a 2 , t 2 ) ∈ M 2 for which a 12 = a 1 a 2 . Using [START_REF] Bertrand | Modal event-clock specifications for timed component-based design[END_REF] and [START_REF] Caillaud | Constraint Markov chains[END_REF], we get (a 3 , t 3 ) ∈ M 3 , (a 4 , t 4 ) ∈ M 4 and

Let a 34 = a 3 a 4 and β = P (β 1 , β 2 ), then we have (a 34 , (t 3 , t 4 )) ∈ M 34 . Also, (t

We have shown that for all (a 12 , (t 1 , t 2 )) ∈ M 12 , there exists (a 34 , (t 3 , t 4 )) ∈ M 34 and β ∈ L such that ((t 1 , t 2 ), (t 3 , t 4 )) ∈ R β and F (a 12 , a 34 , β) L α. To show the re- verse property, starting from an element (a 34 , (t 3 , t 4 )) ∈ M 34 , we can proceed entirely analogous, using [START_REF] Boudol | Graphical versus logical specifications[END_REF] and [START_REF] Caires | A spatial logic for concurrency (part I)[END_REF].

Theorem 11 For all specifications S 1 , S 2 , S 3 , we have

Proof We show the proof for NAA. Let

We assume that the elements of Tran 1 (s 1 ) are pairwise disjoint for each s 1 ∈ S 1 ; this can be achieved by, if necessary, splitting states.

and M 2 ∈ Tran 2 (s 2 ). As d L m (s 2 , s 3 /s 1 ) L α, we can pair M 2 with an M / ∈ Tran / (s 3 /s 1 ), i.e., such that the conditions in Definition 3 are satisfied.

Let M 3 = M / M 1 . We show that the conditions in Definition 3 are satisfied for the pair M , M 3 :

-Let (a, t 1 t 2 ) ∈ M , then there are a 1 , a 2 ∈ Σ with a = a 1 a 2 and (a

Hence there is (a 2 , t) ∈ M / and β ∈ L such that

Note that a 3 = a 1 a 2 is defined and F (a, a 3 , β) α. Write t = {t 1 3 /t 1 1 , . . . , t n 3 /t n 1 }. By construction, there is an index i for which

(a 1 , t 1 ) ∈ M 1 such that a 3 = a 1 a 2 and t 3 /t 1 ∈ t.

Hence there are (a 2 , t 2 ) ∈ M 2 and β ∈ L for which

Note that a = a 1 a 2 is defined and F (a, a 3 , β) L α. Thus (a, t 1 t 2 ) ∈ M , and by

Assume, for the other direction of the proof, that

and define

The condition

is satisfied by construction. For the inverse condition, let (a 1 , t 1 ) ∈ M 1 , then s 1 a1 1 t 1 , and as R is a DMTS refinement family, this implies that there is s 2

We are left with showing that M 2 ∈ Tran 2 (s 2 ). First we notice that by construction, indeed s 2

We have

We know that

Then there is (a 2 , t 2 ) ∈ N 2 and β ∈ L such that

) by construction. This implies that there is

a2 t 2 as was to be shown.

Let s 2 -→ N 2 and assume, for the sake of contradiction, that there is no s 1 -→ N 1 for which ∀(a 1 , t 1 ) ∈

There is an NAA

We show that R is a witness for d L m (ad

We show that ∀(a

This in turn implies that there must be (a

for all (a 2 , M 2 ) ∈ N 2 . By the same arguments as above, there is (a 2 , M 2 ) ∈ N 2 for which (M 1 , M 2 ) ∈ R β .

We miss to show that R is initialized. Let M 0 1 ∈ D 0 1 , then we have s 0 1 ∈ S 0 1 with M 0 1 ∈ Tran 1 (s 0 1 ). As R is initialized, this entails that there is s 0 2 ∈ S 0 2 with (s 0 1 , s 0 2 ) ∈ R d L m (A1,A2) , which gives us M 0 2 ∈ Tran 2 (s 0 2 ) which satisfies the conditions in the definition of R d L m (A1,A2) , whence

Let (a 1 , t 1 ) ∈ M 1 and define

We miss to show that R is initialized. Let

2 ) for some s 0 2 ∈ S 0 2 , and then Let α ∈ L, (s 1 , s 2 ) ∈ R α , a 1 ∈ Σ, and t 1 ∈ a1 1 (s 1 ). Then s 1 a1 1 t 1 , hence we have s 2 a2 2 t 2 and β ∈ L with (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) L α, but then also

Let α ∈ L and (s 1 , s 2 ) ∈ R α , and assume that

Let α ∈ L and (x 1 , x 2 ) ∈ R α , and assume that x 1 a1 1 y 1 . Then y 1 ∈ a1 1 (x 1 ), hence there are a 2 ∈ Σ, y 2 ∈ a2 2 and β ∈ L such that (y 1 , y 2 ) ∈ R β and F (a 1 , a 2 , β) L α, but then also x 2 a2 2 y 2 . Assume that x 2 -→ 2 N 2 , then N 2 ∈ ♦ 2 (x 2 ). Hence there must be N 1 ∈ ♦ 1 (x 1 ) such that ∀(a 1 , y 1 ) ∈ N 1 : ∃(a 2 , y 2 ) ∈ N 2 , β ∈ L : (y 1 , y 2 ) ∈ R β , F (a 1 , a 2 , β) L α, but then also

1 , ∆ 1 ), N 2 = (X 2 , X 0 2 , ∆ 2 ) be νcalculus expressions in normal form, with DMTS translations nd(N 1 ) = (X 1 , X 0 1 , 1 , -→ 1 ) and nd(N 2 ) = (X 2 , X 0 2 , 2 , -→ 2 ). There is a DMTS refinement family R = {R α ⊆ X 1 × X 2 | α ∈ L} such that for all x 0 1 ∈ X 0 1 , there is x 0 2 ∈ X 0 2 for which (x 0 1 , x 0 2 ) ∈ R d L m (N1,N2) .

Let α ∈ L, (x 1 , x 2 ) ∈ R α , a 1 ∈ Σ, and y 1 ∈ a1 1 (x 1 ). Then x 1 a1 1 y 1 , hence we have x 2 a2 2 y 2 and β ∈ L so that (y 1 , y 2 ) ∈ R β and F (a 1 , a 2 , β) L α, but then also y 1 ∈ a2 2 (x 2 ). Let N 2 ∈ ♦ 2 (x 2 ), then also x 2 -→ 2 N 2 . Hence we must have x 1 -→ 1 N 1 with ∀(a 1 , y 1 ) ∈ N 1 : ∃(a 2 , y 2 ) ∈ N 2 , β ∈ L : (y 1 , y 2 ) ∈ R β , F (a 1 , a 2 , β) L α, but then also N 1 ∈ ♦ 1 (x 1 ).