Sebastian S Bauer

Uli Fahrenberg

Axel Legay

Claus Thrane

General Quantitative Specification Theories with Modalities

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. It is shown that this general approach permits to recast many existing problems which arise in 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 [13-15, 18, 21], 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] 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] 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].

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. For quantifying differences, distances between systems are useful; this approach has been explored e.g. in [START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF][START_REF] Larsen | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF][START_REF] Van Breugel | A behavioural pseudometric for metric labelled transition systems[END_REF]. A first quantitative specification theory which is not fragile is introduced in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF], for one specific type of weighted modal transition systems and one specific distance. While this is useful for some applications, it is too specific to cover the whole spectrum of quantitative specification theories.

What is needed is 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; these are worked out in detail.

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. Note that all proofs of this paper had to be omitted due to space constraints.

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.

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 ′ ⊑ k} and assume that Spec is well-formed in the sense that k = ∅ for all k ∈ Spec.

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]. 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)|.

Let d : Imp × Imp → ▲ be a hemimetric on implementation labels; recall that this means that d(m, m) = ⊥ ▲ for all m ∈ Imp and d(m 1 , m 2 ) ⊕ ▲ d(m 2 , m 3 ) ⊒ ▲ d(m 1 , m 3 ) (the triangle inequality) for all m 1 , m 2 , m 3 ∈ Imp. 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 the similarity of this to the construction of Hausdorff metric; cf. [START_REF] Munkres | Topology[END_REF][START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF] for background material on hemimetrics and the Hausdorff construction.

We will assume given an abstract trace distance d T : Spec ∞ × Spec ∞ → ▲ which has a recursive expression using a distance iterator function F : Imp×Imp× ▲ → ▲. This will allow us to recover many of the system distances found in the literature, while preserving key results. We will need F to be continuous in the first two coordinates and monotone in the third; hence F (•, n, α) and F (m, •, α) are continuous functions Imp → ▲ for all α ∈ ▲,and F (m, n, •) : ▲ → ▲ is monotone for all m, n ∈ Imp.

We also assume that F (m, n, ⊥ ▲ ) = d(m, n) for all m, n ∈ Imp, and 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. We also extend the triangle inequality for d to F by imposing that for all k, ℓ, m ∈ Spec and α, β, γ ∈ ▲ with α ⊕ ▲ β ⊒ ▲ γ,

F (k, ℓ, α) ⊕ ▲ F (ℓ, m, β) ⊒ ▲ F (k, m, γ). (1)
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 σ = τ = ε. (2)
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 g • d T . The triangle inequality for F implies the usual triangle inequality for g Example 1. [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] defines an accumulating distance for integer-weighted modal transition systems. In this paper, Spec = Σ × ■, where Σ is a finite set of discrete labels and ■ = {[l, r] | l ∈ ) ∪ {-∞}, r ∈ ) ∪ {∞}, l ≤ r} is the set of extendedinteger intervals, and 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, thus Imp = Σ × ). The implementation label distance is given by d((a, x), (a ′ , y)) = |x -y| if a = a ′ and ∞ 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] De Alfaro | Linear and branching system metrics[END_REF][START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF][START_REF] Larsen | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF][START_REF] Van Breugel | A behavioural pseudometric for metric labelled transition systems[END_REF][START_REF] Zwick | The complexity of mean payoff games[END_REF]. [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] develops a complete specification theory around this specific distance; we will continue this example below to show how it fits in our present context.

• d T : g(d T (σ, τ )) + g(d T (τ, χ)) ≤ g(d T (σ, χ)) for all σ, τ, χ ∈ Spec ∞ , hence g • d T is a hemimetric on Spec ∞ .
Example 2. With the same instantiations of Imp and Spec as above, we can introduce a distance which, instead of accumulating individual label differences, measures the long-run difference between accumulated labels. This maximumlead 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].

Let ▲ = (| ≥0 ∪{∞}) | , define F : Imp×Imp×▲ → ▲ by F ((a, x), (a ′ , y), α) = ⊤ ▲ if a = a ′ and F ((a, x), (a, y), α)(δ) = max(|δ + x -y|, α(δ + x -y)), and extend F to specifications by F (k, ℓ, α) = sup m∈ k inf n∈ ℓ F (m, n, α). Define g : ▲ → | ≥0 ∪ {∞} by g(α) = α(0); the maximum-lead distance assuming the lead is zero. Using our definition of d T from (2), 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 ), . . . ), [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF].

g(d T (σ, τ )) = sup m | m i=0 x i - m i=0 y i | is precisely the maximum-lead distance of
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 ℓ. This last condition is one of consistency: everything which is required, is also allowed. 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.

We will assume all SMTS to be compactly branching [START_REF] Van Breugel | A theory of metric labelled transition systems[END_REF], that is, for any SMTS S and any s ∈ S, the sets {k ∈ Spec | s k s ′ } and {k ∈ Spec | s k -→ s ′ } are to be compact under the label metric d. This is a common assumption in quantitative formalisms which generalizes the standard finitely-branching assumption; together with continuity of F it will allow us to resolve terms of the form sup

s k s ′ inf t ℓ t ′ F (k, ℓ, α). The SMTS (S, s 0 , S , -→ S ) is deterministic if it holds for all s ∈ S, s k1 S s 1 , s k2 S 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 .
Example 1 (contd). For the label distance of [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF], and also the one of Example 2, 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]. The general intuition for determinacy is that there cannot be two distinct transitions out of a state with labels which have a common quantitative refinement.

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 .

Refinement Distances

We define two distances between SMTS, one at the syntactic and one at the semantic level. The modal refinement distance d m : S × T → ▲ between the states of SMTS S, T is defined to be the least fixed point to the equations

d m (s, t) = max      sup s k S s ′ inf t ℓ T t ′ F (k, ℓ, d m (s ′ , t ′ )), sup t ℓ -→ T t ′ inf s k -→ S s ′ F (k, ℓ, d m (s ′ , t ′ )).
We let d m (S, T ) = d m (s 0 , t 0 ), and we write S ≤ α m T if d m (S, T ) ⊑ ▲ α. This definition is an extension of the one of simulation distance in [START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF], and the proof of existence of the least fixed point is similar to the one in [START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF]. Note also that d m extends the refinement relation ≤ m in the sense that s ≤ m t implies d m (s, t) = 0. If we define the linear distance from s to t 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, then d T (s, t) ⊑ ▲ d m (s, t) for all s, t ∈ S, cf. [START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF].

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

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

S ≤ α t T if d t (S, T ) ⊑ ▲ α. Again, S ≤ t T implies d t (S, T ) = 0.
The next proposition follows directly from the triangle inequality (1).

Proposition 1. For all SMTS S, T , U , d m (S, T ) ⊕ ▲ d m (T, U ) ⊒ ▲ d m (S, U ) and d t (S, T ) ⊕ ▲ d t (T, U ) ⊒ ▲ d t (S, U ).
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] Larsen | Modal specifications[END_REF]; note [START_REF] Larsen | Modal specifications[END_REF] that deterministic specifications generally suffice for applications.

Theorem 1. For all SMTS S, T , d t (S, T ) ⊑ ▲ d m (S, T ). If T is deterministic, then d t (S, T ) = d m (S, T ).
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 is an α-widening of S if there is a relation R ⊆ S ×T for which (s 0 , t 0 ) ∈ R and such that for all (s, t) ∈ R, s k S s ′ if and only if t ℓ T t ′ , and s k -→ S s ′ if and only if t ℓ -→ T t ′ , for k ⊑ Spec ℓ, d(ℓ, k) ⊑ ▲ α, and (s ′ , t ′ ) ∈ R; -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.

Example 1 (contd).

In [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] it is shown that 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.

Example 2 (contd). For the maximum-lead distance, 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 a 1-widening of S, but g • d m (T, S) = ∞. Proposition 2. 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 the proof one only needs the fact that d m (I, S) ⊑ d m (I, T ) ⊕ d m (T, S) ⊑ ▲ α for all I ∈ T . Proposition 3. Let T be an α-relaxation of S and T ′ an α ′ -relaxation of S ′ , and

let d m (S, S ′ ) = β. Then β ⊑ ▲ d m (S, T ′ ) ⊕ ▲ α ′ , d m (S, T ′ ) ⊑ β, β ⊑ ▲ d m (T, S ′ ), and d m (T, 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 and with interleaving for non-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. We first define a partial label synchronization operator : Spec × Spec ֒→ Spec which satisfies the following conditions:

-For all k, ℓ, k ′ , ℓ ′ ∈ Spec, if d(k, ℓ) = ⊤ ▲ and d(k ′ , ℓ ′ ) = ⊤ ▲ , then k k ′ is defined if and only if ℓ ℓ ′ is defined; -for all ℓ, ℓ ′ ∈ Spec, (∃k ∈ Spec : d(k, ℓ) = ⊤ ▲ , d(k, ℓ ′ ) = ⊤ ▲ ) ⇐⇒ (∃m ∈ Spec : ℓ m, ℓ ′ m are defined).
This operator permits to synchronize labels at transitions which are executed in parallel; the first property ensures that refinements of synchronable labels can synchronize and vice versa, and the second relates synchronizability to distances in such a way that two labels have a common quantitative refinement if and only if they have a common synchronization.

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.

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 independent implementability: if S is close to T and S ′ close to T ′ , then we can bound the distance between the structural compositions.

Theorem 2. For SMTS S, T , S ′ , T ′ , d m (S S ′ , T T ′ ) ⊑ ▲ P (d m (S, T ), d m (S ′ , T ′ )).
Example 1 (contd). In [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF], structural composition of labels is defined by

(a, [l, r]) (a ′ , [l ′ , r ′ ]) = (a, [l + l ′ , r + r ′ ]) if a = a ′ , undefined otherwise.
This composition is bounded above by

P (α, α ′ ) = α + α ′ , hence Theorem 2 specializes to [2, Thm. 5]: d m (S S ′ , T T ′ ) ≤ d m (S, T ) + d m (S ′ , T ′ ).
Example 2 (contd). For the max-lead distance, and with an application to realtime systems in mind, structural composition is more naturally defined using intersection of intervals rather than addition, that is,

(a, [l, r]) (a ′ , [l ′ , r ′ ]) =      (a, [max(l, l ′ ), min(r, r ′ )])
if a = a ′ and max(l, l ′ ) ≤ min(r, r ′ ), undefined otherwise.

(Note that, however, the definition of structural composition is independent of which distance one uses; one might as well combine addition of intervals, as in Example 1, with the max-lead distance.) This composition is bounded by

P (α, α ′ ) = max(α, α ′ ), thus d m (S S ′ , T T ′ ) ≤ max(d m (S, T ) + d m (S ′ , T ′ )).
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 inverse to , and the second relates it to distances just as we did for above. We extend the first condition to 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 α ∈ ▲. We say that is quantitatively exact if the inequality can be sharpened to

F (m, ℓ k, α) = F (k m, ℓ, α).
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 must-predecessor 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 ρ ). 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
The next theorem shows that under certain standard conditions, quotient is sound and maximal with respect to . Note that the property that X ≤ m T S iff S X ≤ m T implies uniqueness of quotient [START_REF] Fahrenberg | Make a difference! (Semantically)[END_REF]; hence 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. 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 d m (X, T S) ⊒ ▲ d m (S X, T ); -if is quantitatively exact and d m (X, T S) = ⊤ ▲ , then d m (X, T S) = d m (S X, T ).
Example 1 (contd). In [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF], quotient of labels is defined by

(a ′ , [l ′ , r ′ ]) (a, [l, r]) = (a, [l ′ -l, r ′ -r]) if a = a ′ and l ′ -l ≤ r ′ -r, undefined otherwise.
This operator is quantitatively exact, hence Theorem 3 specializes to [2, Thm. 6]:

if d m (X, T S) = ∞, then d m (X, T S) = d m (S X, T ).
Example 2 (contd). For structural composition using interval intersection, it can be shown that given by

(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, [-∞, ∞]) if a = a ′ and l ′ ≤ l ≤ r ≤ r ′ , (a, [-∞, r ′ ]) if a = a ′ and l ′ ≤ l ≤ r < r ′ , undefined if a = a ′ and l ′ ≤ r ′ < l ≤ r.
yields a quotient operator which is quantitatively well-behaved, but not exact.

Theorem 3 implies that d m (X, T S) ≥ d m (S X, T ) if if d m (X, T S) = ∞.

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 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.

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
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. Example 1 (contd). For the formalism of [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF], there is a conjunction operator given by intersection of intervals:

(a, [l, r]) (a ′ , [l ′ , r ′ ]) = (a, [max(l, l ′ ), min(r, r ′ )]) if a = a ′ , max(l, l ′ ) ≤ min(r, r ′ ), undefined otherwise.
This operator is conjunctively compositional, but not conjunctively bounded, whence [2, Thm. 4]: by uniqueness, there does not exist any bounded conjunction operator within the formalism of [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF].

To deal with the problem that, as in Example 1, 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 family C = {C β,γ : ▲×▲ → ▲ | β, γ ∈ ▲} if all C β,γ are monotone in both coordinates, have C β,γ (⊥ ▲ , ⊥ ▲ ) = ⊥ ▲ , C β,γ (α, ⊤ ▲ ) = C β,γ (⊤ ▲ , α) = ⊤ ▲ for all α ∈ ▲, and if it holds for all k, ℓ ∈ Spec for which there is m ∈ Spec with d(m, k) = ⊤ ▲ and d(m, ℓ) = ⊤ ▲ that there exist k ′ , ℓ ′ ∈ Spec with k ⊑ Spec k ′ , ℓ ⊑ Spec ℓ ′ , d(k ′ , k) = β = ⊤ ▲ , and d(ℓ ′ , ℓ) = γ = ⊤ ▲ , such that k ′ ℓ ′ is defined, and then for all m ∈ Spec with d(m, k) = ⊤ ▲ and d(m, ℓ) = ⊤ ▲ ,

F (m, k ′ ℓ ′ , C β,γ (α, α ′ )) ⊑ ▲ C β,γ (F (m, k, α), F (m, ℓ, α ′ ))
for all α, α ′ ∈ ▲. The following theorem shows that relaxed boundedness of entails a similar property for 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 d m (U, S), d m (U, T ) = ⊤ ▲ , then there exist β-and γ-widenings S ′ of S and T ′ of T for which S ′ ∧ T ′ is defined, and such that d m (U, S ′ ∧ T ′ ) ⊑ ▲ C β,γ (d m (U, S), d m (U, T )) for all SMTS U for which d m (U, S) = ⊤ ▲ and d m (U, T ) = ⊤ ▲ .

Example 1 (contd). For the accumulating distance, is relaxed conjunctively bounded by C β,γ (α, α ′ ) = max(α, α ′ )⊕ ▲ max(β, γ). Hence Theorem 5 entails that if S or T are deterministic and there is U for which d m (U, S), d m (U, T ) = ∞, then there exist a β-widening S ′ of S and a γ-widening T ′ of T for which the conjunction S ′ ∧T ′ is defined, and such that d m (U,

S ′ ∧T ′ ) ≤ max(d m (U, S), d m (U, T ))+ max(β, γ) for all SMTS U for which d m (U, S) = ⊤ ▲ and d m (U, T ) = ⊤ ▲ .
Example 2 (contd). Also for the max-lead distance, given by intersection of intervals is the unique conjunction operator. It is again relaxed conjunctively bounded by C β,γ (α, α ′ ) = max(α, α ′ )⊕ ▲ max(β, γ), hence the same specialization of Theorem 5 as above holds for the max-lead distance.

Conclusion

We believe that 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] and our running example of max-lead distances, 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. Application of our framework e.g. to realtime and 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.

Appendix: Proofs

Before we attempt the proofs of the theorems in the paper, we introduce a powerful proof technique which will be used throughout: 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 1. For all SMTS S, T , 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 . Proof (of Lemma 1). Assume first that S ≤ α m T , thus we know that d m (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) | d m (s, t) ⊑ ▲ α}
for every α ∈ ▲; note that R is closed in the sense above. Now let β ∈ ▲ and

(s, t) ∈ R β .
-Assume s k s ′ . By d m (s, t) ⊑ ▲ β and the definition of d m (s, t) it follows that inf t ℓ t ′ F (k, ℓ, d m (s ′ , t ′ )) ⊑ ▲ β. As T is compactly branching and F continuous, the set

{F (k, ℓ, d m (s ′ , t ′ )) | t ℓ t ′ } is compact, hence there exists a transition t ℓ t ′ such that F (k, ℓ, d m (s ′ , t ′ )) ⊑ ▲ β.
-Assume t ℓ -→ t ′ . By d m (s, t) ⊑ ▲ β and the definition of d m (s, t) it fol-

lows that inf s k -→s ′ F (k, ℓ, d m (s ′ , t ′ )) ⊑ ▲ β. Again {F (k, ℓ, d m (s ′ , t ′ )) | s k -→ s ′ } is a compact set, whence there exists a transition s k -→ s ′ such that F (k, ℓ, d m (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 d m , implying that d m (s, t) ⊑ ▲ h(s, t) for all s ∈ S, t ∈ T , thus especially d m (s 0 , t 0 ) ⊑ ▲ α, because (s 0 , t 0 ) ∈ R α implies h(s 0 , t 0 ) ⊑ ▲ α and d m (s 0 , t 0 ) ⊑ ▲ h(s 0 , t 0 ).

⊓ ⊔

Proof (of Theorem 1). If d m (S, T ) = ⊤ ▲ , we have nothing to prove. Otherwise, let R = {R α ⊆ S × T | α ∈ ▲} be a modal refinement family which witnesses d m (S, T ), and let I ∈ S . We will expose J ∈ T for which d m (I, J) ⊑ ▲ d m (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 d m (I, J) ⊑ ▲

d m (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, ℓ, β) ⊑ ▲ α.

⊓ ⊔

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 d m ((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 d m (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 d m ((i, I), (j, J)) ⊑ ▲ α. We must have j n -→ J j ′ with n ∈ ℓ , hence there are i m -→ I i ′ and β ′ ∈ ▲ with d m ((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, ℓ, β ′ ) ⊑ ▲ α}.

⊓ ⊔

Proof (of Proposition 3). An application of the triangle inequality for d m : Theorem 2). The proof of the first claim is in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]. For the second claim,

d m (S, S ′ ) ⊑ ▲ d m (S, T ′ ) ⊕ ▲ d m (T ′ , S ′ ) ⊑ ▲ d m (S, T ′ ) ⊕ ▲ α ′ d m (S, T ′ ) ⊑ ▲ d m (S, S ′ ) ⊕ ▲ d m (S ′ , T ′ ) = d m (S, S ′ ) d m (S, S ′ ) ⊑ ▲ d m (S, T ) ⊕ ▲ d m (T, S ′ ) = d m (T, S ′ ) d m (T, S ′ ) ⊑ ▲ d m (T, S) ⊕ ▲ d m (S, S ′ ) ⊑ α ⊕ ▲ d m (S, S ′ ) ⊓ ⊔ Proof (of
let R = {R α ⊆ S × T | α ∈ ▲}, R ′ = {R ′ α ⊆ S ′ × T ′ | α ∈ ▲}
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 d m (S S ′ , T T ′ ) ⊑ ▲ P (d m (S, T ), d m (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 ′ , ℓ ′ , ᾱ′ ) ⊑ ▲ α ′ .
As F (k, ℓ, ᾱ) = ⊤ ▲ and F (k ′ , ℓ ′ , α ′ ) = ⊤ ▲ , the composition ℓ ℓ ′ is defined, and 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. ⊓ ⊔
Proof (of Theorem 3). The proof that X ≤ m T S if and only if S X ≤ m T is in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]. For the other properties, assume first to be quantitatively well-behaved;

we show that d m (S X, T ) ⊑ ▲ d m (X, T S). If d m (X, T S) = ⊤ ▲ , there is nothing to prove, so assume d m (X, T S) = ⊤ ▲ and let R = {R α ⊆ X × (T × S ∪ {u})} be a witness for d m (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 d m (S X, T ) ⊑ ▲ d m (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 d m (X, T S) ⊑ ▲ d m (S X, T ), assume that d m (S X, T ) = ⊤ ▲ (otherwise there is nothing to prove), let R = {R α ⊆ S × X × T | α ∈ ▲} be a witness for d m (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 d m (X, T S) ⊑ ▲ d m (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 ′ . ⊓ ⊔
Proof (of Theorem 4). The proof of the two first claims is in [START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF]. For the third

claim, let R = {R α ⊆ U × S | α ∈ ▲} and R ′ = {R ′ α ⊆ U × T | α ∈ ▲} be relation families witnessing d m (U, S) and d m (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 d m (U, S ∧ T ) ⊑ ▲ C(d m (U, S), d m (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 boundedness 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 allows us to conclude that k ℓ ′ is defined, but then both k ℓ and k ℓ ′ are defined, hence by determinism of T , ℓ = ℓ ′ and t ′ = t ′′ .

⊓ ⊔ Proof (of Theorem 5). 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 β = ⊥ ▲ , γ = ⊥ ▲ . (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 d m (U, S) = ⊤ ▲ and d m (U, T ) = ⊤ ▲ . We must show that d m (U, S ′ ∧T ′ ) ⊑ ▲ C β,γ (d m (U, S), d m (U, 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. ⊓ ⊔

  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 one in Example 2 below, have no recursive characterization using ▲ = | ≥0 ∪ {∞}. Whether the theory works for more general intermediate lattices than L = (| ≥0 ∪ {∞}) M is an open question; we have had no occasion to use more general lattices in practice.

Theorem 4 .

 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, d m (U, S) = ⊤ ▲ , and d m (U, T ) = ⊤ ▲ , then S ∧ T is defined and d m (U, S ∧ T ) ⊑ ▲ C(d m (U, S), d m (U, T )).

  be witnesses for d m (S, T ) and d m (S ′ , T ′ ), respectively, and define

  Let U fulfill d m (U, S) = ⊤ ▲ and d m (U, T ) = ⊤ ▲ , let R = {R α ⊆ U × S | α ∈ ▲} and R ′ = {R ′ α ⊆ U × T | α ∈ ▲}be relation families witnessing d m (U, S) and d m (U, T ), respectively, define R ∧ η = {(u, (s, t)) | ∃α, α ′ ∈ ▲ :

  Let R = {R α ⊆ U × S | α ∈ ▲} and R ′ = {R ′ α ⊆ U × T | α ∈ ▲} be relation families witnessing d m (U, S) and d m (U, T ), respectively, define R ∧ ′ η = {(u, (s, t)) | ∃α, α ′ ∈ ▲ :


Uli Fahrenberg

Axel Legay

A Robust Specification Theory for Modal Event-Clock Automata

In a series of recent work, we have introduced a general framework for quantitative reasoning in specification theories. The contribution of this paper is to show how this framework can be applied to yield a robust specification theory for timed specifications.

Introduction

Specification theories allow to reason 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. Depending on the application for which they are used, such specification theories may come together 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 set 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, cf. [START_REF] Bauer | Moving from Specifications to Contracts in Component-Based Design[END_REF].

Prominent among existing specification theories, outside logics, is the one of modal transition systems [6, 14-16, 19, 22, 23] 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 for an implementation. So far, existing modal specification theories have relied on Boolean versions of both the refinement and the satisfaction relation. They are hence fragile in the sense that they are unable to quantify the impact of small variations of the behavior of the environment in which a component is working. In a series of recent work [START_REF] Bauer | Quantitative Refinement for Weighted Modal Transition Systems[END_REF][START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF][START_REF] Bauer | Extending Modal Transition Systems with Structured Labels[END_REF], and building on a general theory of quantitative analysis of systems [START_REF] Fahrenberg | A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic[END_REF][START_REF] Fahrenberg | The Quantitative Linear-Time-Branching-Time Spectrum[END_REF][START_REF] Fahrenberg | Distances for Weighted Transition Systems: Games and Properties[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], we have leveraged this problem by extending modal specifications from the Boolean to the quantitative world and introducing truly quantitative versions of the operators mentioned above.

The contribution of this paper is to show how our general quantitative framework from [START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF] can be used to define a notion of robustness for timed modal specifications, or model event-clock specifications (MECS) [START_REF] Bertrand | A Compositional Approach on Modal Specifications for Timed Systems[END_REF]. We first observe that the notion of refinement proposed in [START_REF] Bertrand | A Compositional Approach on Modal Specifications for Timed Systems[END_REF] is not adequate to reason on MECS in a robust manner. We then propose a new version of refinement that can capture quantitative phenomena in a realistic manner, and proceed to exhibit the properties of the above specification-theory operators with respect to this quantitative refinement. We show that structural composition and quotient have properties which are useful generalizations of their standard Boolean properties, hence they can be employed for robust reasoning on MECS without problem. Conjunction, on the other hand, is generally not robust (similarly to the problems exposed in [START_REF] Bauer | Quantitative Refinement for Weighted Modal Transition Systems[END_REF]), but together with the new operator of quantitative widening can be used in a robust manner.

Quantitative Specification Theories

General quantitative specification theories have been introduced in [START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF]. These consist of • a specification formalism: modal transition systems with labels drawn from a set Spec,

• a distance on traces of labels: d T : Spec × Spec → | ≥0 , and

• operations on specifications which allow high-level reasoning and which generally are continuous with respect to the natural distance on specifications induced by the trace distance.

Below we give a more detailed account of these things, in order to be able to apply them to modal event-clock specifications later.

Structured Modal Transition Systems

We assume that the set Spec of labels comes with a partial order ⊑ Spec modeling 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 ′ ⊑ k} denote the set of implementation refinements of a label k, and we assume that Spec is well-formed in the sense that k = / 0 for all k ∈ Spec: any specification label can be implemented.

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 ℓ. This last condition is one of consistency: everything which is required, is also allowed.

An SMTS (S, s 0 , S , -→ S ) is an implementation if -→ S = S ⊆ S × Imp × S, i.e. an ordinary labeled transition system with labels in Imp. Hence in an implementation, all optional behavior has been resolved, and all data has been refined to implementation labels.

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, and S ≡ m T if there is a two-sided refinement S ≤ m T and T ≤ m S.

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 .

Distances

The above setting is purely qualitative, i.e. Boolean: a refinement S ≤ m T either holds, or it does not; a transition system I either is an implementation of a specification S, or it is not. In order to turn this setting into a quantitative one, where we can reason about robustness of refinements and implementations, we need to introduce distances.

We have in [START_REF] Fahrenberg | The Quantitative Linear-Time-Branching-Time Spectrum[END_REF] developed a general framework which allows to reason about a variety of such system distances in a uniform way. To apply this to specifications, let Spec ∞ = Spec * ∪ Spec ω denote the set of finite and infinite traces over Spec, and let d T : Spec ∞ × Spec ∞ → | ≥0 ∪ {∞} be an extended hemimetric.

Recall that this means that d T (σ , σ ) = 0 for all σ ∈ Spec ∞ , and that d T (σ 1 , σ 2 )+d T (σ 2 , σ 3 ) ≥ d T (σ 1 , σ 3 ) for all σ 1 , σ 2 , σ 3 ∈ Spec ∞ . Note that as Spec ⊆ Spec ∞ , d T induces a hemimetric on Spec.

Let M be an arbitrary set and ▲ = (| ≥0 ∪ {∞}) M the set of functions from M to the extended nonnegative 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)|.

Let F : Spec × Spec × ▲ → ▲ be a function with the following properties:

• F is continuous in the first two coordinates: F(•, k, α) and F(k, •, α) are continuous functions

Imp → ▲ for all k ∈ Spec, α ∈ ▲. • F is monotone in the third coordinate: F(k, ℓ, •) is a monotone function ▲ → ▲ for all k, ℓ ∈ Spec. • F(•, •, ⊥ ▲ ) extends d T : for all k, ℓ ∈ Spec, F(k, ℓ, ⊥ ▲ ) = d T (k, ℓ).
• F acts as a Hausdorff metric [START_REF] Munkres | Topology[END_REF] when specification labels are viewed as sets of implementation labels: for all k, ℓ ∈ Spec and α ∈ ▲,

F(k, ℓ, α) = sup m∈ k inf n∈ ℓ F(m, n, α).
• Sets of implementation labels are closed with respect to F: for all k, ℓ ∈ Spec and α ∈ ▲ with

F(k, ℓ, α) = ⊤ ▲ , there are m ∈ k , n ∈ ℓ with F(m, ℓ, α) = F(k, n, α) = F(k, ℓ, α).
• F satisfies an extended triangle inequality: for all k, ℓ, m ∈ Spec and α, β ∈ ▲,

F(k, ℓ, α) ⊕ ▲ F(ℓ, m, β ) ⊒ ▲ F(k, m, α ⊕ ▲ β ).
As the last ingredients, let h T : Spec ∞ × Spec ∞ → ▲ and g : ▲ → | ≥0 ∪ {∞} be functions such that g is monotone with g(⊥ ▲ ) = 0, g(α) = ∞ for α = ⊤ ▲ , and g • h T = d T , and such that h T has a recursive characterization, using F, as follows:

h T (σ , τ) =      F(σ 0 , τ 0 , h T (σ 1 , τ 1 )) if σ , τ = ε, ⊤ ▲ if σ = ε, τ = ε or σ = ε, τ = ε, ⊥ ▲ if σ = τ = ε. (1)
Here ε ∈ Spec ∞ denotes the empty sequence, and for any σ ∈ Spec ∞ , σ 0 denotes its first element and σ 1 the tail of σ with the first element removed.

For technical reasons, we will work mostly with the auxiliary function h T : Spec ∞ × Spec ∞ → ▲ below instead of the distance d T ; indeed, the framework in [START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF] has been developed completely without reference to the distance d T which, from a point of view of applications, should be the actual function of interest. This is due to the fact that the recursive characterization in (1) needs to "live" in ▲ to be applicable to non-trivial distances, cf. [START_REF] Fahrenberg | The Quantitative Linear-Time-Branching-Time Spectrum[END_REF].

We assume all SMTS to be compactly branching [START_REF] Franck Van Breugel | A Theory of Metric Labelled Transition Systems[END_REF], that is, for any SMTS S and any s ∈ S, the sets

{k ∈ Spec | s k s ′ } and {k ∈ Spec | s k -→ s ′ } are to be compact under the hemimetric d T . A SMTS S is said to be deterministic if it holds for all s ∈ S, s k 1 S s 1 , s k 2 S s 2 for which there is k ∈ Spec with h T (k, k 1 ) = ⊤ ▲ and h T (k, k 2 ) = ⊤ ▲ that k 1 = k 2 and s 1 = s 2 .

Operations

Any specification theory comes equipped with certain operations which allow high-level reasoning [START_REF] Bauer | Moving from Specifications to Contracts in Component-Based Design[END_REF]: refinement, structural composition and quotient, and conjunction. For our quantitative framework, we add an operation of widening which allows to systematically relax specifications.

The modal refinement distance d m : S × T → | ≥0 ∪ {∞} between the states of SMTS S, T is defined using an auxiliary function h m : S × T → ▲, which in turn is defined to be the least fixed point to the equations

h m (s,t) = max        sup s k S s ′ inf t ℓ T t ′ F(k, ℓ, h m (s ′ ,t ′ )), sup t ℓ -→ T t ′ inf s k -→ S s ′ F(k, ℓ, h m (s ′ ,t ′ )).
We let d m = g • h m , using the function g : ▲ → | ≥0 ∪ {∞} from above. Also, d m (S, T ) = d m (s 0 ,t 0 ), and we write S ≤ α m T if d m (S, T ) ⊑ ▲ α. This definition is an extension of the one of simulation distance in [START_REF] Fahrenberg | Distances for Weighted Transition Systems: Games and Properties[END_REF], and the proof of existence of the least fixed point is similar to the one in [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF]. Note also that d m extends the refinement relation ≤ m in the sense that s ≤ m t implies d m (s,t) = 0.

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

d t (S, T ) = sup I∈ S inf J∈ T d m (I, J),
and we write S ≤ α t T if d t (S, T ) ⊑ ▲ α. Again, S ≤ t T implies d t (S, T ) = 0. It can be shown [4]

d t (S, T ) = d m (S, T ) if T is deterministic [4].
To introduce structural composition and quotient of SMTS, one needs corresponding operators on labels. Let thus : Spec × Spec ֒→ Spec and : Spec × Spec → Spec be partial label operators which satisfy the following conditions:

• For all k, ℓ, k ′ , ℓ ′ ∈ Spec, if h T (k, ℓ) = ⊤ ▲ and h T (k ′ , ℓ ′ ) = ⊤ ▲ , then k k ′ is defined if and only if ℓ ℓ ′ is defined;
• 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, the following conditions are equivalent:

there exists k ∈ Spec for which both h T (k, ℓ) = ⊤ ▲ and d T (k, ℓ ′ ) = ⊤ ▲ ;

there exists m ∈ Spec for which both ℓ m and ℓ ′ m are defined; there exists m ∈ Spec for which both m ℓ and m ℓ ′ are defined. The structural composition of SMTS S, T is then 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 ′ )
It can be shown [START_REF] Bauer | Extending Modal Transition Systems with Structured Labels[END_REF] that for all SMTS S, S ′ , T , T ′ , S ≤ m T and

S ′ ≤ m T ′ imply S S ′ ≤ m T T ′ .
For a quantitative generalization of this, we need a function P : ▲ × ▲ → ▲ which permits 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. Then P can be used to bound distances between structural compositions: for SMTS S, T , S ′ , T ′ , we have h m (S S ′ , T T ′ ) ⊑ ▲

P(h m (S, T ), h m (S ′ , T ′ )) [4, Thm. 2].
For the definition of quotient, we first need to introduce pruning. For a SMTS S and a subset B ⊆ S of states, the pruning ρ B (S) is given as follows: Define a must-predecessor 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 ρ ). The quotient of an SMTS T by an SMTS 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
Note the extra universal state u which is introduced here. The standard property of quotient is as follows [START_REF] Bauer | Extending Modal Transition Systems with Structured Labels[END_REF]: For SMTS S, T , X, for which S is deterministic and T S exists, X ≤ m T S if and only if S X ≤ m T . Note that this property implies uniqueness (up to ≡ m ) of quotient [START_REF] Fahrenberg | Make a Difference! (Semantically)[END_REF]; hence if quotient exists, it must be defined as above.

For quantitative properties of quotient, we must again look to properties of the label operator which can ensure them. We say that is quantitatively well-behaved if it holds for all k, ℓ, m ∈ Spec that ℓ k is defined and h T (m, ℓ k) = ⊤ ▲ if and only if k m is defined and d T (k m, ℓ) = ⊤ ▲ , and in that case, F(m, ℓ k, α) ⊒ ▲ F(k m, ℓ, α) for all α ∈ ▲. For such a quantitatively well-behaved it can be shown [START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF]Thm. 3] that for all SMTS S, T , X such that S is deterministic and T S exists, h m (X, T S) ⊒ ▲ h m (S X, T ).

For conjunction of SMTS, we need a partial label operator : Spec × Spec → Spec for which it holds that

• for all k, ℓ ∈ Spec, if k ℓ is defined, then k ℓ ⊑ Spec k and k ℓ ⊑ Spec ℓ
• for all k, ℓ, m ∈ Spec for which m ⊑ Spec k and m ⊑ Spec ℓ, k ℓ is defined and m ⊑ Spec k ℓ, and • for all ℓ, ℓ ′ ∈ Spec, there exists k ∈ Spec for which h T (k, ℓ) = ⊤ ▲ and h T (k, ℓ ′ ) = ⊤ ▲ if and only if there exists m ∈ Spec for which ℓ m and ℓ ′ m are defined.

The conjunction of two SMTS S, 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 ℓ undefined (s,t) ∈ B t ℓ -→ T t ′ ∀s k S s ′ : k ℓ undefined (s,t) ∈ B
With this definition, it can be shown [START_REF] Bauer | Extending Modal Transition Systems with Structured Labels[END_REF] that conjunction acts as greatest lower bound: Given SMTS S, T for which S ∧ T is defined, we have S ∧ T ≤ m S and S ∧ T ≤ m T , and if S or T is deterministic and U is a SMTS for which U ≤ m S and U ≤ m T , then S ∧ T is defined and U ≤ m S ∧ T . We again note that this property implies uniqueness, up to ≡ m , of conjunction: if conjunction exists, it must be given as above.

To generalize this to a quantitative greatest lower bound property, we shall have reason to consider two different properties of the label operator . The first is analogous to the one for structural composition above: we say that is 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 T (m, k) = ∞ and d T (m, ℓ) = ∞ that k ℓ is defined and

F(m, k ℓ,C(α, α ′ )) ⊑ ▲ C(F(m, k, α), F(m, ℓ, α ′ ))
for all α, α ′ ∈ ▲. For such a bounded it can be shown [START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF] that if S, T , U are SMTS of which S or T is deterministic, and if h m (U, S) = ⊤ ▲ and h m (U, T ) = ⊤ ▲ , then S ∧ T is defined and h m (U, S ∧ T ) ⊑ ▲

C(h m (U, S), h m (U, T )).

For the second, relaxed boundedness property of , we have to first introduce a notion of quantitative widening. For α ∈ ▲ and SMTS S, T , we say that T is an α-widening of -→ T t ′ , for k ⊑ Spec ℓ, d(ℓ, k) ⊑ ▲ α, and (s ′ ,t ′ ) ∈ R. Thus up to unweighted two-sided refinement, T is the same as S, but transition labels in T can be α "wider" than in S. (Hence also S ≤ m T , but nothing general can be said about quantitative refinement from T to S, cf. [START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF].)

S
We say that the operator is relaxed bounded by a function family

C = {C β ,γ : ▲×▲ → ▲ | β , γ ∈ ▲} if all C β ,γ are monotone in both coordinates, have C β ,γ (⊥ ▲ , ⊥ ▲ ) = ⊥ ▲ , C β ,γ (α, ⊤ ▲ ) = C β ,γ (⊤ ▲ , α) =
⊤ ▲ for all α ∈ ▲, and if it holds for all k, ℓ ∈ Spec for which there is m ∈ Spec with h T (m, k) = ⊤ ▲ and h T (m, ℓ) = ⊤ ▲ that there exist k ′ , ℓ ′ ∈ Spec with k ⊑ Spec k ′ , ℓ ⊑ Spec ℓ ′ , h T (k ′ , k) = β = ⊤ ▲ , and h T (ℓ ′ , ℓ) = γ = ⊤ ▲ , such that k ′ ℓ ′ is defined, and then for all m ∈ Spec with h T (m, k) = ⊤ ▲ and

d T (m, ℓ) = ⊤ ▲ , F(m, k ′ ℓ ′ ,C β ,γ (α, α ′ )) ⊑ ▲ C β ,γ (F(m, k, α), F(m, ℓ, α ′ ))
for all α, α ′ ∈ ▲. The following property can then be shown [4, Thm. 5]: Let S, T be SMTS with S or T deterministic. If there is an SMTS U for which h m (U, S) = ⊤ ▲ and h m (U, T ) = ⊤ ▲ , then there exist β -and γ-widenings S ′ of S and T ′ of T for which S ′ ∧ T ′ is defined, and such that h m (U, S ′ ∧ T ′ ) ⊑ ▲ C β ,γ (h m (U, S), h m (U, T )) for all SMTS U for which h m (U, S) = ⊤ ▲ and h m (U, 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] 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. We assume a fixed finite alphabet Σ and let δ / ∈ Σ denote a special symbol which signifies passage of time. Let Φ(Σ) denote the set of closed clock constraints over Σ, given by A modal event-clock specification (MECS) [START_REF] Bertrand | A Compositional Approach on Modal Specifications for Timed Systems[END_REF] 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 ≤ k | a ≥ k | φ 1 ∧ φ 2 (a ∈ Σ, k ∈ ◆,φ 1 , φ 2 ∈ Φ(Σ)) .
A with g ⊆ g ′ . As before we write q a,g A q ′ instead of (q, a, g, q ′ ) ∈ A , similarly for -→ A . Figure 1 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 -→ s ′ . The semantics of a MECS A = (Q, q 0 , A , -→ A ) is the ITMTS A = (S, s 0 , S , -→ S ) given as follows:

Spec = (Σ × {[0, 0]}) ∪ ({δ } × ■) ⊆ (Σ ∪ {δ }) × ■, with (a, [l, r]) ⊑ Spec (a ′ , [l ′ , r ′ ]) if and only if a = a ′ , l ≥ l ′ , and r ≤ r ′ (hence [l, r] ⊆ [l ′ , r ′ ]),
S = {(q, v) | q ∈ Q, v : Σ → ■} s 0 = (q 0 , λ x.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]}
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 , also any of the "relaxed" or "robust" semantics of [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] are implementations of A ; any robust semantics "lives" in our framework. As we are using closed clock constraints for MECS, A as defined above is compactly branching.

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). 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 ), . . . , (a n , x n ) and σ ′ = (a 0 , x ′ 0 ), . . . , (a n , x ′ n ) (note that the discrete labels in Σ ∪ {δ } are the same), their timing difference is with the max m=0,...,n replaced by sup m∈◆ for infinite traces. This is precisely the maximum-lead distance of [START_REF] Henzinger | Quantifying Similarities Between Timed Systems[END_REF][START_REF] Thrane | Quantitative Simulations of Weighted Transition Systems[END_REF], and we show below how it fits in the framework of this paper.

|(x 0 + x 1 + • • • + x n ) -(x ′ 0 + x ′ 1 + • • • + x ′ n )|,
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 |x

0 -x ′ 0 | + λ |x 1 -x ′ 1 | + • • • + λ n |x n -x ′ n |
, 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 the more general approach of [START_REF] Bauer | General Quantitative Specification Theories with Modalities[END_REF].

Let ▲ = (| ≥0 ∪ {∞}) | , the set of mappings from leads to distances, define F :

Imp × Imp × ▲ → ▲ by F((a,t), (a ′ ,t ′ ), α) = ⊤ ▲ if a = a ′ , λ d. max(|d + t -t ′ |, α(d + t -t ′ )) if a = a ′
and extend F to specifications by F(k, ℓ, α) = sup m∈ k inf n∈ ℓ F(m, n, α). Define g : ▲ → | ≥0 ∪ {∞} by g(α) = α(0); the maximum-lead distance assuming the lead is zero. Using our characterization of h T from (1), it can then be shown that d T = g • h T : Spec ∞ × Spec ∞ → | ≥0 ∪ {∞} is precisely the maximumlead distance, cf. [START_REF] Fahrenberg | Distances for Weighted Transition Systems: Games and Properties[END_REF][START_REF] Henzinger | Quantifying Similarities Between Timed Systems[END_REF]. We also instantiate our definitions of modal and thorough refinement distance for ITMTS; for MECS A, B we let

d m (A, B) = d m ( A , B ), d t (A, B) = d t ( A , B ).
Determinism for ITMTS is the same as in [START_REF] Bauer | Quantitative Refinement for Weighted Modal Transition Systems[END_REF]

: if k 1 , k 2 ∈ Spec, with k 1 = (a 1 , [l 1 , r 1 ]), k 2 = (a 2 , [l 2 , r 2 ]),
then there is k ∈ Spec with h T (k, k 1 ) = ⊤ ▲ and h T (k, k 2 ) = ⊤ ▲ if and only if a 1 = a 2 . Hence an ITMTS S is deterministic if and only if it holds for all s ∈ S that s

(a,[l 1 ,r 1 ]) S s 1 and s (a,[l 2 ,r 2 ]) S s 2 imply [l 1 , r 1 ] = [l 2 , r 2 ]
and s 1 = s 2 . For an MECS A, A is hence deterministic if and only if for all locations q, q a,g 1 q 1 and q a,g 2 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.

For structural composition of ITMTS we use CSP-style synchronization on discrete labels and intersection of intervals. Note that this is different from [START_REF] Bauer | Quantitative Refinement for Weighted Modal Transition Systems[END_REF] which instead uses addition of intervals. Given (a, [l, r]), (a ′ , [l ′ , r ′ ]) ∈ Spec we hence define

(a, [l, r]) (a ′ , [l ′ , r ′ ]) = (a, [max(l, l ′ ), min(r, r ′ )]) if a = a ′ and max(l, l ′ ) ≤ min(r, r ′ ) , undefined otherwise .
It can be shown that is bounded by P(α, α ′ ) = max(α, α ′ ). Also, 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 2 depicts some examples of structural compositions. 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.

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 valuations u + d = λ a.(u(a) + d) and u[b] = λ a.(if a = b then 0 else u(a)). Note that for brevity we use lambda notation for anonymous functions here. 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 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(a) = [l a , r a ] ∈ ■ 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 v + d = λ a.(v(a) + [d, d]) and u[b] = λ a.(if a = b then [0, 0] else u(a)).

  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

Figure 1 :

 1 Figure1: 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 1 , S 2 .As customary, we omit may-transitions which have an underlying must-transition with the same label. Note that S 1 ≤ m S and S 2 ≤ m S, but d m (S 2 , S) = 1.

Figure 2 : 1 . 1 .

 211 Figure 2: A MECS model T of a process accessing the resource S from Fig. 1, together with the structural compositions S T , S 1 T , and S 2 T . Note that d m (S 2 T, S T ) = 1.

Figure 3 .

 3 It can be shown that the operator is quantitatively well-behaved.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 φ ′ φ = λ a.(φ ′ (a) φ (a))

  and what interests us is the maximal timing difference at any point of the runs. Hence we want the distance between σ and σ ′ to be max m=0,...,n | ∑

		get		get		get
		grant		grant		get ≤ 4
	grant get ≤ 5	get ≤ 2	extra	get ≤ 1	grant get ≤ 1	grant	extra	grant get ≤ 3
						get
		S		S 1		S 2
						m i=0 x i -∑ m i=0 x ′ i |, and

A Robust Specification Theory for Modal Event-Clock Automata 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 2. Let A, B, X be MECS for which B A exists, then B A

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 [4, Thm. 3], and by the same theorem, h m (X, B A) ⊑ h m (A X, B), so as g : ▲ → | ≥0 ∪ {∞}, the claim follows.

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 synchronized transition has to satisfy both interval constraints. It can be shown that is not bounded, but relaxed bounded by

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 = λ 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 nwidening of an 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. Theorem 3. 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]