Uli Fahrenberg

Axel Legay

General Quantitative Specification Theories with Modal Transition Systems

This paper proposes a new theory of quantitative specifications. It generalizes the notions of step-wise refinement and compositional design operations from the Boolean to an arbitrary quantitative setting. Using a great number of examples, it is shown that this general approach permits to unify many interesting quantitative approaches to system design.

Introduction

Specification theories permit reasoning about behaviors of systems at the abstract level, which is needed in various application such as abstraction-based model checking for programming languages, or compositional reasoning. Such specification theories generally come with (1) a satisfaction relation that allows to decide whether an implementation is a model of the specification, (2) a notion of refinement for determining the relationship between specifications and their sets of implementations, (3) a structural composition which, at the abstract level, mimics the behavioral composition of systems, (4) a quotient that allows to synthesize specifications from refinements, and (5) a logical composition that allows to compute intersections of sets of implementations.

Prominent among specification theories is the one of modal transition systems [30-32, 36, 40], which are labeled transition systems equipped with two types of transitions: must transitions that are mandatory for any implementation, and may transitions which are optional. In recent work [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF][START_REF] Bauer | A logic for accumulated-weight reasoning on multiweighted modal automata[END_REF][START_REF] Beneš | Dualpriced modal transition systems with time durations[END_REF][START_REF] Juhl | Modal transition systems with weight intervals[END_REF], modal transition systems have been extended by adding richer information to the usual discrete label set of transition systems, permitting to reason about quantitative aspects of models and specifications. These quantitative labels can be used to model and analyze e.g. timing [START_REF] David | Timed I/O automata: a complete specification theory for real-time systems[END_REF][START_REF] Henzinger | Quantifying similarities between timed systems[END_REF], resource usage [START_REF] Bauer | A logic for accumulated-weight reasoning on multiweighted modal automata[END_REF][START_REF] Illum Rasmussen | On using priced timed automata to achieve optimal scheduling[END_REF], or energy consumption [START_REF] Bouyer | Quantitative analysis of real-time systems using priced timed automata[END_REF][START_REF] Fahrenberg | Energy games in multiweighted automata[END_REF].

receive, [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Bauer | Moving from specifications to contracts in componentbased design[END_REF] deliver, [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] check, [0,[START_REF] Bauer | Weighted modal transition systems[END_REF] deliver, [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Alur | A theory of timed automata[END_REF] Fig. 1 Specification of a simple email system, with integer intervals modeling time constraints for performing the corresponding actions. In particular, [START_REF] Juhl | Modal transition systems with weight intervals[END_REF] extends modal transition systems with integer intervals and introduces corresponding extensions of the above operations which observe the added quantitative information, and [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF] generalizes this theory to general structured labels. Both theories are, however, fragile in the sense that they rely on Boolean notions of satisfaction and refinement: as refinement either holds or does not, they are unable to quantify the impact of small variations in quantities.

An example of a quantitative specification, taken from [START_REF] Bauer | Weighted modal transition systems[END_REF], is shown in Figure 1. The intuition is that any concrete implementation must be able to receive and deliver email, within one to three and one to four time units, respectively; but it also may be able to check incoming email, e.g. for viruses, before delivering it. No other behavior is permitted.

Figure 2 shows four different implementation candidates for the specification of Figure 1. The first candidate in Figure 2(a), however, has an error in the discrete structure: after receiving an email, it may check the email indefinitely. Hence it does not satisfy the specification. The second candidate, in Figure 2(b), is also problematic: not implementing the checking part of the specification is entirely permissible, but it takes too long to receive email. Thus, if the timing constraints are abstracted from, it is a perfectly good implementation; but the quantitative timing constraints are off. The implementation candidate in Figure 2(c) has similar problems, as it takes too long to deliver emails after checking them. The transition system in Figure 2(d) is, finally, a true implementation of the specification.

An important observation is, now, that even though the systems in Figures 2(b) and 2(c) strictly are not implementations of the email system specification, they conform much better to it than the system in Figure 2(a). Intuitively, they "almost" comply with the specification; given some other engineering constraints, they might indeed be considered "good enough" given the specification. It is, then, this "almost" and "good enough" which we shall attempt to formalize in this work.

Our point of view is, more generally speaking, that any quantitative specification formalism falls short with a Boolean notion of satisfaction and refinement. If the specification formalism is intended to model quantitative properties, then it is of little use to know that a proposed implementation does not precisely adhere to a specification; much more useful information is obtained by knowing how well it implements the specification, or how far it is deviating. Of course, the answer to this "how far" question might be ∞, due to discrete errors as in Figure 2(a); but in case it is finite, useful knowledge may be gained e.g. as to how much more implementation effort is needed, or whether one can satisfy oneself with this slightly imperfect implementation.

A first quantitative specification theory which is not fragile is introduced in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF][START_REF] Bauer | Weighted modal transition systems[END_REF]. This uses modal transition systems weighted with intervals as specifications, as in the examples in Figures 1 and2. Quantitative satisfaction and refinement are measured using a discounted accumulating distance, which adds up discrepancies between transition weights, but discounts them so that differences in the further future matter less than differences incurred early. Coming back to our examples, and with a discounting factor of .9, the satisfaction distances of the four implementations in Figure 2 to the specification in Figure 1 are ∞ for system 2(a), 5.3 for system 2(b), 3.0 for system 2(c), and 0 for system 2(d). It will of course depend on the concrete application how these numbers are interpreted, and whether a distance of 5.3 or 3.0 will be considered "good enough".

Pertaining to the application at hand, specifications may be better given using some other formalism than interval-weighted modal transition systems, and satisfaction and refinement may be more realistically measured using other distances than the one given above. For quantifying differences between systems (i.e. without paying attention to specifications), a number of different distances have been used in different contexts [START_REF] Černý | Simulation distances[END_REF][START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Doyen | Robustness of sequential circuits[END_REF][START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF][START_REF] Franck Van Breugel | A behavioural pseudometric for metric labelled transition systems[END_REF], so one should indeed expect the same need for variation with quantitative specification theories.

What is needed is, thus, a quantitative specification theory that is independent of both the specific labels and the distance used to measure differences; this is what we introduce in this paper. Using the concept of distance iterator function from [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF], we introduce a general notion of refinement distance between structured modal transition systems and a general quantitative specification theory. It turns out that there are some natural technical compatibility conditions relating the label composition operators with the distance which give rise to different properties of the specification theory.

We start out by introducing a general framework of quantitative refinement for quantitative specifications in Sections 2 and 3, together with a natural notion of quantitative relaxation of specifications. In Sections 4 and 5, we enrich this theory with generic operations which turn our framework into a complete specification theory in the sense of [START_REF] Bauer | Moving from specifications to contracts in componentbased design[END_REF]. These operations are as follows:

-Structural composition composes two specifications to mimic parallel composition at implementation level; the structural composition S T of two specifications S, T thus covers all parallel compositions of implementations of S with implemen-tations of T . In our quantitative setting, this is expressed by a quantitative independent implementability property, Theorem 2 on page 17: for all specifications S, T , S ′ , T ′ , the distance from S S ′ to T T ′ is bounded above by a uniform function P on the distances from S to T and from S ′ to T ′ . A prerequisite for our generic structural composition of specifications is a (partial) composition operator on labels which specifies which labels can synchronize, and what is the label produced by a synchronization. In the spirit of [START_REF] Winskel | Models for concurrency[END_REF], this covers the most common label synchronizations such as CCS or CSP. In order for quantitative independent implementability to hold, some reasonable assumptions on are necessary which are quantitative generalizations of standard properties [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]. One of these is that composition of labels respects the bound function P we have adhered to above: intuitively, for labels k, ℓ, k ′ , ℓ ′ , the distance from k ℓ to k ′ ℓ ′ needs to be bounded by P applied to the distances from k to ℓ and from k ′ to ℓ ′ . Note that this is a completely static property which can easily be decided upon.

-Quotient is the adjoint to structural composition, i.e. it is used to solve equations of the form S X ≡ T for X. This is useful for synthesizing partial specifications: if T is the specification of an overall system and S the specification of a part which has already been provided, then the quotient X = T S specifies the missing components. This is expressed by the universal property of quotient in Theorem 3 on page 20: for all specifications S, T and X, X refines T S if and only if S X refines T . (Universality of the property refers to the fact that if quotient exists, it is uniquely defined.)

To define quotient, one needs an operator on labels which is adjoint to . In order to extend quotient's universal property to the quantitative domain, we specify reasonable quantitative assumptions on the relation between and , more precisely, on the distance between m and ℓ k versus the one from k m to ℓ, for labels k, ℓ and m. Under these assumptions (more precisely, if is quantitatively exact as we will define it later), we can show that for all specifications S, T , X, the distance from X to T S equals the one from S X to T .

-Conjunction ∧ of specifications is used to obtain implementations which must comply with both of two specifications. Similarly to the operations above, its prerequisite is a conjunction operator on labels. It has been shown in [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF] that if is greatest lower bound for labels, then the operator ∧ is greatest lower bound for specifications. In order to generalize the properties of ∧ to the quantitative setting, we make an assumption of boundedness on , using a uniform bound function C similar to the function P for structural composition. Under this assumption, we can show in Theorem 4 on page 22 a quantitative generalization of the greatest lower bound property: for all specifications S, T , U , the distance from U to S ∧ T is bounded above by C applied to the distances from U to S and from U to T . Motivated by an example which shows that for a common instantiation of our framework, is not bounded, we also introduce a weaker variant of boundedness and show that also this can be lifted from labels to specifications (Theorem 5 on page 23).

Our general quantitative theory can be instantiated with a variety of different distances and operators, all useful for different applications; hence it can serve as a unifying framework for these applications. We develop one specific example in detail in the last section, using the modal event-clock automata of [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF][START_REF] Bertrand | Modal eventclock specifications for timed component-based design[END_REF][START_REF] Bertrand | Refinement and consistency of timed modal specifications[END_REF] for specifications and a distance suitable for real-time information. This maximum-lead distance, first introduced in [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF], is fundamentally different from the one used in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF][START_REF] Bauer | Weighted modal transition systems[END_REF], and so are the properties of the obtained quantitative specification theory. This shows the strength of our general approach.

Structured Modal Transition Systems

Labeled transition systems have long been established as the de-facto formalism for specifying formal semantics for discrete behavior and communication of programming languages and reactive systems. However, in order to capture meta-data and expectations about these, such as e.g. execution times of hardware platforms, cost of certain operations, or energy consumption, we require a richer formalism.

Labels and traces

We work with a poset Spec of specification labels with a partial order ⊑ Spec and denote by Spec ∞ = Spec * ∪ Spec ω the set of finite and infinite traces over Spec. In applications, Spec may be used to model data about the behavior of a system; for specifications this may be considered as legal parameters of operation, whereas for implementations it may be thought of as observed information.

The partial order ⊑ Spec is meant to model refinement of data; if k ⊑ Spec ℓ, then k is more refined (leaves fewer choices) than ℓ. The set

Imp = {k ∈ Spec | k ′ ⊑ Spec k =⇒ k ′ = k}
is called the set of implementation labels; these are the data which cannot be refined further. We let k = {k ′ ∈ Imp | k ′ ⊑ Spec k} and assume that k = ∅ for all k ∈ Spec.

Hemimetrics, pseudometrics and metrics

When k ⊑ Spec ℓ, we want to be able to quantify the impact of this difference in data on the systems in question, thus circumventing the fragility of the theory. To this end, we introduce a general notion of distance on sequences of data following the approach laid out in [START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF]. Before we can proceed however, we need to recall some terminology. Let | ≥0 ∪ {∞} denote the extended positive reals, let X be a set and

d : X × X → | ≥0 ∪ {∞}. Then d is called -a hemimetric if d(x, x) =
0 for all x ∈ X (indiscernibility of identicals) and d(x, y) + d(y, z) ≥ d(x, z) for all x, y, z ∈ X (triangle inequality); -a pseudometric if it is a hemimetric and additionally, d(x, y) = d(y, x) for all

x, y ∈ X (symmetry); -a metric if it is a pseudometric and additionally, d(x, y) = 0 implies x = y for all

x, y ∈ X (identity of indiscernibles)

As our (hemi-, pseudo-)metrics may take the values ∞, some authors will refer to them as extended (hemi-, pseudo-)metrics. Note that contrary to pseudometrics and metrics, hemimetrics are asymmetric distances: no relation is implied between d(x, y) and d(y, x). This will be useful for us, as we shall be considered with quantitative generalizations of preorders on specifications, which themselves by nature are asymmetric. Most of the distances we will consider are thus hemimetrics.

The symmetrization of a hemimetric d is the pseudometric d : X×X → | ≥0 ∪{∞} given by d(x, y) = max(d(x, y), d(y, x)); this is the smallest of all pseudometrics d ′ on X for which d ≤ d ′ . Given hemimetrics d on X and d ′ on another set X ′ , the product distance D on X × X ′ is defined by D((x, x ′ ), (y,

y ′ )) = d(x, y) + d(x ′ , y ′ ).
The Hausdorff hemimetric associated with a hemimetric d :

X × X → | ≥0 ∪ {∞} is the function d H : 2 X × 2 X → | ≥0 ∪ {∞} given for subsets A, B ⊆ X by d H (A, B) = sup x∈A inf y∈B d(x, y).
This is a well-known construction for metric spaces, cf. [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Munkres | Topology[END_REF]; there it is usually symmetrized and defined only for closed subsets, in which case it is a metric.

Trace distances

In order to build a framework for specification distances which is general enough to cover the distances commonly used, we introduce a notion of abstract trace distance which factors through a lattice on which it has a recursive characterization. We will show in Section 2.4 that this indeed covers the common scenarios.

Let M be an arbitrary set and ▲ = (| ≥0 ∪ {∞}) M the set of functions from M to the extended non-negative real line. Then ▲ is a complete lattice with partial order ⊑ ▲ given by α ⊑ ▲ β if and only if α(x) ≤ β(x) for all x ∈ M , and with an addition ⊕ ▲ given by (α ⊕ ▲ β)(x) = α(x) + β(x). The bottom element of ▲ is also the zero of ⊕ ▲ and given by ⊥ ▲ (x) = 0, and the top element is ⊤ ▲ (x) = ∞. We also define a metric on ▲ by d ▲ (α,

β) = sup x∈M |α(x) -β(x)|.
Intuitively, the lattice ▲ serves as a memory for more elaborate trace distances such as e.g. the limit-average distance, see Section 2.4. For simpler distances, it will suffice to let M = { * } be the one-point set and thus ▲ = | ≥0 ∪ {∞}. We extend the notions of hemimetrics, pseudometrics and metrics from above to mappings d :

X × X → ▲, by replacing in their defining properties 0 by ⊥ ▲ and + by ⊕ ▲ . Let d : Imp × Imp → ▲ be a hemimetric on implementation labels. We extend d to Spec by d(k, ℓ) = sup m∈ k inf n∈ ℓ d(m, n). Hence also this distance is asymmetric; the intuition is that any label in k has to be matched as good as possible in ℓ . Note that this is the Hausdorff hemimetric associated with d on implementation labels.

We will assume given an abstract trace distance d T : Spec ∞ × Spec ∞ → ▲ which is a hemimetric and has a recursive expression using a distance iterator function F : Imp × Imp × ▲ → ▲, see below. This will allow us to recover many of the system distances found in the literature, while preserving key results. We will need to assume that F satisfies the following properties:

(1) F is continuous in the first two coordinates: F (•, n, α) and F (m, •, α) are continuous functions Imp → ▲ for all α ∈ ▲.

(2) F is monotone in the third coordinate: F (m, n, •) : ▲ → ▲ is monotone for all m, n ∈ Imp.

(3) F extends d: for all m, n ∈ Imp, F (m, n, ⊥ ▲ ) = d(m, n).

(4) Indiscernibility of identicals: F (m, m, α) = α for all m ∈ Imp.

(5) An extended triangle inequality: for all m, n, o ∈ Imp and α, β, γ ∈ ▲ with α ⊕ ▲ β ⊒ ▲ γ, F (m, n, α) ⊕ ▲ F (n, o, β) ⊒ ▲ F (m, o, γ).

Note how the last two axioms are a generalization of the axioms for hemimetrics stated above.

We extend F to specification labels by defining

F (k, ℓ, α) = sup m∈ k inf n∈ ℓ F (m, n, α).
Then also the extended F : Spec × Spec × ▲ → ▲ is continuous in the first two and monotone in the third coordinates. Additionally, we assume that sets of implementation labels are closed with respect to F in the sense that for all k, ℓ ∈ Spec and

α ∈ ▲ with F (k, ℓ, α) = ⊤ ▲ , there are m ∈ k , n ∈ ℓ with F (m, ℓ, α) = F (k, n, α) = F (k, ℓ, α).
Note that this implies that the sets k are closed under the hemimetric d on Spec. Axioms (4) and (5) for F above now imply that for the extension, the following holds:

(4 ′ ) For all k, ℓ ∈ Spec with k ⊑ Spec ℓ and all α ∈ ▲, F (k, ℓ, α) = α. (5 ′ ) For all k, ℓ, m ∈ Spec and α, β, γ ∈ ▲ with α⊕ ▲ β ⊒ ▲ γ, F (k, ℓ, α)⊕ ▲ F (ℓ, m, β) ⊒ ▲ F (k, m, γ).
Let ε ∈ Spec ∞ denote the empty sequence, and for any sequence σ ∈ Spec ∞ , denote by σ 0 its first element and by σ 1 the tail of the sequence with the first element removed. We assume that d T has a recursive characterization, using F , as follows:

d T (σ, τ ) =      F (σ 0 , τ 0 , d T (σ 1 , τ 1 )) if σ, τ = ε, ⊤ ▲ if σ = ε, τ = ε or σ = ε, τ = ε, ⊥ ▲ if σ = τ = ε. (1)
We remark that a recursive characterization such as the one above is quite natural. Not only does it cover all commonly used trace distances (see the examples in the next section), but recursion is central to computing, and any trace distance without a recursive characterization would strike us as being quite artificial. It is precisely this recursive characterization which allows us to lift the trace distance to states of specifications in Definition 3 below, see also [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF] where this relation was discovered.

In applications (see below), the lattice ▲ comes equipped with a homomorphism g : ▲ → | ≥0 ∪ {∞} for which g(d T (σ, σ)) = 0 for all σ ∈ Spec ∞ . The actual trace distance of interest is then the composition dT = g • d T . The triangle inequality for F implies the usual triangle inequality for dT : dT (σ, τ ) + dT (τ, χ) ≤ dT (σ, χ) for all σ, τ, χ ∈ Spec ∞ , hence dT is a hemimetric on Spec ∞ . We need to work with distances which factor through ▲, instead of plainly taking values in | ≥0 ∪{∞}, because some distances which are useful in practice, as the ones in Examples 3 and 5 below, have no recursive characterization using ▲ = | ≥0 ∪{∞}. Whether the theory works for more general intermediate lattices than ▲ = (| ≥0 ∪ {∞}) M is an open question; we have had no occasion to use more general lattices in practice.

Examples

To give an application to the framework laid out above, we show here a few examples of specification labels and trace distances and how they fit into the framework. For a much more comprehensive application of the theory see Section 7. Example 1 A good example of a set of specification labels, introduced in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF], is given by Spec = Σ × ■, where Σ is a finite set of discrete labels and ■ = {[l, r] | l ∈ ) ∪ {-∞}, r ∈ ) ∪ {∞}, l ≤ r} is the set of extended-integer intervals. The partial order is defined by (a, [l, r]) ⊑ Spec (a ′ , [l ′ , r ′ ]) if and only if a = a ′ , l ′ ≤ l and r ′ ≥ r. Hence refinement is given by restricting intervals, so that

Imp = Σ ×{[x, x] | x ∈ )} ≈ Σ ×).
The implementation label distance is given by

d((a, x), (a ′ , x ′ )) = [c]|x -x ′ | if a = a ′ , ∞ otherwise, so that for specification labels (a, [l, r]), (a ′ , [l ′ , r ′ ]), d((a, [l, r]), (a ′ , [l ′ , r ′ ])) = sup m∈ (a,[l,r]) inf n∈ (a ′ ,[l ′ ,r ′ ]) d(m, n) = max(l ′ -l, r -r ′ , 0) if a = a ′ , ∞ otherwise. Now let ▲ = | ≥0 ∪{∞} and F (m, n, α) = d(m, n
)+λα for some fixed discounting factor λ ∈ | with 0 < λ < 1, then d T (σ, τ ) = j λ j d(σ j , τ j ) for implementation traces σ, τ of equal length. This distance hence accumulates individual distances on labels; it has been studied for weighted transition systems and games e.g. in [START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF][START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF][START_REF] Franck Van Breugel | A behavioural pseudometric for metric labelled transition systems[END_REF][START_REF] Zwick | The complexity of mean payoff games[END_REF]. The paper [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] then develops a complete specification theory around this specific distance; we will continue this example below to show how it fits in our present context.

Example 2 Using the same setting as above, with Spec = Σ × ■, (a, [l, r]) ⊑ Spec (a ′ , [l ′ , r ′ ]) if and only if a = a ′ , l ′ ≤ l and r ′ ≥ r, and d((a, x), (a ′ , x ′ )) = |xx ′ | if a = a ′ and ∞ otherwise, we can instantiate F to a point-wise instead of accumulating distance. Let again ▲ = | ≥0 ∪ {∞}, but F (m, n, α) = max(d(m, n), α). Then d T (σ, τ ) = sup j d(σ j , τ j ) for implementation traces σ, τ of equal length, hence measuring the biggest individual difference between the traces' symbols. This distance has been studied for weighted transition systems and games in [20-22, 37, 46] and other papers; we will also continue this example below to show how to develop a specification theory based on the point-wise distance.

Example 3 Again with the same instantiations of Imp and Spec as above, we can introduce limit-average distance. Here we let ▲ = (| ≥0 ∪ {∞}) ◆ , g : ▲ → | ≥0 ∪ {∞} given by g(α) = lim inf j α(j), and

F (m, n, α)(j) = 1 j+1 d(m, n) + j j+1 α(j -1), then dT (σ, τ ) = g(d T (σ, τ )) = lim inf j 1 j+1 j i=0 d(σ j , τ j )
for traces of equal length. This distance has been studied e.g. in [START_REF] Černý | Simulation distances[END_REF][START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF][START_REF] Zwick | The complexity of mean payoff games[END_REF]; we show below how it, in the framework of the present paper, gives a limit-average specification theory.

Let us give some intuition on why it is quite natural to use ▲ = (| ≥0 ∪ {∞}) ◆ for limit-average distance, and why the simple ▲ = | ≥0 ∪ {∞} does not work in this case. Essentially, when we move along the traces σ and τ to compute there distance, we have to sum up the individual distances d(σ i , τ i ). But the contribution of j i=0 d(σ j , τ j ) is divided by j +1 to compute the end result, hence we have to keep track of where in the traces we currently are for computing distance recursively. This is naturally achieved by remembering and increasing the index j during the recursion, which we do using M = ◆ and thus ▲ = (| ≥0 ∪ {∞}) ◆ .

Example 4 Examples 1 to 3 above are in a sense agnostic to the precise structure of implementation and specification labels. Indeed, the definitions only use the label distance d : Imp × Imp → | ≥0 ∪ {∞}, hence Imp (and Spec) can be any set. In particular, the theory put forward here (and also its specialization in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]) works equally well in a multi-weighted setting as e.g. in [START_REF] Fahrenberg | Energy games in multiweighted automata[END_REF], where

Imp = ) k , Spec = ■ k for some k ∈ ◆.
Example 5 With the same instantiations of Imp and Spec as in Examples 1 to 3, we can introduce a distance which, instead of accumulating individual label differences, measures the long-run difference between accumulated labels. This maximum-lead distance is especially useful for real-time systems and has been considered in [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF][START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF]. Unlike Examples 1 to 3, it does not use the distance d on implementation labels in the definition of the trace distance; rather it accumulates the labels itself before taking the distance.

Let ▲ = (| ≥0 ∪ {∞}) | and define F : Imp × Imp × ▲ → ▲ by F ((a, x), (a ′ , x ′ ), α)(δ) = [c]∞ if a = a ′ , max(|δ + x -x ′ |, α(δ + x -x ′ )) if a = a ′ .
Define g : ▲ → | ≥0 ∪ {∞} by g(α) = α(0); the maximum-lead distance assuming the lead is zero. It can then be shown that for implementation traces σ = ((a 0 , x 0 ), (a 1 , x 1 ), . . . ), τ = ((a 0 , y 0 ), (a 1 , y 1 ), . . . ),

dT (σ, τ ) = g(d T (σ, τ )) = sup m m i=0 x i - m i=0 y i
is precisely the maximum-lead distance of [START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF][START_REF] Henzinger | Quantifying similarities between timed systems[END_REF].

We note that, like for limit-average distance, the simple lattice ▲ = | ≥0 ∪ {∞} does not work for a recursive characterization of maximum-lead distance. This is due to the fact that during the computation of the distance from σ to τ , we have to keep track of the lead δ which we have accumulated until now, i.e. how much σ is ahead of τ ; this is precisely what we achieve by using M = | and thus ▲ = (| ≥0 ∪ {∞}) | .

We will come back to this example in Section 7 in the context of modal event-clock specifications and their robust semantics.

Example 6 Specification labels different from the ones above can e.g. be clock constraints, or zones [START_REF] Alur | A theory of timed automata[END_REF]. For a finite set Σ, let Spec = Φ(Σ) be the set of closed clock constraints over Σ given by

Φ(Σ) ∋ φ ::= a ≤ k | a ≥ k | φ 1 ∧ φ 2 (a ∈ Σ, k ∈ ◆, φ 1 , φ 2 ∈ Φ(Σ)).
Clock constraints have a natural partial order given by φ ⊑ Spec φ ′ iff φ =⇒ φ ′ . Implementation labels are then clock constraints which impose a precise value for each a ∈ Σ, which can be seen as functions u :

Σ → ◆. The natural distance between such discrete clock valuations is d(u, u ′ ) = max a∈Σ |u(a) -u ′ (a)
|, and on top of this, any interesting trace distance can be imposed using our framework.

Structured Modal Transition Systems

Definition 1

A structured modal transition system (SMTS) is a tuple (S, s 0 , S , -→ S ) consisting of a set S of states, an initial state s 0 ∈ S, and must and may transitions -→ S , S ⊆ S ×Spec×S for which it holds that for all

s k -→ S s ′ there is s ℓ S s ′ with k ⊑ Spec ℓ.
The last condition is one of consistency: everything which is required, is also allowed. If no confusion can arise, we will omit the subscripts S on the must and may transitions; we will also sometimes identify an SMTS (S, s 0 , S , -→ S ) with its state set S.

Intuitively, a may transition s k s ′ specifies that an implementation I of S is permitted to have a corresponding transition i m -→ i ′ , for any m ∈ k , whereas a must transition s ℓ -→ s ′ postulates that I is required to implement at least one corresponding transition i n -→ i ′ for some n ∈ ℓ . We will make this precise below.

An SMTS S is an implementation if -→ S = S ⊆ S × Imp × S;
hence in an implementation, all optional behavior has been resolved, and all data has been refined to implementation labels.

Definition 2 An SMTS (S, s 0 , S , -→ S ) is ▲-deterministic, for a given lattice ▲, if it holds for all s ∈ S, s k1 s 1 , s k2 s 2 for which there is k ∈ Spec with

d(k, k 1 ) = ⊤ ▲ and d(k, k 2 ) = ⊤ ▲ that k 1 = k 2 and s 1 = s 2 .
Note that for the Boolean label distance given by d(k, k ′ ) = ⊥ ▲ if k = k ′ and ⊤ ▲ otherwise, the above definition reduces to the property that if k 1 = k 2 , then also s 1 = s 2 , hence ▲-determinism is a generalization of usual determinism. In our quantitative case, we need to be more restrictive: not only do we not allow distinct transitions from s with the same label, but we forbid distinct transitions with labels which have a common quantitative refinement. Despite of this, we will generally omit the ▲ and say deterministic instead of ▲-deterministic.

Examples 1-3 (contd) For the label distance d((a, x), (a ′ , x ′ )) = |x -x ′ | if a = a ′
and ∞ otherwise of Examples 1 to 3 and 5, the above condition that there exist k ∈ Spec with d(k, k 1 ) = ⊤ ▲ and d(k, k 2 ) = ⊤ ▲ is equivalent, with k 1 = (a 1 , I 1 ) and k 2 = (a 2 , I 2 ), to saying that a 1 = a 2 , hence our notion of determinism agrees with the one of [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF].

A modal refinement of SMTS S, T is a relation R ⊆ S × T such that for any (s, t) ∈ R, -whenever s k S s ′ , then also t ℓ T t ′ for some k ⊑ Spec ℓ and (s ′ , t ′ ) ∈ R, -whenever t ℓ -→ T t ′ , then also s k -→ S s ′ for some k ⊑ Spec ℓ and (s ′ , t ′ ) ∈ R.
Thus any behavior which is permitted in S is also permitted in T , and any behavior required in T is also required in S. We write S ≤m T if there is a modal refinement

R ⊆ S × T with (s 0 , t 0 ) ∈ R.
The implementation semantics of a SMTS S is the set S = {I ≤m S | I is an implementation}, and we write S ≤ t T if S ⊆ T , saying that S thoroughly refines T . It follows by reflexivity of ≤m that S ≤m T implies S ≤ t T , hence modal refinement is a syntactic over-approximation of thorough refinement.

It can be shown for standard modal transition systems that S ≤ t T does not imply S ≤m T , unless T is deterministic, see [START_REF] Beneš | On determinism in modal transition systems[END_REF]. We shall provide a quantitative generalization of this result in Theorem 1 below. Also, modal refinement for MTS can be decided in polynomial time, whereas deciding thorough refinement is EXPTIMEcomplete [START_REF] Beneš | On determinism in modal transition systems[END_REF]. Essentially, thorough refinement-inclusion of implementation setsis the relation one really is interested in, but modal refinement provides a useful over-approximation.

Refinement Distances

We define two distances between SMTS, one at the syntactic and one at the semantic level.

Modal and thorough refinement distance

Definition 3

The modal refinement distance dm : S × T → ▲ between the states of SMTS S, T is defined to be the least fixed point to the equations

dm(s, t) = max        sup s k S s ′ inf t ℓ T t ′ F (k, ℓ, dm(s ′ , t ′ )), sup t ℓ -→ T t ′ inf s k -→ S s ′ F (k, ℓ, dm(s ′ , t ′ )).
We let dm(S, T ) = dm(s 0 , t 0 ), and we write S ≤ α m T if dm(S, T ) ⊑ ▲ α.

Lemma 1

The modal refinement distance is well-defined and a hemimetric. Also,

S ≤m T implies dm(S, T ) = ⊥ ▲ .
Proof Let I : ▲ S×T → ▲ S×T be the endofunction defined by

I(h)(s, t) = max        sup s k S s ′ inf t ℓ T t ′ F (k, ℓ, h(s ′ , t ′ )), sup t ℓ -→ T t ′ inf s k -→ S s ′ F (k, ℓ, h(s ′ , t ′ )).
The lattice ▲ S×T is complete because ▲ is, and I is monotone because F (k, ℓ, •) : ▲ → ▲ is. By an application of Tarski's fixed point theorem [START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF], I has a unique least fixed point which hence defines dm.

The property that dm(S, S) = 0 for all SMTS S is clear, and the triangle inequality dm(S, T ) ⊕ ▲ dm(T, U ) ⊒ ▲ dm(S, U ) can be shown inductively.

To show the last claim, assume s ≤m t. Then for any s k s ′ there is

t ℓ t ′ for which k ⊑ Spec ℓ, hence F (k, ℓ, α) = α for all α ∈ ▲ by Axiom (4 ′ ).
Similarly for must transitions, so the fixed point equations simplify to

dm(s, t) = max sup s s ′ inf t t ′ dm(s ′ , t ′ ), sup t-→t ′ inf s-→s ′ dm(s ′ , t ′ ) , the least fixed point of which is dm(s, t) = ⊥ ▲ . ⊓ ⊔
One can also define a linear distance between states, analogous to trace inclusion. This is given by

d T (s, t) = max sup σ∈Tr(s) inf τ ∈Tr(t) d T (σ, τ ), sup τ ∈Tr(t) inf σ∈Tr(s) d T (σ, τ ) ,
where Tr(s) denotes the set of (may or must) traces emanating from s. It can then be shown [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF] that d T (s, t) ⊑ ▲ dm(s, t) for all s, t ∈ S.

Definition 4

The thorough refinement distance from an SMTS S to an SMTS T is

d t (S, T ) = sup I∈ S inf J∈ T dm(I, J),
and we write

S ≤ α t T if d t (S, T ) ⊑ ▲ α.

Lemma 2

The thorough refinement distance is a hemimetric, and S ≤ t T implies

d t (S, T ) = ⊥ ▲ .
Proof The equality d t (S, S) = ⊥ ▲ is clear, and the triangle inequality d t (S, T ) +

d t (T, U ) ≥ d t (S, U ) follows like in the proof of [1, Lemma 3.72]. If S ≤ t T , then S ⊆ T implies d t (S, T ) = ⊥ ▲ . ⊓ ⊔

Refinement families

As is the case for ordinary (bi)simulation [START_REF] David | Concurrency and automata on infinite sequences[END_REF], there is a dual relational notion of refinement distance which is useful e.g. in proofs. Before we can introduce this, we need a notion similar to the finite branching assumption one needs to make for the case of bisimulation, cf. [START_REF] Milner | Communication and Concurrency[END_REF].

Definition 5 A SMTS S is said to be compactly branching if the sets {(s ′ , k) | s k s ′ }, {(s ′ , k) | s k -→ s ′ } ⊆ S × Spec are compact under the symmetrized product distance dm × d for every s ∈ S.
Recall that the pseudometric dm× d is given by dm× d((s, k), (s

′ , k ′ )) = dm(s, s ′ )+ d(k, k ′ ) = max(dm(s, s ′ ), dm(s ′ , s)) + max(d(k, k ′ ), d(k ′ , k)). We will need compact- ness of the sets {(s ′ , k) | s k s ′ }, {(s ′ , k) | s k -→ s ′ } ⊆ S ×
Spec for the property that continuous functions on defined on them attain their infimum and supremum, see Lemma 3 and its proof below.

The notion of compact branching was first introduced, for a formalism of metric transition systems, in [START_REF] Franck Van Breugel | A theory of metric labelled transition systems[END_REF]. It is a natural generalization of finite branching to a distance setting; we shall henceforth assume all our SMTS to be compactly branching. Definition 6 A modal refinement family from S to T , for SMTS S, T , is an ▲indexed family of relations R = {Rα ⊆ S × T | α ∈ ▲} with the property that for all α ∈ ▲ and all (s, t) ∈ Rα,

-whenever s k S s ′ , then there is β ∈ ▲ and (s ′ , t ′ ) ∈ R β for which t ℓ T t ′ and F (k, ℓ, β) ⊑ ▲ α, -whenever t ℓ -→ T t ′ , then there is β ∈ ▲ and (s ′ , t ′ ) ∈ R β for which s k -→ S s ′ and F (k, ℓ, β) ⊑ ▲ α.
Additionally we assume R to be closed in the sense that for all s ∈ S, t ∈ T , (s, t) ∈ R inf{α|(s,t)∈Rα} .

Lemma 3 For all SMTS S, T and α ∈ ▲, S ≤ α m T if and only if there is a modal refinement family R from S to T with (s 0 , t 0 ) ∈ Rα.

We say that a modal refinement family as in the lemma witnesses S ≤ α m T ; this is of course the same as saying that it witnesses dm(S, T ) ⊑ ▲ α, which we sometimes shorten to say that it witnesses dm(S, T ).

Proof Assume first that S ≤ α m T , thus we know that dm(S, T ) ⊑ ▲ α. We have to show that there is a modal refinement family R from S to T with (s 0 , t 0 ) ∈ Rα.

Define a family

R = {R α ′ ⊆ S × T | α ′ ∈ ▲} by R α ′ = {(s, t) | dm(s, t) ⊑ ▲ α ′ }
for every α ′ ∈ ▲; note that R is closed in the sense above. Now let β ∈ ▲ and

(s, t) ∈ R β .
-Assume s k s ′ . By dm(s, t) ⊑ ▲ β and the definition of dm(s, t) it follows that inft ℓ t ′ F (k, ℓ, dm(s ′ , t ′ )) ⊑ ▲ β. As T is compactly branching and F continuous, the set {F (k, ℓ, dm(s ′ , t ′ )) | t ℓ t ′ } is compact, hence there exists a transition

t ℓ t ′ such that F (k, ℓ, dm(s ′ , t ′ )) ⊑ ▲ β.
-Assume t ℓ -→ t ′ . By dm(s, t) ⊑ ▲ β and the definition of dm(s, t) it follows that

infs k -→s ′ F (k, ℓ, dm(s ′ , t ′ )) ⊑ ▲ β. Again {F (k, ℓ, dm(s ′ , t ′ )) | s k -→ s ′ } is a compact set, whence there exists a transition s k -→ s ′ such that F (k, ℓ, dm(s ′ , t ′ )) ⊑ ▲ β.
For the other direction, assume a refinement family R from S to T with (s

0 , t 0 ) ∈ Rα. Define h : S × T → ▲ by h(s, t) = inf{α | (s, t) ∈ Rα}. Then (s, t) ∈ R β implies that h(s, t) ⊑ ▲ β. Let s ∈ S and t ∈ T , then (s, t) ∈ R h(s,t) because R is closed, hence for all s k s ′ there is t ℓ t ′ and α ′ ∈ ▲ for which F (k, ℓ, α ′ ) ⊑ ▲ h(s, t)
and

(s ′ , t ′ ) ∈ R α ′ , implying h(s ′ , t ′ ) ⊑ ▲ α ′ and hence F (k, ℓ, h(s ′ , t ′ )) ⊑ ▲ h(s, t)
by monotonicity and transitivity. Similarly, for all

t ℓ -→ t ′ there is s k -→ s ′ with F (k, ℓ, h(s ′ , t ′ )) ⊑ ▲ h(s, t).
Hence h is a pre-fixed point for the equations in the definition of dm, implying that dm(s, t) ⊑ ▲ h(s, t) for all s ∈ S, t ∈ T , thus especially dm(s 0 , t 0 ) ⊑ ▲ α, because (s 0 , t 0 ) ∈ Rα implies h(s 0 , t 0 ) ⊑ ▲ α and dm(s 0 , t 0 ) ⊑ ▲ h(s 0 , t 0 ). ⊓ ⊔

Modal distance bounds thorough distance

The next theorem shows that the modal refinement distance overapproximates the thorough one, and that it is exact for deterministic SMTS. This is similar to the situation for standard modal transition systems [START_REF] Kim | Modal specifications[END_REF]; note [START_REF] Kim | Modal specifications[END_REF] that deterministic specifications generally suffice for applications.

Theorem 1 For all SMTS S, T , d t (S, T ) ⊑ ▲ dm(S, T ). If T is deterministic, then

d t (S, T ) = dm(S, T ).
The counterexample for the Boolean version of this result given in [START_REF] Beneš | On determinism in modal transition systems[END_REF] also works in our setting, to show that there exist (necessarily nondeterministic) SMTS S, T for which d t (S, T ) = ⊥ ▲ , but dm(S, T ) = ⊤ ▲ .

Proof If dm(S, T ) = ⊤ ▲ , we have nothing to prove. Otherwise, let R = {Rα ⊆ S ×T | α ∈ ▲} be a modal refinement family which witnesses dm(S, T ), then (s 0 , t 0 ) ∈ R dm(S,T ) . Let I ∈ S ; we will expose J ∈ T for which dm(I, J) ⊑ ▲ dm(S, T ).

Let R 1 ⊆ I × S be a witness for

I ≤m S, define R ′ α = R 1 • Rα ⊆ I × T for all α ∈ ▲, and let R ′ = {R ′ α | α ∈ ▲}.
We let the states of J be J = T , with j 0 = t 0 , and define J = -→ J as follows: For any i m -→ I i ′ and any t ∈ T for which

(i, t) ∈ R ′ α ∈ R ′ for some α ∈ ▲, α = ⊤ ▲ , we have t ℓ T t ′ with (i ′ , t ′ ) ∈ R ′ β ∈ R ′ for some β ∈ ▲ with F (m, ℓ, β) ⊑ ▲ α. As ℓ is closed under F , there is n ∈ ℓ for which F (m, n, β) = F (m, ℓ, β), and we add a transition t n -→ J t ′ to J.
Similarly, for any t ℓ -→ T t ′ and any i ∈ I for which

(i, t) ∈ R ′ α ∈ R ′ for some α ∈ ▲, α = ⊤ ▲ , we have i m -→ I i ′ with (i ′ , t ′ ) ∈ R ′ β for some β ∈ ▲ with F (m, ℓ, β) ⊑ ▲ α.
Using again closedness of ℓ , we find n ∈ ℓ for which F (m, n, β) = F (m, ℓ, β) and add a transition t n -→ J t ′ to J. We show that the identity relation

{(t, t) | t ∈ T } ⊆ J × T witnesses J ≤m T . Let first t n -→ J t ′ ;
we must have used one of the two constructions above for creating this transition. In the first case, there is t ℓ T t ′ with n ∈ ℓ , and in the second case, there is

t ℓ -→ T t ′ , hence also t ℓ ′ T t ′ with ℓ ⊑ Spec ℓ ′ , thus n ∈ ℓ ⊆ ℓ ′ . Now let t ℓ -→ T t ′ , then the second construction above has introduced t n -→ J t ′ with n ∈ ℓ .
To finish the proof, we show that the family R ′ is a witness for dm(I, J) ⊑ ▲ dm(S, T ). First,

(i 0 , s 0 ) ∈ R 1 and (s 0 , t 0 ) ∈ R dm(S,T ) imply (i 0 , t 0 ) ∈ R ′ dm(S,T ) . Let (i, t) ∈ R ′ α ∈ R ′ for some α ∈ ▲, α = ⊤ ▲ , and assume first i m -→ I i ′ . Then t ℓ T t ′ and t n -→ J t ′
by the first part of our above construction, and (i ′ , t ′ ) ∈ R ′ β with F (m, n, β) ⊑ ▲ F (m, ℓ, β) ⊑ ▲ α. For the converse, and transition t n -→ J t ′ must have been introduced above, and in both cases, i m

-→ I i ′ with (i ′ , t ′ ) ∈ R ′ β and F (m, n, β) ⊑ ▲ F (m, ℓ, β) ⊑ ▲ α.
Now to the proof of the second assertion of the theorem. If d t (S, T ) = ⊤ ▲ , we are done. Otherwise we inductively construct a relation family R = {Rα ⊆ S ×T | α ∈ ▲} which satisfies d t ((s, S), (t, T )) ⊑ α for any (s, t) ∈ Rα, as follows: Begin by letting Rα = {(s 0 , t 0 )} for all α ⊒ ▲ d t (S, T ), and let now (s, t) ∈ Rα with d t ((s, S), (t, T ))

⊑ α = ⊤ ▲ . Let s k S s ′ and t ℓ T t ′ such that d(k, ℓ) = ⊤ ▲ . Let (i ′ , I ′ ) ∈ (s ′ , S)
and m ∈ k , then there is (i, I) ∈ (s, S) for which i m -→ I i ′′ and (i ′′ , I) ≤m (i ′ , I ′ ). By the triangle inequality we have d t ((i, I), (t, T )) ⊑ ▲ d t ((i, I), (s, S)) ⊕ ▲ d t ((s, S), (t, T )) ⊑ ▲ α, hence there is t

ℓ ′ t ′′ for which d(m, ℓ ′ ) ⊑ ▲ α. But we also have d(m, ℓ) ⊑ ▲ d(m, k) ⊕ ▲ d(k, ℓ) = d(k, ℓ) = ⊤ ▲ , so by determinism of T it follows that ℓ = ℓ ′ and t ′ = t ′′ .
As m ∈ k was chosen arbitrarily above, we have

d(m, ℓ) ⊑ ▲ α for all m ∈ k , hence d(k, ℓ) = F (k, ℓ, ⊥ ▲ ) ⊑ α. Let B = {β ′ ∈ ▲ | F (k, ℓ, β ′ ) ⊑ ▲ α} and β = sup B, then F (k, ℓ, β) ⊑ ▲ α as ⊥ ▲ ∈ S. Add (s ′ , t ′ ) to Rγ for all γ ⊒ ▲ β.
We miss to show that d t ((s ′ , S), (t ′ , T )) ⊑ ▲ β. By d t ((s, S), (t, T )) ⊑ ▲ α we must have (j, J) ∈ (t, T ) , j n -→ J j ′ , and β ′ ∈ ▲ for which dm((i ′ , I ′ ), (j ′ , J)) ⊑ ▲ β ′ and

F (m, n, β ′ ) ⊑ ▲ α. Then F (k, ℓ, β ′ ) = F (m, ℓ, β ′ ) ⊑ ▲ F (m, n, β ′ ) ⊑ ▲ α, hence β ′ ∈ B, implying that d t ((s ′ , S), (t ′ , T )) ⊑ ▲ β ′ ⊑ ▲ β.
We show that R is a refinement family which witnesses dm(S, T ). Let (s, t) ∈ Rα ∈ R for some α ∈ ▲ and assume s k S s ′ . Let m ∈ k , then there is (i, I) ∈ (s, S) with i m -→ I i ′ . As d t ((i, I), (t, T )) ⊑ ▲ α, this implies that there is t ℓ T t ′ with d(m, ℓ) ⊑ ▲ α. Also for any other m ′ ∈ k we have t ℓ ′ T t ′′ with d(m, ℓ ′ ) ⊑ ▲ α, hence ℓ = ℓ ′ and t ′ = t ′′ by determinism. As m was chosen arbitrarily, we have

d(m, ℓ) ⊑ α for all m ∈ k , hence d(k, ℓ) = F (k, ℓ, ⊥ ▲ ) ⊑ α. By construction of R, (s ′ , t ′ ) ∈ R β for β = sup{β ′ ∈ ▲ | F (k, ℓ, β ′ ) ⊑ ▲ α}. Now assume t ℓ -→ T t ′ . Let (i, I) ∈ (s, S)
, then we have (j, J) ∈ (t, T ) with dm((i, I), (j, J)) ⊑ ▲ α. We must have j n -→ J j ′ with n ∈ ℓ , hence there are i m -→ I i ′ and β ′ ∈ ▲ with dm((i ′ , I), (j ′ , J)) ⊑ ▲ β ′ and F (m, n, β ′ ) ⊑ ▲ α.

The above considerations hold for all (i, I) ∈ (s, S) , hence there is k ∈ ▲

with m ∈ k , s k -→ S s ′ , and F (k, ℓ, β ′ ) = F (m, ℓ, β ′ ). But then F (k, ℓ, β ′ ) ⊑ ▲ F (m, n, β ′ ) ⊑ ▲ α, hence by construction of R, (s ′ , t ′ ) ∈ R β for β = sup{β ′ ∈ ▲ | F (k, ℓ, β ′ ) ⊑ ▲ α}. ⊓ ⊔

Quantitative relaxation

In a quantitative framework, it can be useful to be able to relax and strengthen specifications during the development process. Which precise relaxations and strengthenings one wishes to apply will depend on the actual application, but we can here show three general relaxations which differ from each other in the level of the theory at which they are applied. For α ∈ ▲ and SMTS S, T , -→ T t ′ , for k ⊑ Spec ℓ, d(ℓ, k) ⊑ ▲ α, and (s ′ , t ′ ) ∈ R;

-T is an α-widening of S if
-T is an α-relaxation of S if S ≤m T and T ≤ α m S;

the α-extended implementation semantics of S is

S +α = {I ≤ α m S | I implementation}.
Hence α-widening is an entirely syntactic notion: up to unweighted bisimulation, T is the same as S, but transition labels in T can be α "wider" than in S (hence also S ≤m T ). The second notion, α-relaxation, works at the level of semantics of specifications, whereas the last notion is at implementation level. A priori, there is no relation between the syntactic and semantic notions, even though one can be established in some special cases.

Examples 1-3 (contd) For the accumulated distance with discounting factor λ, any α-widening is also a (1λ) -1 α-relaxation. This is due to the fact that for traces σ, τ ∈ Spec ∞ with d(σ j , τ j ) ≤ α for all j, we have j λ j d(σ j , τ j ) ≤ j λ j α ≤

(1λ) -1 α by convergence of the geometric series, cf. [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF].

For the point-wise distance, it is easy to see that any α-widening is also an α-relaxation, and the same holds for the limit-average distance:

lim inf j 1 j+1 j i=0 d(σ i , τ i ) ≤ lim inf j 1 j+1 jα = α
Example 5 (contd) For the maximum-lead distance on the other hand, it is easy to expose cases of α-widenings which are not β-relaxations for any β. One example consists of two one-state SMTS S, T with loops s 0 a,1

-→ s 0 and t 0 a,[0,2] -→ t 0 ; then T is an α-widening of S for α(δ) = |δ + 1|, but dm(T, S) = ⊤ ▲ . Proposition 1 If T is an α-relaxation of S, then T ⊆ S +α .
It can be shown for special cases that the inclusion in the proposition is strict [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]; for its proof one only needs the fact that dm(I, S) ⊑ ▲ dm(I, T ) ⊕ dm(T, S) ⊑ ▲ α for all I ∈ T .

Also of interest is the relation between relaxations of different specifications. An easy application of the triangle inequality for dm shows that the distance between relaxations is bounded by the sum of the relaxation constants and the unrelaxed systems' distances:

Proposition 2 Let T be an α-relaxation of S and T ′ an α ′ -relaxation of S ′ . Then dm(T, T ′ ) ⊑ ▲ α ⊕ ▲ dm(S, S ′ ) and dm(T ′ , T ) ⊑ ▲ α ′ ⊕ ▲ dm(S ′ , S). ⊓ ⊔

Structural Composition and Quotient

We now introduce the different operations on SMTS which make up a specification theory. Firstly, we are interested in composing specifications S, S ′ into a specification S S ′ by synchronizing on shared actions. Secondly, we need a quotient operator which solves equations of the form S X ≡ T , that is, the quotient synthesizes the most general specification T S which describes all SMTS X satisfying the above equation.

Structural composition

To structurally compose SMTS, we assume given a generic partial label composition operator : Spec × Spec ֒→ Spec which specifies which labels can synchronize, cf. [START_REF] Winskel | Models for concurrency[END_REF]. We will need to assume the following property:

-for all ℓ, ℓ ′ ∈ Spec, (∃k ∈ Spec : d(k, ℓ) = ⊤ ▲ , d(k, ℓ ′ ) = ⊤ ▲ ) ⇐⇒ (∃m ∈ Spec : ℓ m, ℓ ′ m are defined).
This operator permits to compose labels at transitions which are executed in parallel; the property required relates composability to distances in such a way that two labels have a common quantitative refinement if and only if they have a common synchronization. This is quite natural and holds for all our examples, and is needed to relate determinism to composition in the proof of Theorem 3 below.

Additionally, we must assume that there exists a function P : ▲ × ▲ → ▲ which allows us to infer bounds on distances on synchronized labels. We assume that P is monotone in both coordinates, has P (⊥ ▲ , ⊥ ▲ ) = ⊥ ▲ , P (α, ⊤ ▲ ) = P (⊤ ▲ , α) = ⊤ ▲ for all α ∈ ▲, and that

F (k k ′ , ℓ ℓ ′ , P (α, α ′ )) ⊑ ▲ P (F (k, ℓ, α), F (k ′ , ℓ ′ , α ′ ))
for all k, ℓ, k ′ , ℓ ′ ∈ Spec and α, α ′ ∈ ▲ for which k k ′ and ℓ ℓ ′ are defined. Hence

d(k k ′ , ℓ ℓ ′ ) ⊑ ▲ P (d(k, ℓ), d(k ′ , ℓ ′ )
) for all such k, ℓ, k ′ , ℓ ′ ∈ Spec, thus P indeed bounds distances of synchronized labels.

Intuitively, P gives us a uniform bound on label composition: distances between composed labels can be bounded above using P and the individual labels' distances.

Definition 7

The structural composition of two SMTS S and T is the SMTS S T = (S × T, (s 0 , t 0 ), S T , -→ S T ) with transitions defined as follows:

s k S s ′ t ℓ T t ′ k ℓ defined (s, t) k ℓ S T (s ′ , t ′ ) s k -→ S s ′ t ℓ -→ T t ′ k ℓ defined (s, t) k ℓ -→ S T (s ′ , t ′ )
The next theorem shows that structural composition supports quantitative independent implementability: the distance between structural compositions can bounded above using P and the distances between the individual components.

Theorem 2 For SMTS S, T , S ′ , T ′ , with dm(S S ′ , T T ′ ) = ⊤ ▲ , dm(S S ′ , T T ′ ) ⊑ ▲ P (dm(S, T ), dm(S ′ , T ′ )).

Proof Let R = {Rα ⊆ S × T | α ∈ ▲}, R ′ = {R ′ α ⊆ S ′ × T ′ | α ∈ ▲} be witnesses for dm(S, T
) and dm(S ′ , T ′ ), respectively, and define

R β = {((s, s ′ ), (t, t ′ )) ∈ S × S ′ × T × T ′ | ∃α, α ′ ∈ ▲ : (s, t) ∈ Rα ∈ R, (s ′ , t ′ ) ∈ R ′ α ′ ∈ R ′ , P (α, α ′ ) ⊑ ▲ β}
for all β ∈ ▲. We show that R = {R β | β ∈ L} is a witness for dm(S S ′ , T T ′ ) ⊑ ▲ P (dm(S, T ), dm(S ′ , T ′ )).

First, ((s 0 , s ′ 0 ), (t 0 , t ′ 0 )) ∈ R P (dm(S,T ),dm(S ′ ,T ′ )) . Let now β ∈ ▲ \ {⊤ ▲ } and

((s, s ′ ), (t, t ′ )) ∈ R β ∈ R , then we have α, α ′ ∈ ▲ \ {⊤ ▲ } with (s, t) ∈ Rα ∈ R, (s ′ , t ′ ) ∈ R ′ α ′ ∈ R ′ , and P (α, α ′ ) ⊑ ▲ β. Let (s, s ′ ) k k ′ S S ′ (s, s′ ), then s k S s and s ′ k ′ S ′ s′ . As (s, t) ∈ Rα ∈ R, we have t ℓ T t and ᾱ ∈ ▲ with (s, t) ∈ Rᾱ ∈ R and F (k, ℓ, ᾱ) ⊑ ▲ α. Similarly, (s ′ , t ′ ) ∈ R ′ α ′ ∈ R ′ implies that there is t ′ ℓ ′ T ′ t′ and ᾱ′ ∈ ▲ with (s ′ , t′ ) ∈ R ′ ᾱ′ ∈ R ′ and F (k ′ , ℓ ′ , ᾱ′ ) ⊑ ▲ α ′ . Now if the composition ℓ ℓ ′ is undefined, then dm(S S ′ , T T ′ ) = ⊤ ▲ . If it is defined, then we have (t, t ′ ) ℓ ℓ ′ T T ′ ( t, t′ ) by definition of S S ′ . Also, ( t, t′ ) ∈ R P ( ᾱ, ᾱ′ ) ∈ R and F (k k ′ , ℓ ℓ ′ , P (ᾱ, ᾱ′ )) ⊑ ▲ P (F (k, ℓ, ᾱ), F (k ′ , ℓ ′ , ᾱ′ )) ⊑ ▲ P (α, α ′ ).
The reverse direction, assuming a transition (t, t ′ )

ℓ ℓ ′ -→ T T ′ ( t, t′ ), is similar. ⊓ ⊔
Example 1 (contd) One popular label synchronization operator for the set Spec = Σ × ■ from our examples, also used in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF], is given by adding interval boundaries, viz.

(a, [l, r]) (a ′ , [l ′ , r ′ ]) = (a, [l + l ′ , r + r ′ ]) if a = a ′ , undefined otherwise.
It can then be shown [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] that

d(k k ′ , ℓ ℓ ′ ) ≤ d(k, ℓ) + d(k ′ , ℓ ′ ) (2)
for all k, ℓ, k ′ , ℓ ′ ∈ Spec for which k k ′ and ℓ ℓ ′ are defined.

For the accumulating distance, (2) implies that is bounded above by P (α,

α ′ ) = α + α ′ : F (k k ′ , ℓ ℓ ′ , α + α ′ ) = d(k k ′ , ℓ ℓ ′ ) + λ(α + α ′ ) ≤ d(k, ℓ) + λα + d(k ′ , ℓ ′ ) + λα ′ = F (k, ℓ, α) + F (k ′ , ℓ ′ , α ′ )
Theorem 2 thus specializes to [4, Thm. 5]: dm(S S ′ , T T ′ ) ≤ dm(S, T ) + dm(S ′ , T ′ ) for all SMTS S, T, S ′ , T ′ .

Example 2 (contd) Also for the point-wise distance, a bound is given by P (α,

α ′ ) = α + α ′ : F (k k ′ , ℓ ℓ ′ , α + α ′ ) = max(d(k k ′ , ℓ ℓ ′ ), α + α ′ ) ≤ max(d(k, ℓ) + d(k ′ , ℓ ′ ), α + α ′ ) ≤ max(d(k, ℓ), α) + max(d(k ′ , ℓ ′ ), α ′ ) = F (k, ℓ, α) + F (k ′ , ℓ ′ , α ′ ),
the last inequality because of distributivity of addition over maximum. Thus also here, dm(S S ′ , T T ′ ) ≤ dm(S, T ) + dm(S ′ , T ′ ) for all SMTS S, T, S ′ , T ′ .

Example 3 (contd) For the limit-average distance, a similar bound P (α, α ′ ) = α ⊕ α ′ works: For all j ∈ ◆,

F (k k ′ , ℓ ℓ ′ , α ⊕ α ′ )(j) = 1 j+1 d(k k ′ , ℓ ℓ ′ ) + j j+1 (α(j -1) + α ′ (j -1)) ≤ 1 j+1 d(k, ℓ) + j j+1 α(j -1) + 1 j+1 d(k ′ , ℓ ′ ) + j j+1 α ′ (j -1) = F (k, ℓ, α)(j) + F (k ′ , ℓ ′ , α ′ )(j).
Hence also for the limit-average distance, dm(S S ′ , T T ′ ) ≤ dm(S, T ) + dm(S ′ , T ′ ) for all SMTS S, T, S ′ , T ′ .

In Section 7 we will introduce a different label synchronization operator with different properties.

Quotient

For quotients of SMTS, we need a partial label operator : Spec × Spec ֒→ Spec for which it holds that for all k, ℓ, m ∈ Spec, ℓ k is defined and m ⊑ Spec ℓ k if and only if k m is defined and k m ⊑ Spec ℓ;

for all ℓ, ℓ ′ ∈ Spec, (∃k ∈ Spec :

d(k, ℓ) = ⊤ ▲ , d(k, ℓ ′ ) = ⊤ ▲ ) ⇐⇒ (∃m ∈ Spec : m ℓ, m ℓ ′ are defined).
The first condition ensures that is adjoint to , and the second relates it to distances just as we did for above. Extending the first condition, we say that is quantitatively well-behaved if it holds for all k, ℓ, m ∈ Spec that ℓ k is defined and d(m, ℓ k) = ⊤ ▲ if and only if k m is defined and d(k m, ℓ) = ⊤ ▲ , and in that case, F (m, ℓ k, α) ⊒ ▲ F (k m, ℓ, α) for all α ∈ ▲, and that is quantitatively exact if the inequality can be sharpened to

F (m, ℓ k, α) = F (k m, ℓ, α).
Both of these are useful quantitative generalization of the adjunction between and ; we will see examples below of quantitatively exact label quotients and in Section 7 of a quantitatively well-behaved one.

In the definition of quotient below, we denote by ρ B (S) the pruning of a SMTS S with respect to the states in B ⊆ S, which is obtained as follows. Define a mustpredecessor operator pre : 2 S → 2 S by pre(S ′ ) = {s ∈ S | ∃k ∈ Spec, s ′ ∈ S ′ : s k -→ s ′ } and let pre * be the reflexive, transitive closure of pre. Then ρ B (S) exists if

s 0 / ∈ pre * (B), and in that case, ρ B (S) = (Sρ, s 0 , ρ, -→ρ) with Sρ = S \ pre * (B), ρ = ∩ (Sρ × Spec × Sρ), and -→ρ = -→ ∩ (Sρ × Spec × Sρ).
Definition 8 For SMTS S, T , the quotient of T by S is the SMTS T S = ρ B (T × S ∪ {u}, (t 0 , s 0 ), T S , -→ T S ) given as follows (if it exists):

t ℓ T t ′ s k S s ′ ℓ k defined (t, s) ℓ k T S (t ′ , s ′ ) t ℓ -→ T t ′ s k -→ S s ′ ℓ k defined (t, s) ℓ k -→ T S (t ′ , s ′ ) t ℓ -→ T t ′ ∀s k -→ S s ′ : ℓ k undefined (t, s) ∈ B m ∈ Spec ∀s k S s ′ : k m undefined (t, s) m T S u m ∈ Spec u m T S u
In the above definition, u is a new universal state from which everything is allowed and nothing required (last SOS rule). This state is reached from a quotient state (t, s) under label m whenever there is no may transition from s with whose label m can synchronize (next-to-last SOS rule), because in that case, any transition in the quotient will be canceled in the structural composition (cf. Theorem 3 below), and we need the quotient to be maximal. Similarly, if t specifies a must transition under a label ℓ which cannot be matched by any transition from s, then the quotient state (t, s) is inconsistent; hence we add it to B and remove it when pruning.

The next theorem shows that under certain standard conditions, quotient is sound and maximal with respect to structural composition. Theorem 3 Let S, T , X be SMTS such that S is deterministic and T S exists. Then X ≤m T S if and only if S X ≤m T . Also, -if is quantitatively well-behaved, then dm(X, T S) ⊒ ▲ dm(S X, T ); -if is quantitatively exact and dm(X, T S) = ⊤ ▲ , then dm(X, T S) = dm(S X, T ).

The (Boolean) property that X ≤m T S iff S X ≤m T implies uniqueness of quotient [START_REF] Fahrenberg | Make a difference! (Semantically)[END_REF]. For the quantitative generalizations, the property induced by a well-behaved means that distances to the quotient bound distances of structural compositions, which can be useful in further calculations; similarly for exact . Note that uniqueness implies that if a certain instantiation of our framework admits a quotient which is not quantitatively well-behaved, there is no hope that one can find another one which is.

Proof The proof that X ≤m T S if and only if S X ≤m T is in [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]. For the other properties, assume first to be quantitatively well-behaved; we show that dm(S X, T ) ⊑ ▲ dm(X, T S). If dm(X, T S) = ⊤ ▲ , there is nothing to prove, so assume dm(X, T S) = ⊤ ▲ and let R = {Rα ⊆ X × (T × S ∪ {u})} be a witness for

dm(X, T S). Define R ′ α = {((s, x), t) | (x, (t, s)) ∈ Rα} ⊆ S × X × T for all α ∈ ▲
and collect these to a family R ′ = {R ′ α | α ∈ ▲}. We show that R ′ is a witness for dm(S X, T ) ⊑ ▲ dm(X, T S).

We have

((s 0 , x 0 ), t 0 ) ∈ R ′ dm(X,T S) ∈ R ′ , so let α ∈ ▲ and ((s, x), t) ∈ R ′ α ∈ R ′ , and assume first that (s, x) k m S X (s ′ , x ′ ). Then s k S s ′ and x m X x ′ by definition of S X. Now (x, (t, s)) ∈ Rα ∈ R implies that there is (t, s) ℓ k ′ T S (t ′ , s ′′ ) and α ′ ∈ ▲ for which F (m, ℓ k ′ , α ′ ) ⊑ ▲ α and (x ′ , (t ′ , s ′′ )) ∈ R α ′ ∈ R. But then also ((s ′′ , x ′ ), t ′ ) ∈ R ′ α ∈ R ′ , hence k ′ m is defined and F (k ′ m, ℓ, α ′ ) ⊑ ▲ F (m, ℓ k ′ , α ′ ) ⊑ ▲ α.
Now k m and k ′ m being defined implies that there is k ′′ for which d(k ′′ , k) = ⊤ ▲ and d(k ′′ , k ′ ) = ⊤ ▲ , and by definition of T S, s

k ′ S s ′′ . As S is deterministic, this implies k = k ′ and s ′ = s ′′ . Hence ((s ′ , x ′ ), t ′ ) ∈ R ′ α ′ ∈ R ′ and F (k m, ℓ, α ′ ) ⊑ ▲ α.
Assume now that t ℓ -→ T t ′ . We must have s k -→ S s ′ for which ℓ k is defined, for otherwise (t, s) ∈ B and hence (t, s) would have been pruned in T S. Thus

(t, s) ℓ k -→ T S (t ′ , s ′ ), which by (x, (t, s)) ∈ Rα ∈ R implies that there is x m -→ X x ′ and α ′ ∈ ▲ for which F (m, ℓ k, α ′ ) ⊑ ▲ α and (x ′ , (t ′ , s ′ )) ∈ R α ′ ∈ R, hence ((s ′ , x ′ ), t ′ ) ∈ R ′ α ′ ∈ R ′ . But then k m is defined and F (k m, ℓ, α ′ ) ⊑ ▲ F (m, ℓ k, α ′ ) ⊑ ▲ α, and (s, x) k m -→ S X (s ′ , x ′ ).
Let now be quantitatively exact. To show that dm(X, T S) ⊑ ▲ dm(S X, T ), assume that dm(S X, T ) = ⊤ ▲ (otherwise there is nothing to prove), let R = {Rα ⊆ S × X × T | α ∈ ▲} be a witness for dm(S X, T ), and define

R ′ α = {(x, (t, s)) | ((s, x), t) ∈ Rα} ∪ {(x, u) | x ∈ X} ⊆ X × (T × S ∪ {u}) for all α ∈ ▲. We show that R ′ = {R ′ α | α ∈ ▲} is a witness for dm(X, T S) ⊑ ▲ dm(S X, T ). We have (x 0 , (t 0 , s 0 )) ∈ R ′ dm(S X,T ) ∈ R ′ . Let α ∈ ▲, (x, u) ∈ R ′ α ∈ R ′ and x m X x ′ , then also u m T S u, F (m, m, ⊥ ▲ ) ⊑ α, and (x ′ , u) ∈ R ′ ⊥ ▲ ∈ R ′ . Now let (x, (t, s)) ∈ R ′ α ∈ R ′ and x m X x ′ . If k m is undefined for all s k S s ′ , then by definition of T S, (t, s) m T S u, F (m, m, ⊥ ▲ ) ⊑ α, and (x ′ , u) ∈ R ′ ⊥ ▲ ∈ R ′ .
If there is a transition s k S s ′ for which k m is defined (by determinism there can be at most one), then also (s, x)

k m S X (s ′ , x ′ ). As ((s, x), t) ∈ Rα ∈ R, we must have t ℓ t ′ and α ′ ∈ ▲ with F (k m, ℓ, α ′ ) ⊑ ▲ α and ((s ′ , x ′ ), t ′ ) ∈ R α ′ ∈ R, hence (x ′ , (t ′ , s ′ )) ∈ R ′ α ′ ∈ R ′ .
Then ℓ k is defined and F (m, ℓ k, α ′ ) ⊑ ▲ α, and by definition of T S, (t, s)

ℓ k T S (t ′ , s ′ ). Now assume that (t, s) ℓ k -→ T S (t ′ , s ′ ), then t ℓ -→ T t ′ and s k -→ S s ′ by definition of T S. By ((s, x), t) ∈ Rα ∈ R, we have (s, x) k ′ m -→ S X (s ′′ , x ′ ) and α ′ ∈ ▲ with F (k ′ m, ℓ, α ′ ) ⊑ ▲ α and ((s ′′ , x ′ ), t ′ ) ∈ R α ′ ∈ R. This in turn implies that s k ′ -→ S s ′′ and x m -→ X s ′ by definition of S X. We also see that ℓ k ′ is defined, which by determinism of S entails k = k ′ and s ′ = s ′′ . Hence F (k m, ℓ, α ′ ) ⊑ ▲ α and (x ′ , (t ′ , s ′ )) ∈ R ′ α ′ ∈ R ′ . ⊓ ⊔
Examples 1-3 (contd) For the label synchronization operator for Spec = Σ × ■ given by adding interval boundaries, a quotient can be defined by

(a ′ , [l ′ , r ′ ]) (a, [l, r]) = (a, [l ′ -l, r ′ -r]) if a = a ′ and l ′ -l ≤ r ′ -r, undefined otherwise.
It can then be shown [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] that d(m, ℓ k) = d(k m, ℓ) for all k, ℓ, m ∈ Spec for which both ℓ k and k m are defined. From this it easily follows that both for the accumulating, the point-wise, and the limit-average distance, is quantitatively exact, hence for all three distances, Theorem 3 specializes to the theorem that dm(X, T S) = dm(S X, T ) for all SMTS S, T , X for which S is deterministic, T S exists and dm(X, T S) = ∞. For the accumulating distance, this is [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]Thm. 6].

Of course, different label synchronization operators give rise to different quotients with different properties; we refer again to Section 7.

Conjunction

Conjunction of SMTS can be used to merge two specifications into one. Let : Spec × Spec ֒→ Spec be a partial label operator for which it holds that for all k, ℓ ∈ Spec, if k ℓ is defined, then k ℓ ⊑ Spec k, k ℓ ⊑ Spec ℓ, and for all ℓ, ℓ ′ ∈ Spec, (∃k ∈ Spec :

d(k, ℓ) = ⊤ ▲ , d(k, ℓ ′ ) = ⊤ ▲ ) ⇐⇒ (∃m ∈ Spec : ℓ m, ℓ ′ m are defined).
The first requirement above ensures that conjunction acts as a lower bound, and the second one relates it to distances such that two labels have a common quantitative refinement if and only if they have a common conjunction. One also usually wants conjunction to be a greatest lower bound; we say that is conjunctively compositional if it holds for all k, ℓ, m ∈ Spec for which m ⊑ Spec k and m ⊑ Spec ℓ that also k ℓ is defined and m ⊑ Spec k ℓ.

As a quantitative generalization, and analogously to what we did for structural composition, we say that is conjunctively bounded by a function C : ▲×▲ → ▲ if C is monotone in both coordinates, has C(⊥ ▲ , ⊥ ▲ ) = ⊥ ▲ , C(α, ⊤ ▲ ) = C(⊤ ▲ , α) = ⊤ ▲ for all α ∈ ▲, and if it holds for all k, ℓ, m ∈ Spec for which d(m, k) = ⊤ ▲ and d(m, ℓ) = ⊤ ▲ that k ℓ is defined and

F (m, k ℓ, C(α, α ′ )) ⊑ ▲ C(F (m, k, α), F (m, ℓ, α ′ ))
for all α, α ′ ∈ ▲. Note that this implies that d(m, k ℓ) ⊑ ▲ C(d(m, k), d(m, ℓ)), hence conjunctive boundedness implies conjunctive compositionality. Like P for structural composition, C gives a uniform bound on label conjunction.

Definition 9

The conjunction of two SMTS S and T is the SMTS S ∧ T = ρ B (S × T, (s 0 , t 0 ), S∧T , -→ S∧T ) given as follows:

s k -→ S s ′ t ℓ T t ′ k ℓ defined (s, t) k ℓ -→ S∧T (s ′ , t ′ ) s k S s ′ t ℓ -→ T t ′ k ℓ defined (s, t) k ℓ -→ S∧T (s ′ , t ′ ) s k S s ′ t ℓ T t ′ k ℓ defined (s, t) k ℓ S∧T (s ′ , t ′ ) s k -→ S s ′ ∀t ℓ T t ′ : k ℓ undef. (s, t) ∈ B t ℓ -→ T t ′ ∀s k S s ′ : k ℓ undef. (s, t) ∈ B
Note that like for quotient, conjunction of SMTS may give inconsistent states which need to be pruned away after. As seen in the last two SOS rules above, this is the case when one SMTS specifies a must transition which the other SMTS cannot synchronize with. Hence, the demand on implementations of the conjunction is that they simultaneously must and cannot have a transition, which of course is unsatisfiable.

The next theorem shows the precise conditions under which conjunction is a greatest lower bound. Note that the greatest-lower-bound condition U ≤m S, U ≤m T =⇒ U ≤m S ∧ T entails uniqueness. Theorem 4 Let S, T , U be SMTS. If S ∧ T is defined, then S ∧ T ≤m S and S ∧ T ≤m T . If, additionally, S or T are deterministic, then:

-If is conjunctively compositional, U ≤m S, and U ≤m T , then S ∧ T is defined and U ≤m S ∧ T . -If is conjunctively bounded by C, dm(U, S) = ⊤ ▲ , and dm(U, T ) = ⊤ ▲ , then S ∧ T is defined and dm(U, S ∧ T ) ⊑ ▲ C(dm(U, S), dm(U, T )).

Proof The proof of the two first claims is in [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]. For the third claim, let

R = {Rα ⊆ U × S | α ∈ ▲} and R ′ = {R ′ α ⊆ U × T | α ∈ ▲} be relation families witnessing dm(U, S) and dm(U, T ), respectively, define R ∧ β = {(u, (s, t)) | ∃α, α ′ ∈ ▲ : (u, s) ∈ Rα, (u, t) ∈ R ′ α ′ , C(α, α ′ ) ⊑ ▲ β} ⊆ U ×S×T for all β ∈ ▲, and let R ∧ = {R ∧ β | β ∈ ▲}.
We show that R ∧ is a witness for dm(U, S ∧ T ) ⊑ ▲ C(dm(U, S), dm(U, T )).

We have (u 0 , (s

0 , t 0 )) ∈ R ∧ C(dm(U,S),dm(U,T )) ∈ R ∧ . Let β ∈ ▲ \ {⊥ ▲ } and (u, (s, t)) ∈ R ∧ β ∈ R ∧ , then we have α, α ′ ∈ ▲ \ {⊥ ▲ } with (u, s) ∈ Rα ∈ R, (u, t) ∈ R ′ α ′ ∈ R ′ , and C(α, α ′ ) ⊑ ▲ β. Assume u m U u ′ , then there exist s k S s ′ and ᾱ ∈ ▲ for which (u ′ , s ′ ) ∈ Rᾱ ∈ R and F (m, k, ᾱ) ⊑ ▲ α, and similarly t ℓ T t ′ and ᾱ′ with (u ′ , t ′ ) ∈ R ′ ᾱ′ ∈ R ′ and
F (m, ℓ, ᾱ′ ) ⊑ α ′ . Then d(m, k) = ⊤ ▲ and d(m, ℓ) = ⊤ ▲ , so by conjunctive bounded- ness k ℓ is defined, and (s, t)

k ℓ S∧T (s ′ , t ′ ) by definition of S∧T . Also, (u ′ , (s ′ , t ′ )) ∈ R ∧ C( ᾱ, ᾱ′ ) ∈ R ∧ and F (m, k ℓ, C(ᾱ, ᾱ′ )) ⊑ ▲ C(F (m, k, ᾱ), F (m, ℓ, ᾱ′ )) ⊑ ▲ C(α, α ′ ). Assume (s, t) k ℓ -→ S∧T (s ′ , t ′ ), then s k -→ S s ′ and t ℓ -→ T t
′ by definition of S ∧ T . We can without loss of generality postulate that T is deterministic. The fact that (u, s) ∈ Rα ∈ R implies that there are u m -→ U u ′ and ᾱ ∈ ▲ for which

(u ′ , s ′ ) ∈ Rᾱ ∈ R and F (m, k, ᾱ) ⊑ ▲ α. We must also have u m ′ U u ′ for some m ′ ⊒ Spec m, and then (u, t) ∈ R ′ ᾱ ∈ R ′ implies that there exist t ℓ ′ T t ′′ and ᾱ′ ∈ ▲ with (u ′ , t ′′ ) ∈ R ′ ᾱ′ ∈ R ′ and F (m ′ , ℓ ′ , ᾱ′ ) ⊑ ▲ α ′ . The triangle inequality for F gives F (m, ℓ ′ , ᾱ′ ) ⊑ ▲ F (m, m ′ , ⊥ ▲ )⊕F (m ′ , ℓ ′ , ᾱ′ ) ⊑ ▲ α ′ , hence d(m, ℓ ′ ) = ⊤ ▲ .
Together with d(m, k) = ⊤ ▲ , conjunctive boundedness al- lows us to conclude that k ℓ ′ is defined, but then both k ℓ and k ℓ ′ are defined, hence by determinism of T , ℓ = ℓ ′ and t ′ = t ′′ . ⊓ ⊔ Examples 1-3 (contd) For the set Spec = Σ × ■ from our examples, the unique compositional conjunction operator on is given, on labels, by intersection of intervals [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]:

(a, [l, r]) (a ′ , [l ′ , r ′ ]) = (a, [max(l, l ′ ), min(r, r ′ )]) if a = a ′ , max(l, l ′ ) ≤ min(r, r ′ ), undefined otherwise.
We can easily show that is not conjunctively bounded: with m = (a, [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | A theory of timed automata[END_REF]), k = (a, [0, 1]) and ℓ = (a, [START_REF] Bauer | Moving from specifications to contracts in componentbased design[END_REF][START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]), d(m, k) = d(m, ℓ) = 1, but k ℓ is not defined. Noting that this statement does not involve the distance iterator F , we conclude that neither accumulating, point-wise nor limit-average distance admit a bounded conjunction operator. For the accumulating distance, this statement is [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]Thm. 4].

To deal with the problem that, as in the above example, conjunction may not be conjunctively bounded, we introduce another, weaker, property which ensures some compatibility of conjunction with distances. We say that is relaxed conjunctively bounded by a function C : ▲ × ▲ → ▲ if C is monotone in both coordinates, has C(⊥ ▲ , ⊥ ▲ ) = ⊥ ▲ , C(α, ⊤ ▲ ) = C(⊤ ▲ , α) = ⊤ ▲ for all α ∈ ▲, and such that for all k, ℓ ∈ Spec for which there is m ∈ Spec with d(m, k) = ⊤ ▲ and d(m, ℓ) = ⊤ ▲ , there

exist k ′ , ℓ ′ ∈ Spec with k ′ ℓ ′ defined, k ⊑ Spec k ′ , ℓ ⊑ Spec ℓ ′ , d(k ′ , k) = ⊤ ▲ , and d(ℓ ′ , ℓ) = ⊤ ▲ , such that for all m ′ ∈ Spec, α, α ′ ∈ ▲, F (m ′ , k ′ ℓ ′ , C(α, α ′ )) ⊑ ▲ C(F (m ′ , k, α), F (m ′ , ℓ, α ′ )). (3)
The following theorem shows that relaxed boundedness of entails a similar property for SMTS conjunction.

Theorem 5 Let S, T be SMTS with S or T deterministic and relaxed conjunctively bounded by C. If there is an SMTS U for which dm(U, S) = ⊤ ▲ and dm(U, T ) = ⊤ ▲ , then there exist β-and γ-widenings S ′ of S and T ′ of T for which S ′ ∧ T ′ is defined, and such that dm(U ′ , S ′ ∧ T ′ ) ⊑ ▲ C(dm(U ′ , S), dm(U ′ , T )) for all

SMTS U ′ .
Proof We start by constructing S ′ and T ′ , almost as in the proof of the third claim of Theorem 4. The states of S ′ and T ′ will be the same as for S and T , and we start by letting

β = ⊥ ▲ , γ = ⊥ ▲ . Let U fulfill dm(U, S) = ⊤ ▲ and dm(U, T ) = ⊤ ▲ , let R = {Rα ⊆ U × S | α ∈ ▲} and R ′ = {R ′ α ⊆ U × T | α ∈ ▲} be relation families witnessing dm(U, S) and dm(U, T ), respectively, define R ∧ η = {(u, (s, t)) | ∃α, α ′ ∈ ▲ : (u, s) ∈ Rα, (u, t) ∈ R ′ α ′ , C(α, α ′ ) ⊑ ▲ η} ⊆ U × S × T for all η ∈ ▲, and let R ∧ = {R ∧ η | η ∈ ▲}. Now let η ∈ ▲ \ {⊤ ▲ } and (u, (s, t)) ∈ R ∧ η ∈ R ∧ , then we have α, α ′ ∈ ▲ \ {⊥ ▲ } with (u, s) ∈ Rα ∈ R, (u, t) ∈ R ′ α ′ ∈ R ′ , and C(α, α ′ ) ⊑ ▲ η. Let u m U u ′ , then also s k S s ′ and t ℓ T t ′ ,
and there are ᾱ, ᾱ′ ∈ ▲ \ {⊤ ▲ } with F (m, k, ᾱ) ⊑ ▲ α and F (m, ℓ, ᾱ′ ) ⊑ ▲ α ′ . Hence d(m, k) = ⊤ ▲ and d(m, ℓ) = ⊤ ▲ , and by relaxed conjunctive boundedness we have k

′ , ℓ ′ ∈ Spec with k ⊑ Spec k ′ , ℓ ⊑ Spec ℓ ′ , d(k ′ , k) = ⊤ ▲ , d(ℓ ′ , ℓ) = ⊤ ▲ , and k ′ ℓ ′ defined. We add the transitions s k ′ S ′ s ′ , t ℓ ′ T ′ t ′ to S ′ and T ′ and update β := max(β, d(k ′ , k)), γ := max(γ, d(ℓ ′ , ℓ)).

As the sets

{k ∈ Spec | s k S s ′ }, {ℓ ∈ Spec | t ℓ T t ′ }
are compact, the above process converges to some β, γ = ⊤ ▲ . The must transitions we just copy from S to S ′ and from T to T ′ , and then S ′ is a β-widening of S and T ′ is a γ-widening of T .

We must show that S ′ and T ′ satisfy the properties claimed. By construction S ′ ∧ T ′ is defined, so let U ′ be an SMTS with dm(U ′ , S) = ⊤ ▲ and dm(U ′ , T ) = ⊤ ▲ (otherwise we have nothing to prove). We must show that dm(U ′ , S ′ ∧ T ′ ) ⊑ ▲

C(dm(U ′ , S), dm(U ′ , T )). Let R = {Rα ⊆ U ′ × S | α ∈ ▲} and R ′ = {R ′ α ⊆ U ′ × T |
α ∈ ▲} be relation families witnessing dm(U ′ , S) and dm(U ′ , T ), respectively, define

R ∧ ′ η = {(u ′ , (s, t)) | ∃α, α ′ ∈ ▲ : (u ′ , s) ∈ Rα, (u ′ , t) ∈ R ′ α ′ , C(α, α ′ ) ⊑ ▲ η} ⊆ U ′ × S ×
T for all η ∈ ▲, and let

R ∧ ′ = {R ∧ ′ η | η ∈ ▲}.
We have

(u ′ 0 , (s 0 , t 0 )) ∈ R ∧ ′ C(dm(U ′ ,S),dm(U ′ ,T )) ∈ R ∧ ′ . Let η ∈ ▲ \ {⊥ ▲ } and (u ′ , (s, t)) ∈ R ∧ ′ η , then we have α, α ′ ∈ ▲ \ {⊥ ▲ } with (u ′ , s) ∈ Rα ∈ R, (u ′ , t) ∈ R ′ α ′ ∈ R ′ , and C(α, α ′ ) ⊑ ▲ η. Let u ′ m U ′ u ′′ , then also s k S s ′ and t ℓ T t ′ , and there are ᾱ, ᾱ′ ∈ ▲ \ {⊤ ▲ } with (u ′′ , s ′ ) ∈ Rᾱ, (u ′′ , t ′ ) ∈ R ′ ᾱ′ , F (m, k, ᾱ) ⊑ ▲ α, and F (m, ℓ, ᾱ′ ) ⊑ ▲ α ′ .
By construction of S ′ and T ′ , we have s

k ′ S ′ s ′ and t ℓ ′ T ′ t ′ with k ⊑ Spec k ′ , ℓ ⊑ Spec ℓ ′ , d(k ′ , k) ⊑ ▲ β,
and d(ℓ ′ , ℓ) ⊑ ▲ γ, and such that k ′ ℓ ′ is defined. Also,

(u ′′ , (s ′ , t ′ )) ∈ R ∧ ′ C( ᾱ, ᾱ′ ) and F (m, k ′ ℓ ′ , C(ᾱ, ᾱ′ )) ⊑ ▲ C(F (m, k, ᾱ), F (m, ℓ, ᾱ′ )) ⊑ ▲ C(α, α ′ ).
The other direction of the proof, starting with a transition (s, t)

k ℓ -→ S ′ ∧T ′ (s ′ , t ′ )
, is an exact copy of the corresponding part of the proof of Theorem 4. ⊓ ⊔ Example 1 (contd) For the set Spec = Σ × ■ from our examples, the following lemma shows a one-step version of relaxed conjunctive boundedness.

Lemma 4 For all

k, ℓ ∈ Spec for which there is m ∈ Spec with d(m, k) = ∞ and d(m, ℓ) = ∞, there exist k ′ , ℓ ′ ∈ Spec with k ⊑ Spec k ′ , ℓ ⊑ Spec ℓ ′ , d(k ′ , k) = ∞, d(ℓ ′ , ℓ) = ∞, and k ′ ℓ ′ defined, and then d(m ′ , k ′ ℓ ′ ) ≤ max(d(m ′ , k), d(m ′ , ℓ)) for all m ′ ∈ Spec. Proof Let k, ℓ ∈ Spec such that there is m ∈ Spec with d(m, k) = ∞ and d(m, ℓ) = ∞.
This implies that k = (a, [l, r]) and ℓ = (a, [l ′ , r ′ ]) for some a ∈ Σ, k, l, k ′ , l ′ ∈ ) ∪ {-∞, ∞}. Without loss of generality we can assume that l ≤ l ′ .

If r ≥ l ′ , then k ℓ = (a, [l ′ , r]) is defined, and we take k ′ = k, ℓ ′ = ℓ. Now let m ′ = (a ′ , [l ′′ , r ′′ ]) ∈ Spec. If a ′ = a, the property to prove is trivially true. If a ′ = a, then we have

d(m ′ , k ′ ℓ ′ ) = max(0, l ′ -l ′′ , r ′′ -r), d(m ′ , k) = max(0, l -l ′′ , r ′′ -r), d(m ′ , ℓ) = max(0, l ′ -l ′′ , r ′′ -r ′ ).
Thus we need to show that max(0, l ′l ′′ , r ′′r) ≤ max(0, ll ′′ , r ′′r, l ′l ′′ , r ′′r ′ ), which is clear as all left-hand terms also appear on the right-hand side.

In case r < l ′ , we let

k ′ = (a, [l, l ′ ]) and ℓ ′ = (a, [r, r ′ ]). Then k ⊑ Spec k ′ , ℓ ⊑ Spec ℓ ′ , and k ′ ℓ ′ = (a, [r, l ′ ]) is defined. Also, d(k ′ , k) = d(ℓ ′ , ℓ) = l ′ -r = ∞.
Let m ′ = (a ′ , [l ′′ , r ′′ ]) as before, then the case a ′ = a is again trivial. We have

d(m ′ , k ′ ℓ ′ ) = max(0, r -l ′′ , r ′′ -l ′ ),
so we need to show that

max(0, r -l ′′ , r ′′ -l ′ ) ≤ max(0, l -l ′′ , r ′′ -r, l ′ -l ′′ , r ′′ -r ′ ) = max(0, r ′′ -r, l ′ -l ′′ ),
where the equality follows from l ≤ l ′ , hence ll ′′ ≤ l ′l ′′ , and r ≤ r ′ , hence r ′′ -r ′ ≤ r ′′ -r. But 0 ≤ l ′r, rl ′′ < l ′ = l ′′ , and r ′′l ′ < r ′′r because of r < l ′ , so the inequality follows. ⊓ ⊔

For the accumulating distance, it then follows that is relaxed conjunctively bounded by C(α, α ′ ) = α + α ′ : Using the notation from Lemma 4, we need to show [START_REF] Bauer | Moving from specifications to contracts in componentbased design[END_REF]

, i.e. that d(m ′ , l ′ ℓ ′ ) + λ(α + α ′ ) ≤ d(m ′ , k) + λα + d(m ′ , ℓ) + λα ′ , which however is clear by d(m ′ , k ′ ℓ ′ ) ≤ max(d(m ′ , k), d(m ′ , ℓ)) ≤ d(m ′ , k) + d(m ′ , ℓ).
Example 2 (contd) For the pointwise distance, is relaxed conjunctively bounded by C(α, α ′ ) = max(α, α ′ ): (3) is then equivalent to max(d(m ′ , k ′ ℓ ′ ), α, α ′ ) ≤ max(d(m ′ , k), d(m ′ , ℓ), α, α ′ ), which follows from Lemma 4.

Example 3 (contd) For the limit-average distance, is relaxed conjunctively bounded by C(α, α ′ ) = α⊕ ▲ α ′ : Again using the notation from Lemma 4, we need to show (3), so we need to see that for all j ∈ ◆ + , 1

j+1 d(m ′ , k ′ ℓ ′ )+ j j+1 α(j -1)+ j j+1 α ′ (j -1) ≤ 1 j+1 d(m ′ , k) + j j+1 α(j -1) + 1 j+1 d(m ′ , ℓ) + j j+1 α ′ (j -1). This follows again from d(m ′ , k ′ ℓ ′ ) ≤ max(d(m ′ , k), d(m ′ , ℓ)) ≤ d(m ′ , k) + d(m ′ , ℓ).

Logical Characterizations

We show that quantitative refinement admits a logical characterization. Our results extend the logical characterization of modal transition systems in [START_REF] Kim | Modal specifications[END_REF]. Our logic L is the smallest set of expressions generated by the following abstract syntax:

φ, φ 1 , φ 2 := tt | ff | ℓ φ | [ℓ]φ | φ 1 ∧ φ 2 | φ 1 ∨ φ 2 (ℓ ∈ Spec)
The semantics of a formula φ ∈ L is a mapping φ@ : S → ▲ given inductively as follows:

tt@s = ⊥ ff @s = ⊤ (φ 1 ∧ φ 2 )@s = max(φ 1 @s, φ@ 2 s) (φ 1 ∨ φ 2 )@s = min(φ 1 @s, φ 2 @s)

ℓ φ@s = inf{F (k, ℓ, φ@t) | s k -→ t, d(k, ℓ) = ⊤ ▲ } [ℓ]φ@s = sup{F (k, ℓ, φ@t) | s k t, d(k, ℓ) = ⊤ ▲ }
For a SMTS S we write φ@S = φ@s 0 . The below theorems express the fact that L is quantitatively sound for refinement distance, i.e. the value of a formula in a specification is bounded by its value in any other specification together with their distance, and that the disjunction-free fragment of L is quantitatively implementation complete, i.e. the value of any disjunction-free formula in a specification S is bounded above by its value in any implementation of S. Note that disjunction-freeness is a very common assumption in this context, cf. [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF].

Theorem 6 For all φ ∈ L and all SMTS S, T , φ@S ⊑ ▲ φ@T ⊕ ▲ dm(S, T ).

Proof Structural induction. The claim obviously holds for φ = tt and φ = ff ; if φ = φ 1 ∧ φ 2 , then φ i @s 1 ⊑ ▲ φ i @s 2 ⊕ ▲ dm(s 1 , s 2 ) for i = 1, 2 imply that also max(φ 1 @s 1 , φ 2 @s 1 ) ⊑ ▲ max(φ 1 @s 2 , φ 2 @s 2 ) ⊕ ▲ dm(s 1 , s 2 ), and similarly for φ =

φ 1 ∨ φ 2 .
For the case φ = ℓ φ ′ , there is nothing to prove if there are no transitions

s 2 -→ 2 or if dm(s 1 , s 2 ) = ⊤ ▲ . Let thus s 2 k2 -→ 2 t 2 , then there exist s 1 k1 -→ 1 t 1 with F (k 1 , k 2 , dm(t 1 , t 2
)) ⊑ ▲ dm(s 1 , s 2 ). Now by induction hypothesis, φ ′ @t 1 ⊑ ▲ dm(t 1 , t 2 ) ⊕ ▲ φ ′ @t 2 , and then, using the triangle inequality, F (k 1 , ℓ, φ ′ @t 1 ) ⊑ ▲ F (k 1 , k 2 , dm(t 1 , t 2 )) ⊕ ▲ F (k 2 , ℓ, φ ′ @t 2 ) ⊑ ▲ dm(s 1 , s 2 ) ⊕ ▲ F (k 2 , ℓ, φ ′ @t 2 ).

As s 2

k2

-→ 2 t 2 was arbitrary, this entails

inf{F (k 1 , ℓ, φ ′ @t 1 ) | s 1 k1 -→ 1 t 1 } ⊑ ▲ inf{F (k 2 , ℓ, φ ′ @t 2 ) | s 1 k2 -→ 2 t 2 } ⊕ ▲ dm(s 1 , s 2 ).
For the case φ = [ℓ]φ ′ the proof is similar: We have nothing to prove if dm(s 1 , s 2 ) = ⊤ ▲ or if there are no transitions s 1 k1 1 t 1 with F (k 1 , ℓ, φ ′ @t 1 ) = ⊤ ▲ , so assume there is such a transition. Then we also have s 2 k2 2 t 2 with F (k 1 , k 2 , dm(t 1 , t 2 )) ⊑ ▲ dm(s 1 , s 2 ), and

F (k 1 , ℓ, φ ′ @t 1 ) ⊑ ▲ F (k 1 , k 2 , dm(t 1 , t 2 )) ⊕ ▲ F (k 2 , ℓ, φ ′ @t 2 ) ⊑ ▲ dm(s 1 , s 2 ) ⊕ ▲ F (k 2 , ℓ, φ ′ @t 2 ).
Theorem 7 For all disjunction-free φ ∈ L and all SMTS S, φ@S = sup I∈ S φ@I.

Proof Theorem 6 entails φ@I ⊑ ▲ φ@S ⊕ ▲ dm(I, S) = φ@S for all I ∈ S , hence also sup I∈ S φ@I ⊑ ▲ φ@S. To show that φ@S ⊑ ▲ sup I∈ S φ@I we use structural induction on φ. If φ = tt, both sides are ⊥ ▲ , and if φ = ff , both sides are ⊤ ▲ , so the induction base is clear.

The case φ = φ 1 ∧ φ 2 is also clear: By hypothesis, φ 1 @S ⊑ ▲ sup I∈ S φ 1 @I and similarly for φ 2 , hence φ@S = max(φ 1 @S, φ 2 @S) ⊑ ▲ max( sup

I∈ S φ 1 @I, sup I∈ S φ 2 @I) = sup I∈ S
max(φ 1 @I, φ 2 @I).

For the case φ = ℓ φ ′ , we are done if φ@S = ⊥ ▲ . Otherwise, let α ⊏ ▲ φ@S; we want to expose I ∈ S for which α ⊏ ▲ φ@I. Start by letting I = {i 0 } and -→ I = ∅. Now for each transition s 0 k -→ S t, we have α ⊏ ▲ F (k, ℓ, φ ′ @t), so (assuming for the moment that φ ′ @t = ⊥ ▲ ) there is α ′ k ⊏ ▲ φ ′ @t for which F (k, ℓ, α ′ k ) ⊐ ▲ α. By induction hypothesis, there is J ∈ t, S for which α ′ k ⊏ ▲ φ ′ @J; let n ∈ k such that F (n, ℓ, φ ′ @J) = F (k, ℓ, φ ′ @J), and add J together with a transition i 0 n -→ I j 0 to I.

In case φ ′ @t = ⊥ ▲ , we just take an arbitrary J ∈ t, S .

For the so-constructed implementation I we have

φ@I = inf{F (m, ℓ, φ ′ @j | i 0 m -→ I j} = inf{F (k, ℓ, φ ′ @J) | s 0 k -→ S t, J ∈ t, S , φ ′ @t = ⊥ ▲ or α ′ k ⊏ ▲ φ ′ @J} ⊐ ▲ inf({F (k, ℓ, α ′ k ) | s 0 k -→ S t} ∪ {F (k, ℓ, φ ′ @t)}) ⊒ ▲ α, (4)
the strict inequality in (4) because S is compactly branching.

For the case φ = [ℓ]φ ′ , let again α ⊏ ▲ φ@S, and let I ∈ S be any implementation (there exists one because of local consistency of S). If F (k, ℓ, φ ′ @t) = ⊤ ▲ for all s 0 k S t, then φ@S = sup ∅ = ⊥ ▲ and we are done. Otherwise let s 0 k S t be such that φ@S = F (k, ℓ, φ ′ @t), which exists because S is compactly branching.

Then α ⊏ ▲ F (k, ℓ, φ ′ @t), so (assuming that φ ′ @t = ⊥ ▲ ) we have α ′ k ⊏ ▲ φ ′ @t with

F (k, ℓ, α ′ k ) ⊐ ▲ α.
Let J ∈ t, S such that α ′ k ⊏ ▲ φ ′ @J, let n ∈ k such that F (n, ℓ, φ ′ @J) = F (k, ℓ, φ ′ @J), and add J together with a transition i 0 n -→ I j 0 to I. Then

φ@I = sup{F (m, ℓ, φ ′ @n) | i 0 m -→ I j} ⊒ ▲ F (n, ℓ, φ ′ @J) = F (k, ℓ, φ ′ @J) ⊒ ▲ F (k, ℓ, α ′ k ) ⊐ ▲ α.
In case φ ′ @t = ⊥ ▲ instead, we again take an arbitrary J ∈ t, S , and then φ@I ⊒ ▲ F (k, ℓ, φ ′ @t) ⊐ ▲ α. ⊓ ⊔

Robust Semantics of Modal Event-Clock Specifications

As an application of the framework laid out in this paper, we consider the modal event-clock specifications (MECS) of [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF][START_REF] Bertrand | Modal eventclock specifications for timed component-based design[END_REF][START_REF] Bertrand | Refinement and consistency of timed modal specifications[END_REF] and give them a robust semantics as SMTS. We choose MECS instead of a more expressive real-time formalism such as e.g. timed automata [START_REF] Alur | A theory of timed automata[END_REF] mainly for ease of exposition; it is certainly possible to extend the work presented here also to these formalisms. Motivated by the real-time framework, we use the maximum-lead distance from Example 5 to measure quantitative satisfaction and refinement and intersection of timing constraints for label composition. The so-defined quantitative specification theory has a bounded parallel composition and a well-behaved quotient. Conjunction is relaxed bounded. We will see later that "relaxed" or "robust" semantics of MECS as introduced e.g. in [START_REF] Bouyer | Timed automata can always be made implementable[END_REF][START_REF] Gupta | Robust timed automata[END_REF][START_REF] Swaminathan | A symbolic decision procedure for robust safety of timed systems[END_REF][START_REF] Swaminathan | The surprising robustness of (closed) timed automata against clock-drift[END_REF], though very different from each other, all are restrictions of our semantics.

Modal event-clock specifications

We assume a fixed finite alphabet Σ and let δ / ∈ Σ denote a special symbol which signifies passage of time. Let, as in Example 6, Φ(Σ) denote the set of closed clock constraints over Σ, given by

Φ(Σ) ∋ φ ::= a ≤ k | a ≥ k | φ 1 ∧ φ 2 (a ∈ Σ, k ∈ ◆, φ 1 , φ 2 ∈ Φ(Σ)) .
(u + d)(a) = u(a) + d, u[b](a) = [c]0 if a = b, u(a) otherwise.
The initial valuation is u 0 given by u 0 (a) = 0 for all a ∈ Σ.

We denote by ❏

= {[x, y] | x ∈ | ≥0 , y ∈ | ≥0 ∪ {∞}, x ≤ y} the set of closed
extended non-negative real intervals, and define addition of intervals, as before, by

[l, r] + [l ′ , r ′ ] = [l + l ′ , r + r ′ ].
An interval clock valuation is a mapping v : Σ → ❏ associating with each symbol a a non-negative interval

(v + d)(a) = v(a) + [d, d], v[b](a) = [c][0, 0] if a = b, u (a)
otherwise.

The initial valuation is v 0 given by v 0 (a) = [0, 0] for all a ∈ Σ.

Definition 10

A modal event-clock specification (MECS) is a tuple A = (Q, q 0 , A , -→ A ) consisting of a finite set Q of locations, with initial location q 0 ∈ Q, and may and must edges A , -→ A ⊆ Q × Σ × Φ(Σ) × Q which satisfy that for all (q, a, g, q ′ ) ∈ -→ A there exists (q, a, g ′ , q ′ ) ∈ A with g ⊆ g ′ .

As before we write q a,g A q ′ instead of (q, a, g, q ′ ) ∈ A , similarly for -→ A . Figure 3 shows some examples of MECS.

To facilitate robust analysis of MECS, we give their semantics not as usual timed transition systems [START_REF] Alur | A theory of timed automata[END_REF] (or as modal region automata as in [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF]), but as interval timed modal transition systems (ITMTS). These are SMTS over 3 An MECS model S of a resource specification, cf. [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF], and two refinement candidates S ′ , S ′′ . As customary, we omit may transitions which have an underlying must transition with the same label. Note that S ′ ≤m S and S ′′ ≤m S, but dm(S ′′ , S) = 1.

Spec = (Σ × {[0, 0]}) ∪ ({δ} × ❏) ⊆ (Σ ∪ {δ}) × ❏, s 0 s 1 s 2 S get grant get ≤ 2 extra grant get ≤ 5 s ′ 0 s ′ 1 S ′ get grant get ≤ 1 s ′′ 0 s ′′ 1 s ′′ 2 s ′′
with (a, [l, r]) ⊑ Spec (a ′ , [l ′ , r ′ ]) if and only if a = a ′ , l ≥ l ′ , and r ≤ r ′ (hence [l, r] ⊆ [l ′ , r ′ ]

Definition 11 The semantics of a MECS

A = (Q, q 0 , A , -→ A ) is the ITMTS A = (S, s 0 , S , -→ S )
given as follows:

S = {(q, v) | q ∈ Q, v : Σ → ❏} s 0 = (q 0 , v 0 ) -→ S = {(q, v) a,0 -→ S (q ′ , v ′ ) | q a,g -→ A q ′ , v |= g, v ′ = v[a]} ∪ {(q, v) δ,[l,r] -→ S (q, v ′ ) | v ′ = v + [l, r]} S = {(q, v) a,0 S (q ′ , v ′ ) | q a,g A q ′ , v |= g, v ′ = v[a]} ∪ {(q, v) δ,[l,r] S (q, v ′ ) | v ′ = v + [l, r]}
As we are using closed clock constraints for MECS, A as defined above is compactly branching. Note that the "real", precise semantics of A as a timed transition system [START_REF] Alur | A theory of timed automata[END_REF] is an implementation of A .

Refinement of MECS is defined semantically: A ≤m B if A ≤m B . Note that the refinement of [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF] is different (indeed it is not quantitative in our sense). By definition of modal refinement, a specification S ≤m A is a more precise, or less relaxed, specification of the semantics of A: any delay intervals on transitions s

δ,[l,r] S s ′ are contained in intervals t δ,[l ′ ,r ′ ]
A t ′ (and similarly for must transitions).

Refinement distance

We are interested in timing differences of (refinements of) MECS, i.e. in expressing how much two ITMTS can differ in the timings of their behaviors. Given two finite traces σ = (a 0 , x 0 ), . . . , (an, xn) and σ ′ = (a 0 , x ′ 0 ), . . . , (an, x ′ n ) (note that the discrete labels in Σ ∪ {δ} are the same), their timing difference is Applying the definition of F , we see that this is equivalent to

|(x 0 + x 1 + • • • + xn) -(x ′ 0 + x ′ 1 + • • • + x ′ n )|,
sup p∈ k k ′ inf q∈ ℓ ℓ ′ max(|d + p -q|, max(α(d + p -q), α ′ (d + p -q))) ≤ max      sup m∈ k inf n∈ ℓ max(|d + m -n|, α(d + m -n)) sup m ′ ∈ k ′ inf n ′ ∈ ℓ ′ max(|d + m ′ -n ′ |, α ′ (d + m ′ -n ′ ));
note that we are abusing notation by identifying e.g. p = (a, x) with x. This inequality in turn is equivalent to

max              sup p∈ k k ′ inf q∈ ℓ ℓ ′ |d + p -q| sup p∈ k k ′ inf q∈ ℓ ℓ ′ α(d + p -q) sup p∈ k k ′ inf q∈ ℓ ℓ ′ α ′ (d + p -q) ≤ max                      sup m∈ k inf n∈ ℓ |d + m -n| sup m∈ k inf n∈ ℓ α(d + m -n) sup m ′ ∈ k ′ inf n ′ ∈ ℓ ′ |d + m ′ -n ′ | sup m ′ ∈ k ′ inf n ′ ∈ ℓ ′ α ′ (d + m ′ -n ′ ).
In this expression, the first line on the left-hand side is bounded by the right-hand side's first line, the second line on the left by the second line on the right, and the

a, [1, 1] S a, [0, 2] T a, [3, 3] S ′ a, [2, 4] T ′ S S ′ a, [2, 2]
T T ′ Fig. 5 Discrete failure in independent implementability. We have dm(S, T ) = dm(S ′ , T ′ ) = ⊥ ▲ , but dm(S S ′ , T T ′ ) = ⊤ ▲ . left-hand side's last line by the last line of the right-hand side, so that altogether, it holds. ⊓ ⊔

The notion of structural composition of ITMTS we obtain is consistent with the one of synchronized product of [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF] (denoted ⊗ in that paper). Figure 4 depicts some examples of structural compositions. Theorem 8 Let A, B, A ′ and B ′ be MECS. With the notion of synchronized product of MECS from [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF], A B ≡m A B . Additionally, if dm(A A ′ , B B ′ ) = ∞, then dm(A A ′ , B B ′ ) ≤ max( dm(A, B), dm(A ′ , B ′ )).

Proof A B ≡m A B is clear from the definitions, and the second part follows directly from Theorem 2. ⊓ ⊔

We finish the section by a remark on the condition dm(A A ′ , B B ′ ) = ∞ in Theorem 8. As the proof of Theorem 2 shows, this is necessary to guard for what one may call discrete failures, where synchronized transitions may fail to exist due to incompatible timing constraints. The example in Figure 5 shows such a failure. When there are no such discrete failures, structural composition is bounded.

Quotient

For quotient of ITMTS we define, for labels (a, [l, r]), (a ′ , [l ′ , r ′ ]) ∈ Spec,

(a ′ , [l ′ , r ′ ]) (a, [l, r]) =                         
undefined if a = a ′ , (a, [l ′ , ∞]) if a = a ′ and l < l ′ ≤ r ≤ r ′ , (a, [l ′ , r ′ ]) if a = a ′ and l < l ′ ≤ r ′ < r , undefined if a = a ′ and l ≤ r < l ′ ≤ r ′ , (a, [0, ∞]) if a = a ′ and l ′ ≤ l ≤ r ≤ r ′ , (a, [0, r ′ ]) if a = a ′ and l ′ ≤ l ≤ r < r ′ , undefined if a = a ′ and l ′ ≤ r ′ < l ≤ r . The intuition is that to obtain the maximal solution [p, q] to an equation [l, r] [p, q] ⊑ Spec [l ′ , r ′ ], whether p and q must restrain the interval in the intersection, or can be 0 and ∞, respectively, depends on the position of [l, r] relative to [l ′ , r ′ ], cf. Figure 6.

l l ′ r r ′ l l ′ r ′ r l r l ′ r ′ l ′ l r r ′ l ′ l r ′ r l ′ r ′ l r

Lemma 6

The operator is quantitatively well-behaved.

Proof We need to show that for all k, ℓ, m ∈ Spec, α ∈ ▲ and with defined on intervals as above. Our quotient of MECS is then defined as in [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF], but with their guard operation replaced by our (hence our quotient is different from theirs, which is to be expected as the notions of refinement are different).

Theorem 9 Let A, B, X be MECS for which B A exists, then B A ≡ B A . If A is strongly deterministic, then dm(X, B A) ≤ dm(A X, B), and X ≤m B A if and only if A X ≤m B.

Proof B A ≡ B

A is clear from the definitions. For the second part, X ≤m B A if and only if A X ≤m B by Theorem 3, and by the same theorem, dm(X, B A) ⊑ dm(A X, B), so as g : ▲ → | ≥0 ∪ {∞} is a homomorphism, the claim follows. ⊓ ⊔

Conjunction

The conjunction operator on labels of ITMTS is defined using intersection of intervals like for structural composition, hence we let k ℓ = k ℓ for k, ℓ ∈ Spec. The intuition is that transition intervals give constraints on timings; hence a transition in the conjunction has to satisfy both interval constraints. Like in Examples 1 to 3, it can be shown that is not bounded.

Lemma 7

The operator is relaxed conjunctively bounded by C(α, α ′ ) = α + α ′ . Proof We use Lemma 4 and the constructions in its proof. We need to show that for all α, α ′ ∈ ▲ and all d ∈ |, + max( inf l ′ ≤y≤r ′ |d + z -y|, inf l ′ ≤y≤r ′ α ′ (d + zy)), the last inequality by distributivity of + over max. As this holds for all z, we have proven [START_REF] Bauer | Weighted modal transition systems[END_REF]. ⊓ ⊔

Our notion of conjunction is consistent with the one for MECS in [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF], and to make use of relaxed boundedness, we need to lift the notion of quantitative widening from the semantic ITMTS level to MECS. This is done by defining, for a clock constraint φ : Σ → ❏ and n ∈ ◆, the n-extended constraint φ +n by φ +n (a) = φ(a)+[-n, n] (this is similar to a construction in [START_REF] Bouyer | Timed automata can always be made implementable[END_REF]), and then saying that a MECS B is an n-widening of another MECS A if there is a relation R ⊆ Q A × Q B for which (q A 0 , q B 0 ) ∈ R, and for all (q A , q B ) ∈ R, q A a,g A q ′ A if and only if q B a,g+n q ′ B with (q B , q ′ B ) ∈ R and similarly for must transitions.

Conclusion

This paper constitutes the first general and complete quantitative theory for modal specifications. We have shown not only how to introduce such a general quantitative framework, but also the general conditions one needs to impose on the interplay between the system distance and the operators such as composition and quotient for the quantitative theory to work properly. Using [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF][START_REF] Bauer | Weighted modal transition systems[END_REF] and our final example of modal event-clock specifications, we have seen two different instantiations of the general framework, using different distances for measuring variations of systems and specifications and different operators for structural composition and quotient. Other applications of our framework, e.g. to hybrid systems, in programming languages or quantitative logics, will require other distances and other operators, but as shown in [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF], they all stay within the unifying framework introduced in this paper.

Fig. 2

 2 Fig.2Four implementations of the simple email system in Figure1.

A

  (real) clock valuation is a mapping u : Σ → | ≥0 ; we say that u |= φ, for φ ∈ Φ(Σ), if u(a) satisfies φ for all a ∈ Σ, and we let φ = {u : Σ → | ≥0 | u |= φ}. For d ∈ | ≥0 and b ∈ Σ we define the delay and reset valuations u + d and u[b] by

  v(a) = [la, ra] ∈ ❏ of possible clock values. We say that v |= φ, for φ ∈ Φ(Σ), if there exists u : Σ → | ≥0 for which u(a) ∈ v(a) for all a ∈ Σ and u |= φ. For d ∈ ❏ and b ∈ Σ we define the valuations v + d and v[b] by

  Fig.[START_REF] Bauer | Moving from specifications to contracts in componentbased design[END_REF] An MECS model S of a resource specification, cf.[START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF], and two refinement candidates S ′ , S ′′ . As customary, we omit may transitions which have an underlying must transition with the same label. Note that S ′ ≤m S and S ′′ ≤m S, but dm(S ′′ , S) = 1.

  as in the examples), and thus with Imp = Σ ×{0}∪{δ}×| ≥0 . Hence an implementation is a usual timed transition system, with discrete transitions s a,0 -→ s ′ and delay transitions s δ,d -→ s ′ .

Fig. 4 A

 4 Fig.[START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] A MECS model T of a process accessing the resource S from Figure3, together with the structural compositions S T , S ′ T and S ′′ T . Note that dm(S ′′ T, S T ) = 1.

Fig. 6

 6 Fig. 6 Quotient [l ′ , r ′ ] [l, r] of intervals, six cases. Top bar: [l, r]; middle bar: [l ′ , r ′ ]; bottom bar: quotient. Note that for the two cases on the right, quotient is undefined.

  d ∈ |, F (m, ℓ ⊖ k, α)(d) ≥ F (k m, ℓ, α)(d).The proof is somewhat complicated by the large number of cases due to different placement of the intervals in k, ℓ and m, so, denoting the left and right interval bounds in k by k -and k + (similarly for ℓ and m), we only show the case whereℓ -≤ k -≤ ℓ + ≤ m -≤ k + ≤ m + . In this case, the assertion that F (m, ℓ ⊖ k, α)(d) ≥ F (k m, ℓ, α)(d) is equivalent to sup m -≤x≤m + inf y≤ℓ + max(|d + x -y|, α(d + xy)) ≥ sup m -≤x≤k + inf ℓ -≤y≤ℓ + max(|d + x -y|, α(d + xy)), which is clear as m -≤ x ≤ k + implies m -≤ x ≤ m + . ⊓ ⊔We can lift our quotient from the semantic ITMTS level to MECS as follows: A clock constraint in Φ(Σ) is equivalent to a mapping Σ → ❏, where ❏ = {[x, y] | x ∈ ◆, y ∈ ◆ ∪ {∞}, x ≤ y} ⊆ ❏ denotes the set of closed extended non-negative integer intervals, and then we can define φ ′ φ by (φ ′ φ)(a) = φ ′ (a) φ(a)

supl

  ′′ ≤z≤r ′′

5 )

 5 inf r≤w≤l ′ max(|d + z -w|, α(d + zw) + α ′ (d + zw)) ≤ sup l ′′ ≤z≤r ′′ inf l≤x≤r max(|d + z -x|, α(d + zx)) + sup l ′′ ≤z≤r ′′ inf l ′ ≤y≤r ′ max(|d + z -y|, α ′ (d + zy)) (Now for all z ∈ [l ′′ , r ′′ ], we have inf r≤w≤l ′ |d + z -w| ≤ inf l≤x≤r |d + z -x| + inf l ′ ≤y≤r ′ |d + z -y| and inf r≤w≤l ′ (α(d + zw) + α ′ (d + zw)) ≤ inf l≤x≤r α(d + zx) + inf l ′ ≤y≤r ′ α ′ (d + zy);both can be shown by simply considering all cases of the placement of the infima. But then also max( infr≤w≤l ′ |d + z -w|, inf r≤w≤l ′ (α(d + zw) + α ′ (d + zw))) z -x| + inf l ′ ≤y≤r ′ |d + z -y| inf l≤x≤r α(d + zx) + inf l ′ ≤y≤r ′ α ′ (d + zy)) ≤ max( infl≤x≤r |d + z -x|, inf l≤x≤r α(d + zx))

Theorem 10

 10 Let A, B be MECS. With ∧ the notion of greatest lower bound from[START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF], A ∧ B ≡ A ∧ B . If A or B is strongly deterministic and there is a MECS C for which dm(C, A) = ∞ and dm(C, B) = ∞, then there are an n-widening A ′ of A and an m-widening B ′ of B for which A ′ ∧ B ′ is defined, and such that dm(C′ , A ′ ∧ B ′ ) ≤ dm(C ′ , A) + dm(C ′ , B) for all MECS C ′ .Proof A∧B ≡ A ∧ B by definition, and the second claim follows from Theorem 5and the homomorphism property of g : ▲ → | ≥0 ∪ {∞}. ⊓ ⊔

  and what interests us is the maximal timing difference at any point of

	get	get ≤ 2 extra			get
	t 0		t 1	s ′ 0 , t 0		s ′ 1 , t 0
	get ≤ 3 grant	get ≤ 5 grant			get ≤ 1 grant
		T			S ′ T
				s ′′ 4 , t 0	get	s ′′ 3 , t 0
		get		get ≤ 1 grant		get ≤ 3 grant
	s 0 , t 0		s 1 , t 0	s ′′ 0 , t 0	get	s ′′ 1 , t 0
	get ≤ 5 grant	get ≤ 2 grant	get ≤ 2 extra	get ≤ 4 grant		get ≤ 2 extra
		s 2 , t 1			s ′′ 2 , t 1
		S T			S ′′ T

Acknowledgements

The authors wish to thank Sebastian S. Bauer and Claus Thrane for numerous discussions on the subject of this work, and a number of anonymous referees for useful comments and improvements.

the runs. Hence we want the distance between σ and σ ′ to be max m=0,...,n | m i=0 x im i=0 x ′ i |, and with the max m=0,...,n replaced by sup m∈◆ for infinite traces. This is precisely the maximum-lead distance of Example 5.

Note that the accumulating distance of [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] measures something entirely different: for the finite traces above, it is

, hence measuring the sum of the differences in the individual timings of transitions rather than the overall timing difference. Thus the work laid out in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] is not applicable to our setting, showing the strength of our more general approach.

Like in Example 5, we hence let ▲ = (| ≥0 ∪ {∞}) | , the set of mappings from leads to distances, define F :

and extend F to specifications by F (k, ℓ, α) = sup m∈ k inf n∈ ℓ F (m, n, α). We also define g : ▲ → | ≥0 ∪ {∞} by g(α) = α(0); the maximum-lead distance assuming the lead is zero.

We also instantiate our definitions of modal and thorough refinement distance for ITMTS; for MECS A, B we let dm(A, B) = dm( A , B ),

We already saw that in our special case, the notion of determinism from Definition 2 specializes to the condition, for all s ∈ S, that s (a,[l1,r1])

S s 1 and s

and s 1 = s 2 . For an MECS A, A is hence deterministic if and only if for all locations q, q a,g1

q 1 and q a,g2 q 2 imply that g 1 = g 2 and q 1 = q 2 . This is a stronger notion of determinism than in [START_REF] Bertrand | A compositional approach on modal specifications for timed systems[END_REF]; we will call it strong determinism for differentiation.

Structural composition

For structural composition of ITMTS, the natural choice is to use CSP-style synchronization on discrete labels and intersection of intervals. As intervals signify timing constraints, composed intervals will then impose the conjunction of the timing constraints. Note that this is different from the synchronization used in Examples 1 to 3. Given (a, [l, r]), (a ′ , [l ′ , r ′ ]) ∈ Spec we hence define

Lemma 5

The operator is bounded above by P (α, α ′ ) = max(α, α ′ ).

Proof Let k, k ′ , ℓ, ℓ ′ ∈ Spec, α, α ′ ∈ ▲ and d ∈ |, and assume both k k ′ and ℓ ℓ ′ defined. Hence we can assume that the discrete parts of k, k ′ , ℓ and ℓ ′ are all the same and ignore them from now on. We need to show that F (k k ′ , ℓ ℓ ′ , max(α, α ′ ))(d) ≤ max(F (k, ℓ, α)(d), F (k ′ , ℓ ′ , α ′ )(d)) .