Sebastian S Bauer

Uli Fahrenberg

Line Juhl

Kim G Larsen

Axel Legay

Claus Thrane

Weighted Modal Transition Systems

Keywords: reducing complexity of design, modal specification, quantitative reasoning

Specification theories as a tool in model-driven development processes of component-based software systems have recently attracted a considerable attention. Current specification theories are however qualitative in nature, and therefore fragile in the sense that the inevitable approximation of systems by models, combined with the fundamental unpredictability of hardware platforms, makes it difficult to transfer conclusions about the behavior, based on models, to the actual system. Hence this approach is arguably unsuited for modern software systems. We propose here the first specification theory which allows to capture quantitative aspects during the refinement and implementation process, thus leveraging the problems of the qualitative setting.

Our proposed quantitative specification framework uses weighted modal transition systems as a formal model of specifications. These are labeled transition systems with the additional feature that they can model optional behavior which may or may not be implemented by the system. Satisfaction and refinement is lifted from the wellknown qualitative to our quantitative setting, by introducing a notion of distances between weighted modal transition systems. We show that quantitative versions of parallel composition as well as quotient (the dual to parallel composition) inherit the properties from the Boolean setting.

Introduction

One of the major current challenges to rigorous design of software systems is that these systems are becoming increasingly complex and difficult to reason about [START_REF] Sifakis | A vision for computer science -the system perspective[END_REF]. As an example, an integrated communication system in a modern airplane can have more than 10 900 distinct states [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF], and state-of-the-art tools offer no possibility to reason about, and model check, the system as a whole.

One promising approach to overcome such problems is the one of compositional and incremental design. Here the reasoning is done as much as possible at higher specification levels rather than at implementations; partial specifications are proven correct and then composed and refined until one arrives at an implementation model. Practice has shown that this is indeed a viable approach [START_REF]COMponent-Based Embedded Systems design Techniques[END_REF][START_REF] Speeds | SPEculative and Exploratory Design in Systems Engineering[END_REF].

Specifications of system requirements are high-level finite abstractions of possibly infinite sets of implementations. A model of a system is considered an implementation of a given specification if the behavior defined by the implementation is implied by the description provided by the specification.

Any practical specification formalism comes equipped with a number of operations which allow compositional and incremental reasoning. The first of these is a refinement relation which allows to successively distill specifications into more detailed ones and eventually into implementations. In an implementation, all optional behavior defined in the specification has been decided upon in compliance with the specification.

Also needed is an operation of logical conjunction which allows to combine specifications so that the systems which refine the conjunction of two specifications are precisely the ones which satisfy both partial specifications. Refinement and conjunction together allow for incremental reasoning as specifications are successively refined and composed.

For compositional reasoning, one needs an operation of structural composition which allows to infer specifications from sub-specifications of independent requirements, mimicking at the implementation level e.g. the interaction of components in a distributed system. A partial inverse of this operation is given by the quotient operation which allows to synthesize a specification of the missing components from an overall specification and an implementation which realizes a part of the overall specification.

Over the years, there have been a series of advances on specification theories [START_REF] De | Interface-based design[END_REF][START_REF] Chakrabarti | Synchronous and bidirectional component interfaces[END_REF][START_REF] David | Timed I/O automata: A complete specification theory for real-time systems[END_REF][START_REF] Delahaye | Modular Specification and Compositional Analysis of Stochastic Systems[END_REF][START_REF] Lynch | An introduction to input/output automata[END_REF][START_REF] Nyman | Modal Transition Systems as the Basis for Interface Theories and Product Lines[END_REF][START_REF] Thrane | Quantitative Models and Analysis For Reactive Systems[END_REF]. The predominant approaches are based on modal logics and process algebras but have the drawback that they cannot naturally embed both logical and structural composition within the same formalism [START_REF] Kim | Modal specifications[END_REF]. Hence such formalisms do not permit to reason incrementally through refinement.

In order to leverage these problems, the concept of modal transition systems was introduced [START_REF] Kim | Modal specifications[END_REF]. In short, modal transition systems are labeled transition systems equipped with two types of transitions: must transitions which are mandatory for any implementation, and may transitions which are optional for implementations. It is well established that modal transition systems match all the requirements of a reasonable specification theory (see also [START_REF] Raclet | Residual for component specifications[END_REF] for motivation), and much progress has been made using modal specifications, see e.g. [START_REF] Antonik | 20 years of modal and mixed specifications[END_REF] for an overview. Also, practical experience shows that the formalism is expressive enough to handle complex industrial problems [START_REF]COMponent-Based Embedded Systems design Techniques[END_REF][START_REF] Speeds | SPEculative and Exploratory Design in Systems Engineering[END_REF]. receive deliver check deliver Fig. 1 Modal transition system modeling a simple email system, with an optional behavior: Once an email is received it may e.g. be scanned for containing viruses, or automatically decrypted, before it is delivered to the receiver. receive d el iv er ch ec k ch ec k deliver deliver Fig. 2 An implementation of the simple email system in Figure 1 in which we explicitly model two distinct types of email pre-processing.

As an example, consider the modal transition system shown in Figure 1 which models the requirements of a simple email system in which emails are first received and then delivered. Before delivering the email, the system may check or process the email, e.g. for en-or decryption, filtering of spam emails, or generating automatic answers using has an auto-reply feature (see also [START_REF] Hall | Feature interactions in electronic mail[END_REF]). Must transitions, representing obligatory behavior, are drawn as solid arrows, whereas may transitions, modeling optional behavior, are shown as dashed arrows; hence any implementation of this email system specification must be able to receive and deliver email, and it may also be able to check arriving email before delivering it. No other behavior is allowed.

Implementations can also be represented within the modal transition system formalism, simply as specifications without may transitions. Hence any implementation choice has been resolved, and implementations are plain labeled transition systems. Formally, for a labeled transition system to be an implementation of a given specification, we require that the states of the two objects are related by a refinement relation with the property that all behavior required (must) by the specification has been implemented, and that any implementation behavior was permitted (may) in the specification. Figure 2 shows an implementation of our email specification with two different checks, leading to distinct processing states. Note that a simple system without any check at all, hence only able to receive and deliver email, is also an implementation of the specification.

Motivated by applications to embedded, real-time and hybrid systems, the modal transition system framework has recently been extended in order to reason about quantitative aspects [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF][START_REF] Juhl | Modal transition systems with weight intervals[END_REF]. With these applications in mind, it is necessary not only to be able to specify quantitative aspects of systems, but also to formalize successive refinement of quantities. To illustrate this extension, consider again the modal transition system of Figure 1, but this time with quantities, see Figure 3: Every transition label is extended by integer intervals modeling upper and lower bounds on time required for performing the corresponding actions. For instance, the recep-receive, [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF] deliver, [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Antonik | 20 years of modal and mixed specifications[END_REF] check, [0,[START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF] deliver, [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] De | Interface-based design[END_REF] Fig. [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF] Specification of a simple email system, similar to Figure 1, but extended by integer intervals modeling time units for performing the corresponding actions.

tion of a new email (action receive) must take between one and three time units, the checking of the email (action check ) is allowed to take up to five time units.

In this quantitative setting, there is a problem with using a Boolean notion of refinement (as is done in [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF][START_REF] Juhl | Modal transition systems with weight intervals[END_REF]): If one only can decide whether or not an implementation refines a specification, then the quantitative aspects get lost in the refinement process. As an example, consider the email system implementations in Figure 4. Implementation (a) does not refine the specification, as there is an error in the discrete structure of actions: after receiving an email, the system can check it indefinitely without ever delivering it. Also implementations (b) and (c) do not refine the specification: (b) takes too long to receive email, (c) does not deliver email fast enough after checking it. Implementation (d) on the other hand is a perfect refinement of the specification.

Intuitively however, implementations (b) and (c) conform much better to the specification than implementation (a) in Figure 4: there are no discrepancies in the discrete structure, only the weights are off by 1. Additionally, the quantitative error in implementation (c) occurs later than the one in (b). Hence one may want to say that implementation (d) is in perfect refinement of the specification, (c) is slightly off, (b) is a bit more problematic, whereas implementation (a) is completely unacceptable. A Boolean notion of refinement does not allow to make such distinctions between different negative answers.

To sum up, a Boolean notion of refinement is too fragile for quantitative formalisms. Minor and major modifications in the implementation cannot be distinguished, as both of them may reverse the Boolean answer. As observed in [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF], this view is obsolete; engineers need quantitative notions on how modified implementations differ. The introduction of such a quantitative notion of refinement, and its consequences for the specification theory, are the subject of this paper.

In the above examples, the transition weights have expressed the time used to perform the associated action. However our formalism is abstract enough to also model other quantitative aspects such as e.g. energy consumption or financial aspects. For instance, Figure 5 presents a simple electronic wiper control component for a car, with a normal mode and an optional fast mode. Integer intervals express the allowed energy consumption of each action (using abstract energy units).

Depending on the precise application of our quantitative formalism, there are a few choices which one has to make. One such choice is the precise definition of quantitative refinement, as the way quantitative discrepancies between specifications is measured e.g. depends on whether differences accumulate over time or the interest more lies in the maximal individual differences. Another choice is how to combine quantities during structural composition: when modeling e.g. energy consumption, they should be added; when modeling timing constraints, some form of conjunction wipe, [START_REF] De | Interface-based design[END_REF][START_REF] Antonik | 20 years of modal and mixed specifications[END_REF]

fast, [0, 1] normal, [0, 1]
wipeFast, [START_REF] Antonik | 20 years of modal and mixed specifications[END_REF][START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF] d e a c ti v a te , [0 , 1 ] should be used. To simplify presentation, we develop the theory in this paper for one specific kind of quantitative refinement and one specific choice of composition; a more general treatment is deferred to future work.

To facilitate quantitative reasoning on specifications and implementations, we introduce a real-valued distance between specifications such that perfect refinement corresponds to distance 0, small quantitative discrepancies give rise to small distances, and differences in the discrete control structure correspond to distance ∞.

For the examples in Figs. 3 and4, we will hence deduce the following chain of decreasing distances:

∞ = d(I 1 , S) > d(I 2 , S) > d(I 3 , S) > d(I 4 , S) = 0
Our distance is discounted in the sense that behaviors which occur d steps in the future are discounted by a factor λ d , where λ with 0 < λ < 1 is a fixed discounting factor.

Using a reduction to discounted games [START_REF] Zwick | The complexity of mean payoff games[END_REF], we show that this so-called modal distance is computable in NP ∩ co-NP. As any specification can be seen as the (generally infinite) set of implementations which are in perfect refinement, we also have a natural notion of so-called thorough distance between specifications which is given by the (Hausdorff) distance between their implementation sets; we show that computing through distances is Exptime-hard.

Replacing Boolean refinement by distances has an impact on operations between specifications. As a second contribution of this paper, we propose quantitative versions of structural composition and quotient which inherit the good properties from the Boolean setting. We also propose a new notion of relaxation which is inherent to the quantitative framework and allows e.g. to calibrate the quotient operator: If the overall specification is too restrictive with respect to a partial implementation to synthesize a meaningful specification of the missing components, the overall specification may be relaxed to facilitate a better quotient.

However, there is no free lunch, and working with distances has a price: some of the properties of logical conjunction and determinization are not preserved in our quantitative setting. More precisely, conjunction is not the greatest lower bound with respect to refinement distance as it is in the Boolean setting, and deterministic overapproximation is too coarse. In fact we show that this is a fundamental limitation of any reasonable quantitative specification formalism.

Our final contribution consists of showing that a quantitative interpretation of Hennessy-Milner logic provides a logical characterization which is sound with respect to refinement distance and complete for the disjunction-free fragment.

Related work. The objective of the paper is to propose a new complete quantitative modal specification theory, which exploits a notion of distance between specifications. This distance builds on previous work of some of the authors [START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Fahrenberg | The quantitative linear-time-branchingtime 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 Models and Analysis For Reactive Systems[END_REF][START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF]. For the sake of completeness, we briefly put it in perspective with other notions of distances proposed, particularly but not exclusively for probabilistic systems, in recent years. These include [START_REF] Franck Van Breugel | Topological Models in Comparative Semantics[END_REF][START_REF] Franck Van Breugel | A theory of metric labelled transition systems[END_REF] which develop a theory of metric transition systems and introduce the notion of compact branching, [START_REF] De | Quantitative verification and control via the mu-calculus[END_REF][START_REF] Luca De Alfaro | Discounting the future in systems theory[END_REF][START_REF] Desharnais | Metrics for labelled Markov processes[END_REF][START_REF] Majumdar | Symbolic Algorithms for Verification and Control[END_REF] which introduce discounting distances for Markov decision processes, and [START_REF] Chatterjee | Algorithms for game metrics[END_REF][START_REF] Luca De Alfaro | Game refinement relations and metrics[END_REF] which generalize these to a game setting.

For a non-probabilistic setting of metric transition systems (different from van Breugel's), notions of discounting linear and branching distances are developed in [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF], and an important theoretical contribution is [START_REF] Bonsangue | Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding[END_REF] which develops a theory of directed distances, or hemimetrics as they have come to be called, and relate completion of hemimetric spaces to Yoneda embeddings (see also [START_REF] Lawvere | Metric spaces, generalized logic, and closed categories[END_REF][START_REF] Lawvere | Taking categories seriously[END_REF]). Another, language-based approach to quantitative verification, related to the theory of semiring-weighted automata [START_REF] Droste | Weighted automata and weighted logics[END_REF][START_REF] Droste | Handbook of Weighted Automata[END_REF][START_REF] Droste | Weighted automata and weighted logics with discounting[END_REF], can be found in [START_REF] Černý | Simulation distances[END_REF][START_REF] Chatterjee | Expressiveness and closure properties for quantitative languages[END_REF].

Structure of the paper. The paper starts by introducing our quantitative formalism which has weighted transition systems as implementations and weighted modal transition systems as specifications. In Section 3 we introduce the distances we use for quantitative comparison of both implementations and specification, and Section 4 provides complexity results for the computation of these distances. Section 5 is devoted to a formalization of the notion of relaxation which is of great use in quantitative design. In Section 6 we see some inherent limitations of the quantitative approach, and Section 7 shows that structural composition works as expected in the quantitative framework and links relaxation to quotients. Section 8 finishes the paper by providing logical characterizations of refinement distance.

Weighted Modal Transition Systems

In this section we present the formalism we use for implementations and specifications. As implementations we choose the model of weighted transition systems, i.e. labeled transition systems with integer weights at transitions. Specifications both have a modal dimension, specifying discrete behavior which must be implemented and behavior which may be present in implementations, and a quantitative dimension, specifying intervals of weights on each transition within are permissible for an implementation.

Let ■ = [x, y] x ∈ ) ∪{-∞}, y ∈ ) ∪{∞}, x ≤ y be the set of closed extendedinteger intervals and let Σ be a finite set of actions. Our set of specification labels is K = Σ × ■, pairs of actions and intervals. The set of implementation labels is defined as

Imp = Σ × [x, x] x ∈ ) ≈ Σ × ).
Hence a specification imposes labels and integer intervals which constrain the possible weights of an implementation.

We define a partial order on ■ (representing inclusion of intervals) by [x, y] ⊑ [x ′ , y ′ ] if x ′ ≤ x and y ≤ y ′ , and we extend this order to specification labels by (a, I) ⊑ (a ′ , I ′ ) if a = a ′ and I ⊑ I ′ . The partial order on K is hence a refinement order; if

k 1 ⊑ k 2 for k 1 , k 2 ∈ K, then no more implementation labels are contained in k 1 than in k 2 .
Specifications and implementations are defined as follows:

Definition 1 A weighted modal transition system (WMTS) is a quadruple (S, s 0 , , -→) consisting of a set of states S with an initial state s 0 ∈ S and must (-→) and may ( ) transition relations -→, ⊆ S ×K×S such that for every

(s, k, s ′ ) ∈ -→ there is (s, ℓ, s ′ ) ∈ where k ⊑ ℓ. A WMTS is an implementation if -→ = ⊆ S × Imp × S.
Note the natural requirement that any required (must) behavior is also allowed (may) above, and that implementations correspond to standard integer-weighted transition systems, where all optional behavior and positioning in the intervals has been decided on.

A WMTS is finite if S and (and hence also -→) are finite sets, and it is deterministic if it holds that for any s ∈ S and a ∈ Σ, s, (a, I 1 ), t 1 , s, (a, I 2 ), t 2 ∈ imply I 1 = I 2 and t 1 = t 2 . Hence a deterministic specification allows at most one transition under each discrete action from every state. In the rest of the paper we will write s k s ′ for (s, k, s ′ ) ∈ and similarly for -→, and we will always write S = (S, s 0 , , -→) or S i = (S i , s 0 i , i , -→ i ) for WMTS and I = (I, i 0 , -→) for implementations. Note that an implementation is just a usual integer-weighted transition system.

Our theory will work with infinite WMTS, though we will require them to be compactly branching. This is a natural generalization of the standard requirement on systems to be finitely branching which was first used in [START_REF] Franck Van Breugel | A theory of metric labelled transition systems[END_REF]; see Definition 7 below.

The implementation semantics of a specification is given through modal refinement, as follows:

Definition 2 A modal refinement of WMTS S 1 , S 2 is a relation R ⊆ S 1 × S 2 such that for any (s 1 , s 2 ) ∈ R -whenever s 1 k 1 1 t 1 for some k 1 ∈ K, t 1 ∈ S 1 , then there exists s 2 k 2 2 t 2 for some k 2 ∈ K, t 2 ∈ S 2 , such that k 1 ⊑ k 2 and (t 1 , t 2 ) ∈ R, -whenever s 2 k 2 -→ 2 t 2 for some k 2 ∈ K, t 2 ∈ S 2 , then there exists s 1 k 1 -→ 1 t 1 for some k 1 ∈ K, t 1 ∈ S 1 , such that k 1 ⊑ k 2 and (t 1 , t 2 ) ∈ R.
We write S 1 ≤m S 2 if there is a modal refinement relation R for which (s 0

1 , s 0 2 ) ∈ R.
Hence in such a modal refinement, behavior which is required in S 2 is also required in S 1 , no more behavior is allowed in S 1 than in S 2 , and the quantitative requirements in S 1 are refinements of the ones in S 2 . The implementation semantics of a specification can then be defined as the set of all implementations which are also refinements: Definition 3 The implementation semantics of a WMTS S is the set S = {I | I ≤m S and I is an implementation}. This conforms with the intuition developed in the introduction: if I ∈ S , then any (reachable) behavior i a,x -→ j in I must be allowed by a matching transition s a, [l,r] t in S with l ≤ x ≤ r; correspondingly, any (reachable) required behavior

s a,[l,r] -→ t in S must be implemented by a matching transition i a,x -→ j in I with l ≤ x ≤ r.

Thorough and Modal Refinement Distances

For the quantitative specification formalism we have introduced in the last section, the standard Boolean notions of satisfaction and refinement are too fragile. To be able to reason not only whether a given quantitative implementation satisfies a given quantitative specification, but also to what extent, we introduce a notion of distance between both implementations and specifications.

We 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)

Note that as our (hemi-, pseudo-)metrics may take the values ∞, some authors will refer to them as extended (hemi-, pseudo-)metrics.

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 ′ ).
We first define the distance between implementations; for this we introduce a distance on implementation labels by

d Imp (a 1 , x 1 ), (a 2 , x 2 ) = ∞ if a 1 = a 2 , |x 1 -x 2 | if a 1 = a 2 .
(

) 1
In the rest of the paper, let λ ∈ | with 0 < λ < 1 be a discounting factor.

i1 j1 k1 3 7 6 9 i2 j2 6 7 d(j1, j2) = 0 d(i1, j2) = ∞ d(j1, i2) = ∞ d(k1, j2) = ∞ d(k1, i2) = max{2 + .9 d(k1, i2), .9 0 d(j1, j2)} d(i1, i2) = max{3 + .9 d(j1, j2) 0 , .9 d(k1, i2)}
d(i 1 , i 2 ) = max        sup i1 k 1 -→1j1 inf i2 k 2 -→2j2 d Imp (k 1 , k 2 ) + λd(j 1 , j 2 ), sup i2 k 2 -→2j2 inf i1 k 1 -→1j1 d Imp (k 1 , k 2 ) + λd(j 1 , j 2 ). We define d(I 1 , I 2 ) = d(i 0 1 , i 0 2 ).

Lemma 1

The implementation distance is well-defined, and is a pseudometric.

Proof Except for the symmetrizing max operation, this is precisely the accumulating branching distance from [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF]. Because of λ < 1, the equations above define a contraction (with Lipschitz constant λ), so the Banach fixed point theorem (for extended metric spaces) applies. Hence besides the fixed point d(i 1 , i 2 ) = ∞, the contraction has at most one other fixed point, i.e. there exists indeed a unique least fixed point. We refer to [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF] for a more detailed proof.

Symmetry of d is clear, and so is the property d(i, i) = 0. The triangle inequality can be shown inductively, cf. [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF]. ⊓ ⊔

We remark that besides this accumulating distance, other interesting system distances may be defined depending on the application at hand, cf. [START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF][START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF], but we concentrate here on this distance and leave a generalization to other distances for future work.

Example 1 Consider the two implementations I 1 and I 2 in Figure 6 with a single action (elided for simplicity) and with discounting factor λ = .9. The equations in the illustration have already been simplified by removing all expressions that evaluate to ∞. What remains to be done is to compute the least fixed point of the equation d(k 1 , i 2 ) = max 2 + .9 d(k 1 , i 2 ), 0 . Clearly 0 is not a fixed point, and solving the equation

d(k 1 , i 2 ) = 2 + .9 d(k 1 , i 2 ) gives d(k 1 , i 2 ) = 20. Hence d(i 1 , i 2 ) = max{3, .9 • 20} = 18.
Note that the interpretation of the distance between two implementations depends entirely on the application one has in mind; but it can easily be shown [START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF] that the distance between two implementations is zero if and only if they are weighted bisimilar. The intuition is then that the smaller the distance, the closer the implementations are to being bisimilar.

To lift the implementation distance to specifications, we need first to consider the distance between sets of implementations. Given implementation sets I 1 , I 2 , we define

d(I 1 , I 2 ) = sup I1∈I1 inf I2∈I2 d(I 1 , I 2 )
Note that in case I 2 is finite, we have that for all ε ≥ 0, d(I 1 , I 2 ) ≤ ε if and only if for each implementation I 1 ∈ I 1 there exists I 2 ∈ I 2 for which d(I 1 , I 2 ) ≤ ε, hence this is quite a natural notion of distance. Especially, d(I 1 , I 2 ) = 0 if I 1 is a subset of I 2 up to bisimilarity. For infinite I 2 , we have the slightly more complicated property that d(I 1 , I 2 ) ≤ ε if and only if for all δ > 0 and any I 1 ∈ I 1 , there is

I 2 ∈ I 2 for which d(I 1 , I 2 ) ≤ ε + δ.
Also remark the similarity of this definition to the one of Hausdorff distance between subsets of a metric space, see e.g. [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF]Sect. 3.16]. Crucially however, our distance is missing the symmetrizing max operation of Hausdorff distance, hence it is asymmetric. We may well have d(I 1 , I 2 ) = d(I 2 , I 1 ) and will thus prefer to speak of the distance from I 1 to I 2 rather than between I 1 and I 2 . We lift this distance to specifications as follows:

Definition 5 The thorough refinement distance between WMTS S 1 and S 2 is de- fined as d t (S 1 , S 2 ) = d S 1 , S 2 . We write S 1 ≤ ε t S 2 if d t (S 1 , S 2 ) ≤ ε. Lemma 2 The thorough refinement distance is a hemimetric.
Proof To show that d t (S, S) = 0 is trivial, and the triangle inequality

d t (S 1 , S 2 ) + d T (S 2 , S 3 ) ≥ d t (S 1 , S 3 ) follows like in the proof of [3, Lemma 3.72]. ⊓ ⊔
Indeed this permits us to measure incompatibility of specifications; intuitively, if two specifications have thorough distance ε, then any implementation of the first specification can be matched by an implementation of the second up to ε. Also observe the special case where S 1 = I 1 is an implementation: then

d t (I 1 , S 2 ) = inf I2∈ S2 d(I 1 , I 2 ), which measures how close I 1 is to satisfy the specification S 2 .
To facilitate computation and comparison of refinement distance, we introduce modal refinement distance as an overapproximation. We will show in Theorem 3 below that similarly to the Boolean setting [START_REF] Beneš | Checking thorough refinement on modal transition systems is EXPTIME-complete[END_REF], computation of thorough refinement distance is Exptime-hard, whereas modal refinement distance is computable in NP ∩ co-NP.

First we generalize the distance on implementation labels from Equation (1) to specification labels, again using a Hausdorff-type construction. For k, ℓ ∈ K we define

d K (k, ℓ) = sup k ′ ⊑k,k ′ ∈Imp inf ℓ ′ ⊑ℓ,ℓ ′ ∈Imp d Imp (k ′ , ℓ ′ ).
Note that d K is asymmetric, and that d K (k, ℓ) = 0 if and only if k ⊑ ℓ. Also,

d K (k, ℓ) = d Imp (k, ℓ) for all k, ℓ ∈ Imp.
In more elementary terms, we can express d K as follows:

d K (a 1 , I 1 ), (a 2 , I 2 ) = ∞ if a 1 = a 2 d K (a, [x 1 , y 1 ]), (a, [x 2 , y 2 ]) = max(x 2 -x 1 , y 1 -y 2 , 0) Definition 6 Let S 1 , S 2 be WMTS. The modal refinement distance dm : S 1 × S 2 →
| ≥0 ∪ {∞} from states of S 1 to states of S 2 is the least fixed point of the equations

dm(s 1 , s 2 ) = max        sup s1 k 1 1 t1 inf s2 k 2 2 t2 d K (k 1 , k 2 ) + λdm(t 1 , t 2 ), sup s2 k 2 -→2t2 inf s1 k 1 -→1t1 d K (k 1 , k 2 ) + λdm(t 1 , t 2 ).
We define dm(S 1 , S 2 ) = dm(s 0 1 , s 0

2 ), and we write

S 1 ≤ ε m S 2 if dm(S 1 , S 2 ) ≤ ε.

Lemma 3

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

Proof Like in the proof of Lemma 1, the argument for existence of a unique least fixed point to the defining equations is that they define a contraction. The triangle inequality can again be shown inductively, and the property dm(s, s) = 0 is clear.

⊓ ⊔

We can now give a precise definition of compact branching; for this we need the notions of symmetrization of a hemimetric and of product distance as defined on page 8.

Definition 7 A WMTS S is said to be compactly branching if the sets {(s ′ , k) | s k s ′ }, {(s ′ , k) | s k -→ s ′ } ⊆ S × K are compact under the symmetrized product distance dm × dK for every s ∈ S.
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 the standard requirement on transition systems to be finitely branching to a distance setting; we will need it for the property that continuous functions defined on the sets

{(s ′ , k) | s k s ′ }, {(s ′ , k) | s k -→ s ′ } ⊆ S × K,
for some s ∈ S, attain their infimum and supremum, see Lemma 5 and its proof below.

Thus, we shall henceforth assume all our WMTS to be compactly branching. The following lemma sets up some sufficient conditions for this to be the case.

Lemma 4 Let S be a WMTS and define the sets

L i (s, a), U i (s, a) for all s ∈ S, a ∈ Σ and i ∈ {1, 2} by L 1 (s, a) = {l | s a,[l,r] s ′ }, L 2 (s, a) = {l | s a,[l,r] -→ s ′ }, U 1 (s, a) = {r | s a,[l,r] s ′ }, U 2 (s, a) = {r | s a,[l,r] -→ s ′ }.
(s ′ n ) n∈◆ in {s ′ | s -→ s ′ } has limn→∞ sn ∈ {s ′ | s -→ s ′ },
and for all s ∈ S, a ∈ Σ and i ∈ {1, 2}, L i is finite or -∞ ∈ L i , and

U i is finite or ∞ ∈ U i .
Note that the first property mimicks (and generalizes) standard properties of finite branching and saturation, cf. [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF]Sect. 3.3]. The intuition is that if s has (either may or must) transitions to a converging sequence of states, then it also has a transition to the limit.

Proof The first condition implies that the sets {s ′ ∈ S | s s ′ } and {s ′ ∈ S | s -→ s ′ } are compact in the pseudometric dm for all s ∈ S. By Tychonoff's theorem, products of compact sets are compact, so we need only show that the second condition implies that the sets

{k ∈ K | s k s ′ } and {k ∈ K | s k -→ s ′ } are compact in the pseudometric dK for every s ∈ S. Let s ∈ S. By definition of d K , the sets {k | s k s ′ }, {k | s k -→ s ′ } fall into connected components {I | s a,I s ′ }, {I | s a,I -→ s ′ }
for all a ∈ Σ, hence the former are compact if and only if all the latter are. These in turn are compact if and only if the four sets L i , U i in the lemma, collecting lower and upper bounds of intervals, are compact. Now interval bounds are extended integers, so a sequence in L i or U i converges if and only if it is eventually stable or goes towards -∞ or ∞. If the sets are finite, eventual stability is the only option; if they are infinite, they need to include the limit points -∞ (for the lower interval bounds in L i ) or ∞ (for the upper interval bounds in U i ). ⊓ ⊔ There is a powerful proof technique introduced for branching distances between implementations in [START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF] that we here extend to modal refinement distance. We define a modal refinement family as an | ≥0 -indexed family of relations R = {Rε ⊆ S 1 ×S 2 | ε ≥ 0} such that for any ε and any (s 1 , s 2 ) ∈ Rε, -whenever s 1

k 1 t 1 for some k 1 ∈ K, t 1 ∈ S 1 , then there exists s 2 k 2 t 2 for some k 2 ∈ K, t 2 ∈ S 2 , such that d K (k 1 , k 2 ) ≤ ε and (t 1 , t 2 ) ∈ R ε ′ for some ε ′ ≤ λ -1 ε -d K (k 1 , k 2 ) , -whenever s 2 k 2 -→ t 2 for some k 2 ∈ K, t 2 ∈ S 2 , then there exists s 1 k 1 -→ t 1 for some k 1 ∈ K, t 1 ∈ S 1 , such that d K (k 1 , k 2 ) ≤ ε and (t 1 , t 2 ) ∈ R ε ′ for some ε ′ ≤ λ -1 ε -d K (k 1 , k 2 ) .
Note that modal refinement families are

-upward closed in the sense that (s 1 , s 2 ) ∈ Rε implies that (s 1 , s 2 ) ∈ R ε ′ for all ε ′ ≥ ε, and
downward closed in the sense that for any set

E ⊆ | ≥0 , if (s 1 , s 2 ) ∈ Rε for all ε ∈ E, then also (s 1 , s 2 ) ∈ R inf E .
This property follows from the assumption that our WMTS are compactly branching.

Following the proof strategy developed in [START_REF] Thrane | Quantitative simulations of weighted transition systems[END_REF] for implementations, we can show the following characterization of modal refinement distance by modal refinement families:

Lemma 5 S 1 ≤ ε m S 2 if and only if there is a modal refinement family R with (s 0 1 , s 0 2 ) ∈ Rε ∈ R. Proof First, assume that S 1 ≤ ε m S 2 , i.e. dm(s 0 1 , s 0
2 ) ≤ ε, and define a relation family

R = {R δ | δ ≥ 0} by R δ = {(s 1 , s 2 ) ∈ S 1 × S 2 | dm(s 1 , s 2 ) ≤ δ} for all δ ≥ 0, then (s 0 1 , s 0
2 ) ∈ Rε holds by assumption. We show that R is a modal refinement family. Let (s 1 , s 2 ) ∈ R δ for some δ ≥ 0, then by definition we know that dm(s

1 , s 2 ) ≤ δ. Assume s 1 k 1 1 t 1 . From dm(s 1 , s 2 ) ≤ δ we can infer that inf s2 k 2 2 t2 d K (k 1 , k 2 ) + λdm(t 1 , t 2 ) ≤ δ.
Hence, because S 2 is compactly branching, there exists a may-transition s 2

k 2 t 2 such that d K (k 1 , k 2 ) ≤ δ and dm(t 1 , t 2 ) ≤ λ -1 (δ -d K (k 1 , k 2 )). The latter implies that (t 1 , t 2 ) ∈ R δ ′ for some δ ′ ≤ λ -1 (δ -d K (k 1 , k 2 )
) which was to be shown. The argument for the other assertion for must-transitions is symmetric. This proves that there is a modal refinement family R such that (s 0 1 , s 0

2 ) ∈ Rε ∈ R. For the reverse direction, assume that (s 0

1 , s 0 2 ) ∈ Rε ∈ R for some modal refine- ment family R = {Rε | ε ≥ 0}. We prove that (s 1 , s 2 ) ∈ R δ , for some δ ≥ 0, implies dm(s 1 , s 2 ) ≤ δ. The claim S 1 ≤ ε m S 2 then follows from the assumption (s 0 1 , s 0 2 ) ∈ Rε. s1 S1 t1 a, [0, 1] s2 S2 t2 t3 a , [0 , 0 ] a , [1 , 1 ]
Fig. 7 Incompleteness of modal refinement distance: dt(S 1 , S 2 ) = 0, but dm(S 1 , S 2 ) = ∞.

To this end, observe that the space of functions ∆ = [S 1 ×S 2 → | ≥0 ∪{∞}] forms a complete lattice, when the partial order ≤ ∆ is defined such that for f,

f ′ ∈ ∆, f ≤ ∆ f ′ iff f (s 1 , s 2 ) ≤ f ′ (s 1 , s 2 ) for all s 1 ∈ S 1 , s 2 ∈ S 2 .
Moreover, since max, sup, inf and + are monotone, the function D defined for all f ∈ ∆ by

D(f ) = max        sup s1 k 1 1 t1 inf s2 k 2 2 t2 d K (k 1 , k 2 ) + λf (t 1 , t 2 ), sup s2 k 2 -→2t2 inf s1 k 1 -→1t1 d K (k 1 , k 2 ) + λf (t 1 , t 2 )
is a monotone endofunction on ∆, hence by Tarski's fixed point theorem, D has a least fixed point. Now let us define h(s

1 , s 2 ) = inf{δ | (s 1 , s 2 ) ∈ R δ ∈ R}, and since R δ is downward closed, we have that (s 1 , s 2 ) ∈ R h(s1,s2) . By showing that h is a pre-fixed point of D, i.e. that D(h) ≤ ∆ h, we get that (s 1 , s 2 ) ∈ R δ implies that dm(s 1 , s 2 ) ≤ δ, since h(s 1 , s 2 ) ≤ δ and dm(s 1 , s 2 ) ≤ h(s 1 , s 2 ). Since (s 1 , s 2 ) ∈ R h(s1,s2) every s 1 k 1 s ′
1 can be matched by some s 2

k 2 s ′ 2 such that d K (k 1 , k 2 ) + λδ ′ ≤ h(s 1 , s 2 ) for some δ ′ where (s ′ 1 , s ′ 2 ) ∈ R δ ′ , implying h(s ′ 1 , s ′ 2 ) ≤ δ ′ , but then also d K (k 1 , k 2 ) + λh(s ′ 1 , s ′ 2 ) ≤ h(s 1 , s 2 ). Similarly, every s 2 k 2 -→ s ′ 2 has a match s 1 k 1 -→ s ′ 1 such that d K (k 1 , k 2 ) + λh(s ′ 1 , s ′ 2 ) ≤ h(s 1 , s 2
). Hence we have D(h) ≤ ∆ h which was to be shown. ⊓ ⊔

The next theorems show that modal refinement distance indeed overapproximates thorough refinement distance, and that it is exact for deterministic WMTS. Note that nothing general can be said about the precision of the overapproximation in the nondeterministic case; as an example observe the two specifications in Figure 7 for

which d t (S 1 , S 2 ) = 0 but dm(S 1 , S 2 ) = ∞.
Theorem 1 For WMTS S 1 , S 2 we have d t (S 1 , S 2 ) ≤ dm(S 1 , S 2 ).

Proof If dm(S 1 , S 2 ) = ∞, we have nothing to prove. Otherwise, let R = {Rε ⊆ S 1 × S 2 | ε ≥ 0} be a modal refinement family which witnesses dm(S 1 , S 2 ), i.e. such that (s 0 1 , s 0 2 ) ∈ R dm(S1,S2) , and let I 1 ∈ S 1 . We have to expose I 2 ∈ S 2 for which d(I 1 , I 2 ) ≤ dm(S 1 , S 2 ).

Let R 1 ⊆ I 1 × S 1 be a witness for

I 1 ≤m S 1 , define R ′ ε = R 1 • Rε ⊆ I 1 × S 2 for all ε ≥ 0, and let R ′ = {R ′ ε | ε ≥ 0}. The states of I 2 = (I 2 , i 0 2 , Imp, -→ I2 ) are I 2 = S 2 with i 0 2 = s 0 2
, and the transitions we define as follows:

For any i 1 k ′ 1 -→ I1 j 1 and any s 2 ∈ S 2 for which (i 1 , s 2 ) ∈ R ′ ε ∈ R ′ for some ε, we have s 2 k 2 2 t 2 in S 2 with d K (k ′ 1 , k 2 ) ≤ ε and (j 1 , t 2 ) ∈ R ′ ε ′ ∈ R ′ for some ε ′ ≤ λ -1 ε -d K (k ′ 1 , k 2 ) . Write k ′ 1 = (a ′ 1 , x ′ 1 ) and k 2 = a 2 , [x 2 , y 2 ] , then we must have a ′ 1 = a 2 . Let x ′ 2 =      x 2 if x ′ 1 < x 2 , x ′ 1 if x 2 ≤ x ′ 1 ≤ y 2 , y 2 if x ′ 1 > y 2 (2) and k ′ 2 = (a 2 , x ′ 2 ), and put s 2 k ′ 2 -→ I2 t 2 in I 2 . Note that d K (k ′ 1 , k ′ 2 ) = d K (k ′ 1 , k 2 ). (3)
Similarly, for any s 2

k 2 -→ 2 t 2 in S 2 and any i 1 ∈ I 1 with (i 1 , s 2 ) ∈ R ′ ε ∈ R ′ for some ε, we have i 1 k ′ 1 -→ I1 j 1 with d K (k ′ 1 , k 2 ) ≤ ε and (j 1 , t 2 ) ∈ R ′ ε ′ ∈ R ′ for some ε ′ ≤ λ -1 ε -d K (k ′ 1 , k 2 ) . Write k ′ 1 = (a ′ 1 , x ′ 1 ) and k 2 = (a 2 , [x 2 , y 2 ]), define x ′ 2 as in (2) and k ′ 2 = (a 2 , x ′ 2 ), and put s 2 k ′ 2 -→ I2 t 2 in I 2 . We show that the identity relation id S2 = {(s 2 , s 2 ) | s 2 ∈ S 2 } ⊆ S 2 ×S 2 witnesses I 2 ≤m S 2 . Let first s 2 k ′ 2
-→ I2 t 2 ; we must have used one of the two constructions above for creating this transition. In the first case, we have -→ 2 t 2 on the other hand, we have introduced

s 2 k 2 2 t 2 with k ′ 2 ⊑ k 2 ,
s 2 k ′ 2 -→ I2 t 2 in the second construction above, with k ′ 2 ⊑ k 2 .
We also want to show that the family R ′ is a witness for d(I 1 , I 2 ) ≤ dm(S 1 , S 2 ). We have

(i 0 1 , s 0 2 ) ∈ R ′ dm(S1,S2) = R 1 • R dm(S1,S2) , so let (i 1 , s 2 ) ∈ R ′ ε ∈ R ′ for some ε ≥ 0. For any i 1 k ′ 1 -→ I1 j 1 we have s 2 k 2 2 t 2 and s 2 k ′ 2 -→ I2 t 2 by the first part of our construction above, with d K (k ′ 1 , k ′ 2 ) = d K (k ′ 1 , k 2 ) ≤ ε because of (3)
, and also (j

1 , t 2 ) ∈ R ′ ε ′ ∈ R ′ for some ε ′ ≤ λ -1 ε -d K (k ′ 1 , k 2 ) . For any s 2 k ′ 2
-→ I2 t 2 , we must have used one of the constructions above to introduce this transition, and both give us

i 1 k ′ 1 -→ I1 j 1 with d K (k ′ 1 , k ′ 2 ) ≤ ε and (j 1 , t 2 ) ∈ R ′ ε ′ ∈ R ′ for some ε ′ ≤ λ -1 ε -d K (k ′ 1 , k 2 ) . ⊓ ⊔
The fact that modal refinement only equals thorough refinement for deterministic specifications is well-known from the theory of modal transition systems [START_REF] Kim | Modal specifications[END_REF], and the special case of S 2 deterministic is important, as it can be argued [START_REF] Kim | Modal specifications[END_REF] that indeed, deterministic specifications are sufficient for applications. 2 ) ∈ R dt(S1,S2) and whenever we have (s 1 , s 2 ) ∈ Rε ∈ R, s 1 a,I 1 1 t 1 , and s 2 a,I 2 2 t 2 , then (t 1 , t 2 ) ∈ R λ -1 (ε-dK((a,I1),(a,I2))) .

Theorem 2 If

We show below that this definition makes sense (also that εd K (a, I 1 ), (a, I 2 ) ≥ 0 in all cases), and that R is a modal refinement family. We will use the convenient notation (s 1 , S 1 ) for the WMTS S 1 with initial state s 0 1 replaced by s 1 , similarly for (s 2 , S 2 ).

We first show inductively that for any pair of states (s 1 , s 2 ) ∈ Rε ∈ R we have d t (s 1 , S 1 ), (s 2 , S 2 ) ≤ ε. This is obviously the case for s 1 = s 0 1 and s 1 = s 0 2 , so assume now that (s 1 , s 2 ) ∈ Rε ∈ R is such that d t (s 1 , S 1 ), (s 2 , S 2 ) ≤ ε and let

s 1 a,I 1 1 t 1 , s 2 a,I 2 2 t 2 . Let (q ′ 1 , P ′ 1 ) ∈ (t 1 , S 1 ) and x 1 ∈ I 1 .
There is an implementation (p 1 , P 1 ) ∈ (s 1 , S 1 ) for which p 1 a,x 1 -→ q 1 and such that (q 1 , P 1 ) ≤m (q ′ 1 , P ′ 1 ). Now

d t (p 1 , P 1 ), (s 2 , S 2 ) ≤ d t (p 1 , P 1 ), (s 1 , S 1 ) + d t (s 1 , S 1 ), (s 2 , S 2 ) ≤ ε, hence we must have s 2 a ′ 2 ,I ′ 2 2 t ′ 2 with d K (a, x 1 ), (a ′ 2 , I ′ 2 ) ≤ ε. But then a ′ 2 = a, hence by determinism of S 2 , I 2 = I ′ 2 and t 2 = t ′ 2 .
The above considerations hold for any x 1 ∈ I 1 , hence d K (a, I 1 ), (a, I 2 ) ≤ ε. Thus εd K (a, I 1 ), (a, I 2 ) ≥ 0, and the definition of R above is justified. Now let x 2 ∈ I 2 such that d K (a, x 1 ), (a, x 2 ) = d K (a, x 1 ), (a, I 2 ) , then there is an implementation (p 2 , P 2 ) ∈ (s 2 , S 2 ) for which p 2 a,x 2 -→ q 2 , and

d (q ′ 1 , P ′ 1 ), (q 2 , P 2 ) ≤ λ -1 ε -d K ((a, x 1 ), (a, x 2 )) = λ -1 ε -d K ((a, I 1 ), (a, I 2 )) ,
which, as (q ′ 1 , P ′ 1 ) ∈ (t 1 , S 1 ) was chosen arbitrarily, entails d t (s 1 , S 1 ), (s 2 , S 2 ) ≤ λ -1 ε -d K ((a, I 1 ), (a, I 2 )) .

We are ready to show that R is a refinement family. Let (s 1 , s 2 ) ∈ Rε ∈ R for some ε, and assume s 1 -→ q 2 with x 2 ∈ I 2 , thus there is also p 1 a,x 1 -→ q 1 with d K (a, x 1 ), (a, x 2 ) ≤ ε and d (q 1 , P 1 ), (q 2 , P 2 ) ≤ λ -1 ε -d K ((a, x 1 ), (a, x 2 )) . This in turn implies that s 1 a,I 1 -→ 1 t 1 for some x 1 ∈ I 1 . We will be done once we can show d K (a, I 1 ), (a, I 2 ) ≤ ε, so assume to the contrary that there is

x ′ 1 ∈ I 1 with d K (a, x ′ 1 ), (a, I 2 ) > ε. Then there is an implementation (p ′ 1 , P ′ 1 ) ∈ (s 1 , S 1 ) with p ′ 1 a,x ′ 1 -→ q ′ 1 , hence a transition s 2 a,I ′ 2 2 t ′ 2 with d K (a, x ′ 1 ), (a, I ′ 2 ) ≤ ε. But I ′ 2 = I 2 by determinism of S 2 , a contradiction. ⊓ ⊔

Complexity of Computing Thorough and Modal Refinement Distances

The complexity results in the next theorem show that modal refinement distance can serve as a useful approximation of thorough refinement distance.

Theorem 3 For finite WMTS S 1 , S 2 and ε ≥ 0, it is Exptime-hard to decide whether S 1 ≤ ε t S 2 . The problem whether S 1 ≤ ε m S 2 is decidable in NP ∩ co-NP.

The fact that computing thorough refinement distance is EXPTIME-hard is easy. By [START_REF] Beneš | Checking thorough refinement on modal transition systems is EXPTIME-complete[END_REF], deciding thorough refinement for MTS (without weights) is EXPTIMEcomplete. By translating MTS to WMTS with weight 0 on all transitions, deciding thorough refinement for modal transition systems polynomial-time reduces to deciding whether thorough refinement distance is ≤ 0.

To show an upper bound on the complexity of computing modal refinement distance, we need to introduce discounted values of weighted games, cf. [START_REF] Zwick | The complexity of mean payoff games[END_REF]. A weighted game graph is a finite real-weighted bipartite digraph

(V 1 , V 2 , -), i.e. with V 1 ∩ V 2 = ∅ and -∈ (V 1 × | × V 2 ) ∪ (V 2 × | × V 1
) a finite set of edges. These are assumed to be non-blocking in the sense that each v ∈ V 1 ∪ V 2 has at least one outgoing edge v r w (which is the shorthand for (v, r, w) ∈ -).

A Player-1 strategy in such a weighted game graph is a mapping θ

1 : V 1 → |×V 2 for which v 1 , θ 1 (v 1 ) ∈ -for each v 1 ∈ V 1 . Similarly, a Player-2 strategy is a mapping θ 2 : V 2 → | × V 1 such that v 2 , θ 2 (v 2 ) ∈ -for each v 2 ∈ V 2 .
The sets of all Player-1 and Player-2 strategies are denoted Θ 1 and Θ 2 , respectively.

Denote by tgt(e) = w the target of an edge e = (v, r, w) ∈ -and by wt(e) = r its weight. A vertex v 0 ∈ V 1 and a pair (θ 1 , θ 2 ) ∈ Θ 1 × Θ 2 of strategies determine a unique infinite sequence e j (θ 1 , θ 2 ) j≥0 of edges e j (θ 1 , θ 2 ) ∈ -for which

e 0 (θ 1 , θ 2 ) = v 0 , θ 1 (v 0 ) , e 2j+1 (θ 1 , θ 2 ) = tgt(e 2j ), θ 2 (tgt(e 2j )) , e 2j (θ 1 , θ 2 ) = tgt(e 2j-1 , θ 1 (tgt(e 2j-1 )) .
In other words, the two players alternate to pick edges inaccording to their strategies. The discounted value of the game

(V 1 , V 2 , -) played from v 0 ∈ V 1 with discounting factor λ, 0 ≤ λ < 1, is defined to be p(v 0 , λ) = sup θ1∈Θ1 inf θ2∈Θ2 ∞ j=0 λ j wt e j (θ 1 , θ 2 ) .
We recall the following theorem from [START_REF] Zwick | The complexity of mean payoff games[END_REF]; the complexity result is obtained by reduction to simple stochastic games [START_REF] Condon | The complexity of stochastic games[END_REF].

Lemma 6 ([46])

The discounted value p(v 0 , λ) may be computed as the unique fixed point to the equations

p(v, λ) =      max v r -w r + λp(w, λ) if v ∈ V 1 , min v r -w r + λp(w, λ) if v ∈ V 2 .

The decision problem corresponding to computing

p(v 0 ) is contained in NP ∩ co-NP.
Next we present a reduction from modal refinement distance of WMTS to discounted values of weighted games, cf. [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF].

Lemma 7 For WMTS S 1 , S 2 one can construct in polynomial time a weighted game

(V 1 , V 2 , -) with a vertex v 0 ∈ V 1 such that dm(S 1 , S 2 ) = p(v 0 , √ λ). Proof Let V 1 = S 1 × S 2 , V 2 = S 1 × S 2 × K × {may, must}
, and define the transitions as follows:

(s 1 , s 2 ) 0 -(t 1 , s 2 , k 1 , may) if s 1 k 1 1 t 1 (s 1 , s 2 ) 0 -(s 1 , t 2 , k 2 , must) if s 2 k 2 -→ 2 t 2 (t 1 , s 2 , k 1 , may) dK(k1,k2) - (t 1 , t 2 ) if s 2 k 2 2 t 2 (s 1 , t 2 , k 2 , must) dK(k1,k2) - (t 1 , t 2 ) if s 1 k 1 -→ 1 t 1 Setting v 0 = (s 0 1 , s 0
2 ) finishes the construction. ⊓ ⊔

In [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF] it is also shown that conversely, computing discounted values of weighted games may be polynomial-time reduced to computing simulation distance for weighted transition systems, hence we can conclude the following.

Lemma 8 The decision problem corresponding to computing modal refinement distance for WMTS is polynomial-time equivalent to the decision problem corresponding

to computing discounted values of weighted games.

Relaxation

We introduce here a notion of relaxation which is specific to the quantitative setting. Intuitively, relaxing a specification means to weaken the quantitative constraints, while the discrete demands on which transitions may or must be present in implementations are kept. A similar notion of strengthening may be defined, but we do not use this here.

Definition 8

For WMTS S, S ′ and ε ≥ 0, S ′ is an ε-relaxation of S if S ≤m S ′ and

S ′ ≤ ε m S.
Hence the quantitative constraints in S ′ may be more permissive than the ones in S, but no new discrete behavior may be introduced. Also note that any implementation of S is also an implementation of S ′ , and no implementation of S ′ is further than ε away from an implementation of S. The following proposition relates specifications to relaxed specifications:

Proposition 1 If S ′ 1 and S ′ 2 are ε-relaxations of S 1 and S 2 , respectively, then dm(S 1 , S 2 )-ε ≤ dm(S 1 , S ′ 2 ) ≤ dm(S 1 , S 2 ) and dm(S 1 , S 2 ) ≤ dm(S ′ 1 , S 2 ) ≤ dm(S 1 , S 2 )+ ε.
Proof By the triangle inequality we have

dm(S 1 , S ′ 2 ) ≤ dm(S 1 , S 2 ) + dm(S 2 , S ′ 2 ), dm(S 1 , S 2 ) ≤ dm(S 1 , S ′ 2 ) + dm(S ′ 2 , S 2 ), dm(S 1 , S 2 ) ≤ dm(S 1 , S ′ 1 ) + dm(S ′ 1 , S 2 ), dm(S ′ 1 , S 2 ) ≤ dm(S ′ 1 , S 1 ) + dm(S 1 , S 2 ).⊓ ⊔
On the syntactic level, we can introduce the following widening operator which relaxes all quantitative constraints in a systematic manner. We write I ± δ = [xδ, y + δ] for an interval I = [x, y] and δ ∈ ◆. Widening and relaxation are related as follows; note also that as widening is a global operation whereas relaxation may be achieved entirely locally, not all relaxations may be obtained as widenings.

Proposition 2

The δ-widening of any WMTS S is a (1λ) -1 δ-relaxation. s t u a, [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF][START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF] a, [START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF][START_REF] Basu | Statistical abstraction and model-checking of large heterogeneous systems[END_REF] (a) S

s +1 t +1 u +1
a, [START_REF] Antonik | 20 years of modal and mixed specifications[END_REF][START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] a, [START_REF] Antonik | 20 years of modal and mixed specifications[END_REF][START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] (b) S +1 i j k a, 15 a, 5

(c) I Fig. 8 WMTS S and implementation I for which I ∈ S +(1-λ) -1 δ , for δ = 1 and λ = .9 (thus (1 -λ) -1 δ = 10), but I / ∈ S +δ , so that S +δ S +(1-λ) -1 δ , even though S +δ is a

(1 -λ) -1 δ-relaxation of S.
Proof For the first claim, the identity relation

id S = {(s, s) | s ∈ S} ⊆ S × S is a witness for S ≤m S +δ : if s k t, then by construction s k 2 +δ t with k ⊑ k 2 ,

and if

s k 2 -→ +δ t, then again by construction s k -→ t for some k ⊑ k 2 . Now to prove dm(S +δ , S) ≤ (1 -λ) -1 δ, we define a family of relations R = {Rε | ε ≥ 0} by Rε = ∅ for ε < (1 -λ) -1 δ and Rε = id S for ε ≥ (1 -λ) -1 δ. We show that R is a modal refinement family.
Let (s, s) ∈ Rε for some ε ≥ (1λ) -1 δ, and assume s k 2 +δ t. By construction there is a transition

s k t with d K (k 2 , k) ≤ δ ≤ ε. Now 1 λ ε -d K (k 2 , k) ≥ 1 λ δ 1 -λ -δ = δ 1 -λ ≥ ε
and (t, t) ∈ Rε, which settles this part of the proof. The other direction, starting with a transition

s k -→ t, is similar. ⊓ ⊔
There is also an implementation-level notion which corresponds to relaxation:

Definition 10 The ε-extended implementation semantics, for ε ≥ 0, of a WMTS S is S +ε = I I ≤ ε m S, I implementation . Proposition 3 If S ′ is an ε-relaxation of S, then S ′ ⊆ S +ε .
Proof If I ∈ S ′ , then dm(I, S ′ ) = 0, hence dm(I, S) ≤ ε by Proposition 1, which in turn implies that I ∈ S +ε . ⊓ ⊔

The example in Figure 8 shows that there are WMTS S, S ′ such that S ′ is an ε-relaxation of S but the inclusion S ′ ⊆ S +ε is strict. Indeed, for δ = 1 and λ = .9, we have I ∈ S +(1-λ) -1 δ , but I / ∈ S +δ .

Limitations of the Quantitative Approach

In this section we turn our attention towards some of the standard operators for specification theories; determinization and logical conjunction. In the standard Boolean setting, there is indeed a determinization operator which derives the smallest deterministic overapproximation of a specification, which is useful because it enables checking thorough refinement, cf. Theorem 2. Quite surprisingly, we show that in the quantitative setting, there are problems with these notions which do not appear in the Boolean theory. More specifically, we show that there is no determinization operator which always yields a smallest deterministic overapproximation, and there is no conjunction operator which acts as a greatest lower bound.

Theorem 4 There is no unary operator D on WMTS for which it holds that This D ′ can be defined as follows: For a WMTS S = (S, s 0 ,

, -→), D ′ (S) = P(S) \ {∅}, {s 0 }, d , -→ d ,
where P(S) is the power set of S and the transition relations d and -→ d are defined as follows: Let T ∈ (P(S) \ {∅}) be a state in D ′ (S). For every maximal, nonempty set La ⊆ {I | ∃s ∈ T : s a,I } for some a ∈ Σ, we have T a, La d Ta where Ta = {s ′ ∈ S | ∃s ∈ T , I ∈ La : s a,I s ′ } and La is the smallest interval containing all intervals from La. If, moreover, for each s ∈ T we have s a,I -→ s ′ for some s ′ ∈ Ta and some I ∈ La, then T a, La -→ d Ta. It is straightforward to prove that D ′ satisfies the expected properties.

Assume now that there is an operator D as in the theorem. Then for any WMTS S, S ≤m D ′ (S) and thus D(S) ≤m D ′ (S) by (4.3), and S ≤m D(S) and hence D ′ (S) ≤m D(S) by (4.3 ′ ). We finish the proof by showing that the operator D ′ does not satisfy (4.3). The example in Figure 9 shows a WMTS S and a deterministic WMTS D for which dm D ′ (S), D = 3 + 3λ and dm(S, D) = max(3, 3λ) = 3, hence dm D ′ (S), D ≤ dm(S, D). ⊓ ⊔ Likewise, the greatest-lower-bound property of logical conjunction in the Boolean setting ensures that the set of implementations of a conjunction of specifications is precisely the intersection of the implementation sets of the two specifications. Conjoining two WMTS naturally involves a partial label conjunction operator . We let (a 1 , I 1 ) (a 2 , I 2 ) be undefined if a 1 = a 2 , and otherwise

a, [x 1 , y 1 ] a, [x 2 , y 2 ] =      a, [max(x 1 , x 2 ), min(y 1 , y 2 )] if max(x 1 , x 2 ) ≤ min(y 1 , y 2 ), undefined otherwise.
Before we show that such a conjunction operator for WMTS does not exist in general, we need to define a pruning operator which removes inconsistent states that naturally arise when conjoining two WMTS. The intuition is that if a WMTS S 1 requires a behavior s 1 k 1 -→ 1 for which there is no may transition s 2 k 2 2 such that k 1 k 2 is defined, then the state (s 1 , s 2 ) in the conjunction is inconsistent and will have to be pruned away, together with all must transitions leading to it. In the definition below, pre * denotes the reflexive, transitive closure of pre. Definition 11 For a WMTS S, let pre : 2 S → 2 S be given by pre

(B) = {s ∈ S | s k -→ t ∈ B for some k}. Let ⊆ S be a set of inconsistent states. If s 0 / ∈ pre * ( ), then the pruning of S w.r.t. is defined by ρ (S) = (Sρ, s 0 , ρ, -→ρ) where Sρ = S \ pre * ( ), ρ = ∩ Sρ × K × Sρ and -→ρ = -→ ∩ Sρ × K × Sρ . s0 s1 s2 s3 s4 a , [3 , 3 ]
a , [5 , 6 ] a, [0, 0] a, [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF] (a) S {s0} {s1, s2} {s3, s4} a, [START_REF] Aliprantis | Infinite Dimensional Analysis: A Hitchhiker's Guide[END_REF][START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] a, [0, 3]

(b) D ′ (S) d0 d1 d2 a, [2, 3] a, [0, 0] (c)
s t a, [1, 2] (a) S s1 t1 a, [0, 1] (b) S 1 s2 t2 a, [2, 3] (c) S 2 (s1, s2) (d) S 1 ∧S 2
Fig. 10 Counter-example for Theorem 5: dm(S, S 1 ) = dm(S, S 2 ) = 1, but dm(S, S 1 ∧S 2 ) = ∞.

Theorem 5 There is no partial binary operator ∧ on WMTS for which it holds that, for all WMTS S, S 1 , S 2 such that S 1 and S 2 are deterministic, (5.1) whenever S 1 ∧ S 2 is defined, then S 1 ∧ S 2 ≤m S 1 and S 1 ∧ S 2 ≤m S 2 , (5.2) whenever S ≤m S 1 and S ≤m S 2 , then S 1 ∧ S 2 is defined and S ≤m S 1 ∧ S 2 , (5.3) for any ε ≥ 0, there exist

ε 1 ≥ 0 and ε 2 ≥ 0 such that if S 1 ∧ S 2 is defined, S ≤ ε1 m S 1 and S ≤ ε2 m S 2 , then S ≤ ε m S 1 ∧ S 2 .
Proof We follow the same strategy as in the proof of Theorem 4. One can define a partial conjunction operator ∧ ′ defined for WMTS which satisfies Properties (5.1) and (5.2) as follows: For deterministic WMTS S 1 and S 2 ,

S 1 ∧ ′ S 2 = ρ (S 1 × S 2 , (s 0 1 , s 0
2 ), , -→) where the transition relations and -→ and the set ⊆ S 1 × S 2 of inconsistent states are defined by the following rules:

s 1 k 1 -→ s ′ 1 s 2 k 2 s ′ 2 k 1 k 2 defined (s, t) k 1 k 2 -→ (s ′ 1 , s ′ 2 ) s 1 k 1 s ′ 1 s 2 k 2 -→ s ′ 2 k 1 k 2 defined (s 1 , s 2 ) k 1 k 2 -→ (s ′ 1 , s ′ 2 ) s 1 k 1 s ′ 1 s 2 k 2 s ′ 2 k 1 k 2 defined (s 1 , s 2 ) k 1 k 2 (s ′ 1 , s ′ 2 ) s 1 k 1 -→ k 1 k 2 undefined for any k 2 such that s 2 k 2 (s 1 , s 2 ) ∈ s 2 k 2 -→ k 1 k 2 undefined for any k 1 such that s 1 k 1 (s 1 , s 2 ) ∈
Using these properties, one can see that for all deterministic WMTS S 1 and S 2 , S 1 ∧ S 2 ≤m S 1 ∧ ′ S 2 and S 1 ∧ ′ S 2 ≤m S 1 ∧ S 2 . The WMTS depicted in Figure 10 then show that Property (5.3) cannot hold: here, dm(S, S 1 ) = dm(S, S

2 ) = 1, but dm(S, S 1 ∧ S 2 ) = ∞. ⊓ ⊔
The counterexamples used in the proofs of Theorems 4 and 5 are quite general and apply to a large class of distances, rather than only to the accumulating distance discussed in this paper. Hence it can be argued that what we have exposed here is a fundamental limitation of any quantitative approach to modal specifications.

Structural Composition and Quotient

In this section we show that in our quantitative setting, notions of structural composition and quotient can be defined which obey the properties expected of such operations. In particular, structural composition satisfies independent implementability [START_REF] De | Interface-based design[END_REF], hence the refinement distance between structural composites can be bounded by the distances between their respective components.

First we define partial synchronization operators ⊕ and ⊖ on specification labels which will be used for synchronizing transitions. We let (a 1 , I 1 ) ⊕ (a 2 , I 2 ) and (a 1 , I 1 ) ⊖ (a 2 , I 2 ) be undefined if a 1 = a 2 , and otherwise

a, [x 1 , y 1 ] ⊕ a, [x 2 , y 2 ] = a, [x 1 + x 2 , y 1 + y 2 ] , a, [x 1 , y 1 ] ⊖ a, [x 2 , y 2 ] = undefined if x 1 -x 2 > y 1 -y 2 , a, [x 1 -x 2 , y 1 -y 2 ] if x 1 -x 2 ≤ y 1 -y 2 .
Note that we use CSP-style synchronization, but other types of synchronization can easily be defined. Also, defining ⊕ to add intervals (and ⊖ to subtract them) is only one particular choice; depending on the application, one can also e.g. let ⊕ be intersection of intervals or some other operation. It is not difficult to see that these alternative synchronization operators would lead to properties similar to those we show here.

Definition 12

Let S 1 and S 2 be WMTS. The structural composition of S 1 and S 2 is S 1 S 2 = S 1 × S 2 , (s 0 1 , s 0

2 ), K, , -→ with transitions given as follows:

s 1 k 1 1 t 1 s 2 k 2 2 t 2 k 1 ⊕ k 2 defined (s 1 , s 2 ) k 1 ⊕k 2 (t 1 , t 2 ) s 1 k 1 -→ 1 t 1 s 2 k 2 -→ 2 t 2 k 1 ⊕ k 2 defined (s 1 , s 2 ) k 1 ⊕k 2 -→ (t 1 , t 2 ) The quotient of S 1 by S 2 is S 1 S 2 = ρ S 1 × S 2 ∪ {u}, (s 0 1 , s 0 2 ), K,
, -→ with transitions and the set of inconsistent states given as follows:

s 1 k 1 1 t 1 s 2 k 2 2 t 2 k 1 ⊖ k 2 defined (s 1 , s 2 ) k 1 ⊖k 2 (t 1 , t 2 ) s 1 k 1 -→ 1 t 1 s 2 k 2 -→ 2 t 2 k 1 ⊖ k 2 defined (s 1 , s 2 ) k 1 ⊖k 2 -→ (t 1 , t 2 ) s 1 k 1 -→ 1 t 1 ∀s 2 k 2 -→ 2 t 2 : k 1 ⊖ k 2 undefined (s 1 , s 2 ) ∈ k ∈ K ∀s 2 k 2 2 t 2 : k ⊕ k 2 undefined (s 1 , s 2 ) k u k ∈ K u k u
Note that during the quotient S 1 S 2 inconsistent states can arise which are then recursively removed using the pruning operator ρ, see Definition 11. After a technical lemma, the next theorem shows that structural composition is well-behaved with respect to modal refinement distance in the sense that the distance between the composed systems is bounded by the distances of the individual systems. Note also the special case in the theorem of S 1 ≤m S 2 and S 3 ≤m S 4 implying S 1 S 3 ≤m S 2 S 4 .

Lemma 9 For

k 1 , k 2 , k 3 , k 4 ∈ K with k 1 ⊕ k 3 and k 2 ⊕ k 4 defined, we have d K (k 1 ⊕ k 3 , k 2 ⊕ k 4 ) ≤ d K (k 1 , k 2 ) + d K (k 3 , k 4 ).
Proof Let k i = a, [x i , y i ] for all i. We have

d K (k 1 , k 2 ) + d K (k 3 , k 4 ) = max(x 2 -x 1 , y 1 -y 2 , 0) + max(x 4 -x 3 , y 3 -y 4 , 0) ≥ max (x 2 -x 1 ) + (x 4 -x 3 ), (y 1 -y 2 ) + (y 3 -y 4 ), 0 = max (x 2 + x 4 ) -(x 1 + x 3 ), (y 1 + y 3 ) -(y 2 + y 4 ), 0 = d K (k 1 ⊕ k 3 , k 2 ⊕ k 4 ). ⊓ ⊔
Theorem 6 (Independent implementability) For WMTS S 1 , S 2 , S 3 , S 4 we have dm S 1 S 3 , S 2 S 4 ≤ dm(S 1 , S 2 ) + dm(S 3 , S 4 ).

Proof If dm(S 1 , S 2 ) = ∞ or dm(S 3 , S 4 ) = ∞, we have nothing to prove. Otherwise, let R 1 = {R 1 ε ⊆ S 1 × S 2 | ε ≥ 0}, R 2 = {R 2 ε ⊆ S 3 × S 4 | ε ≥ 0}
be witnesses for dm(S 1 , S 2 ) and dm(S 3 , S 4 ), respectively; hence (s 0

1 , s 0 2 ) ∈ R 1 dm(S1,S2) ∈ R 1 and (s 0 3 , s 0 4 ) ∈ R 2 dm(S3,S4) ∈ R 2 . Define Rε = (s 1 , s 3 ), (s 2 , s 4 ) ∈ S 1 × S 3 × S 2 × S 4 (s 1 , s 2 ) ∈ R 1 ε1 ∈ R 1 , (s 3 , s 4 ) ∈ R 2 ε2 ∈ R 2 , ε 1 + ε 2 ≤ ε
for all ε ≥ 0 and let R = {Rε | ε ≥ 0}. We show that R witnesses dm S 1 S 3 , S 2 S 4 ≤ dm(S 1 , S 2 ) + dm(S 3 , S 4 ). We have (s 0 1 , s 0

3 ), (s 0 2 , s 0 4 ) ∈ R dm(S1,S2)+dm(S3,S4) ∈ R. Now let Lemma 9, and (t 1 , t 3 ), (t 2 , t 4 ) ∈ R ε ′ ∈ R. The reverse direction, starting with a transition (s 2 , s 4 )

(s 1 , s 3 ), (s 2 , s 4 ) ∈ Rε ∈ R for some ε, then (s 1 , s 2 ) ∈ R 1 ε1 ∈ R 1 and (s 3 , s 4 ) ∈ R 2 ε2 ∈ R 2 for some ε 1 + ε 2 ≤ ε. Assume (s 1 , s 3 ) k 1 ⊕k 3 (t 1 , t 3 ), then s 1 k 1 1 t 1 and s 3 k 3 3 t 3 . By (s 1 , s 2 ) ∈ R 1 ε1 ∈ R 1 , we have s 2 k 2 2 t 2 with d K (k 1 , k 2 ) ≤ ε 1 and (t 1 , t 2 ) ∈ R 1 ε ′ 1 ∈ R 1 for some ε ′ 1 ≤ λ -1 ε 1 -d K (k 1 , k 2 ) ; similarly, s 4 k 4 4 t 4 with d K (k 3 , k 4 ) ≤ ε 2 and (t 3 , t 4 ) ∈ R 2 ε ′ 2 ∈ R 2 for some ε ′ 2 ≤ λ -1 ε 2 -d K (k 3 , k 4 ) . Let ε ′ = ε ′ 1 + ε ′ 2 , then the sum k 2 ⊕ k 4 is defined, and ε ′ ≤ λ -1 ε 1 + ε 2 -(d K (k 1 , k 2 ) + d K (k 3 , k 4 )) ≤ λ -1 ε -d K (k 1 ⊕ k 3 , k 2 ⊕ k 4 ) by Lemma 9. We have (s 2 , s 4 ) k 2 ⊕k 4 (t 2 , t 4 ), d K (k 1 ⊕ k 3 , k 2 ⊕ k 4 ) ≤ ε 1 + ε 2 ≤ ε again by
k 2 ⊕k 4 -→ (t 2 , t 4 ), is similar. ⊓ ⊔
Again after a technical lemma, the next theorem expresses the fact that quotient is a partial inverse to structural composition. Intuitively, the theorem shows that the quotient S 1 S 2 is maximal among all WMTS S 3 with respect to any distance S 2 S 3 ≤ ε m S 1 ; note the special case of S 3 ≤m S 1 S 2 if and only if S 2 S 3 ≤m S 1 .

Lemma 10

If k 1 , k 2 , k 3 ∈ K are such that k 1 ⊖ k 2 and k 2 ⊕ k 3 are defined, then d K (k 3 , k 1 ⊖ k 2 ) = d K (k 2 ⊕ k 3 , k 1 ). Proof We can write k i = a, [x i , y i ] for some a ∈ Σ. Then d K (k 3 , k 1 ⊖ k 2 ) = max (x 1 -x 2 ) -x 3 , y 3 -(y 1 -y 2 ), 0 =                x 1 -x 2 -x 3 if x 1 -x 2 -x 3 ≥ 0, x 1 -x 2 -x 3 ≥ y 3 -y 1 + y 2 ; y 3 -y 1 + y 2 if y 3 -y 1 + y 2 ≥ 0, y 3 -y 1 + y 2 ≥ x 1 -x 2 -x 3 ; 0 if x 1 -x 2 -x 3 ≤ 0, y 3 -y 1 + y 2 ≤ 0.
Similarly,

d K (k 2 ⊕ k 3 , k 1 ) = max x 1 -(x 2 + x 3 ), (y 2 + y 3 ) -y 1 , 0 =                x 1 -x 2 -x 3 if x 1 -x 2 -x 3 ≥ 0, x 1 -x 2 -x 3 ≥ y 2 + y 3 -y 1 ; y 2 + y 3 -y 1 if y 2 + y 3 -y 1 ≥ 0, y 2 + y 3 -y 1 ≥ x 1 -x 2 -x 3 ; 0 if x 1 -x 2 -x 3 ≤ 0, y 2 + y 3 -y 1 ≤ 0. ⊓ ⊔
Theorem 7 (Soundness and maximality of quotient) Let S 1 , S 2 and S 3 be locally consistent WMTS such that S 2 is deterministic and S 1 S 2 is defined. If dm(S 3 , S 1 S 2 ) < ∞, then dm(S 3 , S 1 S 2 ) = dm(S 2 S 3 , S 1 ).

Proof To avoid confusion, we write and -→ for transitions in S 1 S 2 and and -→ for transitions in S 2 S 3 . The inequality dm(S 3 , S 1 S 2 ) ≥ dm(S 2 S 3 , S 1 ) is trivial if dm(S 2 S 3 , S 1 ) = ∞, so assume the opposite and let

R 1 = R 1 ε ⊆ S 3 × S 1 × S 2 ∪ {u} ε ≥ 0 be a witness for dm(S 3 , S 1 S 2 ). Define R 2 ε = (s 2 , s 3 ), s 1 s 3 , (s 1 , s 2 ) ∈ R 1 ε ⊆ S 2 × S 3 × S 1 for all ε ≥ 0, and let R 2 = {R 2 ε | ε ≥ 0}. Certainly (s 0 2 , s 0 3 ), s 0 1 ∈ R 2 dm(S3,S1 S2) ∈ R 2 , so let now (s 2 , s 3 ), s 1 ∈ R 2 ε ∈ R 2 for some ε ≥ 0.
Assume (s 2 , s 3 )

k 2 ⊕k 3
(t 2 , t 3 ), then also s 2 k 2 2 t 2 and s 3 k 3 3 t 3 . We have

s 3 , (s 1 , s 2 ) ∈ R 1 ε , so there is (s 1 , s 2 ) k 1 ⊖k ′ 2 (t 1 , t ′ 2 ) for which d K (k 3 , k 1 ⊖ k ′ 2 ) = d K (k ′ 2 ⊕ k 3 , k 1 ) ≤ ε and such that t 3 , (t 1 , t ′ 2 ) ∈ R 1 ε ′ ∈ R 1 , hence (t ′ 2 , t 3 ), t 1 ∈ R 2 ε ′ ∈ R 2 , for some ε ′ ≤ λ -1 ε -d K (k ′ 2 ⊕ k 3 , k 1 )
. By definition of quotient we must have s

1 k 1 1 t 1 and s 2 k ′ 2 2 t ′ 2 , and by determinism of S 2 , k ′ 2 = k 2 and t ′ 2 = t 2 . Assume s 1 k 1 -→ 1 t 1 . We must have a transition s 2 k 2 -→ 2 t 2 for which k 1 ⊖ k 2 is defined. Hence (s 1 , s 2 ) k 1 ⊖k 2 -→ (t 1 , t 2 ). This in turn implies that there is s 3 k 3 -→ 3 t 3 for which d K (k 3 , k 1 ⊖ k 2 ) = d K (k 2 ⊕ k 3 , k 1 ) ≤ ε and such that t 3 , (t 1 , t 2 ) ∈ R 1 ε ′ ∈ R 1 , hence (t 2 , t 3 ), t 1 ∈ R 2 ε ′ ∈ R 2 , for some ε ′ ≤ λ -1 ε -d K (k 2 ⊕ k 3 , k 1 )
, and by definition of parallel composition, (s 2 , s 3 )

k 2 ⊕k 3 -→ (t 2 , t 3 ). s1 t1 a, [0, 0] (a) S 1 s2 t2 a, [0, 1] (b) S 2 s3 t3 a, [0, 0] (c) S 3 (s2, s3) (t2, t3) a, [0, 1] (d) S 2 S 3 (s1, s2) (e) S 1 S 2 Fig. 11 WMTS for which dm(S 2 S 3 , S 1 ) = dm(S 3 , S 1 S 2 ) = ∞. To show that dm(S 3 , S 1 S 2 ) ≤ dm(S 2 S 3 , S 1 ), let R 2 = {R 2 ε ⊆ S 2 × S 3 × S 1 | ε ≥ 0} be a witness for dm(S 2 S 3 , S 1 ), define R 1 ε = s 3 , (s 1 , s 2 ) (s 2 , s 3 ), s 1 ∈ R 2 ε ∪ (s 3 , u) s 3 ∈ S 3 for all ε ≥ 0, and let R 1 = {R 1 ε | ε ≥ 0}, then s 0 3 , (s 0 1 , s 0 2 ) ∈ R 1 dm(S2 S3,S1) ∈ R 1 . For any (s 3 , u) ∈ R 1 ε for some ε ≥ 0,
d K (k 2 ⊕ k 3 , k 1 ) ≤ ε, implying that (s 1 , s 2 ) k 1 ⊖k 2 (t 1 , t 2 ). Hence d K (k 3 , k 1 ⊖ k 2 ) = d K (k 2 ⊕ k 3 , k 1 ) ≤ ε. Also, (t 2 , t 3 ), t 1 ∈ R 2 ε ′ ∈ R 2 , hence t 3 , (t 1 , t 2 ) ∈ R 1 ε ′ ∈ R 1 , for some ε ′ ≤ λ -1 ε -d K (k 3 , k 1 ⊖ k 2 ) . Assume (s 1 , s 2 ) k 1 ⊖k 2 -→ (t 1 , t 2 ), hence we have s 1 k 1 -→ 1 t 1 and s 2 k 2 -→ 2 t 2 . It follows that (s 2 , s 3 ) k ′ 2 ⊕k 3 -→ (t ′ 2 , t 3 ) with d K (k ′ 2 ⊕ k 3 , k 1 ) = d K (k 3 , k 1 ⊖ k ′ 2 ) ≤ ε and such that (t ′ 2 , t 3 ), t 1 ∈ R 2 ε ′ ∈ R 2 , hence t 3 , (t 1 , t ′ 2 ) ∈ R 1 ε ′ ∈ R 1 , for some ε ′ ≤ λ -1 ε-d K (k 3 , k 1 ⊖k ′ 2 )
. By definition of parallel composition we must have

s 2 k ′ 2 -→ 2 t ′ 2 and s 3 k 3 -→ 3 t 3 , and by determinism of S 2 , k ′ 2 = k 2 and t ′ 2 = t 2 . ⊓ ⊔
The example depicted in Figure 11 shows that the condition dm(S 3 , S 1 S 2 ) < ∞ in Theorem 7 is necessary. Here dm(S 2 S 3 , S 1 ) = 1, but dm(S 3 , S 1 S 2 ) = ∞ because of inconsistency between the transitions s 1 a,[0,0] 1 t 1 and s 2 a,[0,1] 2 t 2 for which k 1 ⊖k 2 is defined.

As a practical application, we notice that relaxation as defined in Section 5 can be useful when computing quotients. The quotient construction in Definition 12 introduces inconsistent states (which afterwards are pruned) whenever there is a must transition

s 1 k 1 -→ 1 s ′ 1 such that k 1 ⊖ k 2 is undefined for all transitions s 2 k 2 -→ 2 s ′ 2 .
Looking at the definition of ⊖, we see that this is the case if

k 1 = (a 1 , [x 1 , y 1 ]) and k 2 = (a 2 , [x 2 , y 2 ]) are such that a 1 = a 2 or x 1 -x 2 > y 1 -y 2 .
In the first case, the inconsistency is of a structural nature and cannot be dealt with; but in the second case, it may be avoided by enlarging k 1 : decreasing x 1 or increasing y 1 so that now,

x 1 -x 2 ≤ y 1 -y 2 .
Enlarging quantitative constraints is exactly the intuition of relaxation, thus in practical cases where we get a quotient S 1 S 2 which is "too inconsistent", we may be able to solve this problem by constructing a suitable ε-relaxation S ′ 1 of S 1 . Theorems 6 and 7 can then be used to ensure that also S ′ 1 S 2 is a relaxation of S 1 S 2 .

Logical Characterizations

We now turn our attention to showing 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], by abandoning the usual Boolean interpretation of logical satisfaction, as we did for refinement, and instead interpreting each formula as a map assigning to states a real-valued number denoting the relationship between the property and the state. The logic L is the smallest set of expressions generated by the following abstract syntax:

φ, φ 1 , φ 2 := tt | ff | ℓ φ | [ℓ]φ | φ 1 ∧ φ 2 | φ 1 ∨ φ 2 (ℓ ∈ K)
As usual, when ℓ = (a, [x With this standard (informal) interpretation of logical specifications, implementations which come close to matching the specification are rejected just as much as the truly wrong implementations. Analog to our refinement distance, a quantitative interpretation provides us with continuous judgments on the relationship between a specification S or implementation I and a logical specification φ. Defining the semantics of formulae as a map from states to reals, the value of any φ for the initial state of implementations determines an order on the applicability of the implementations for the given specification. The semantics of a formula φ ∈ L is a mapping φ : S → | ≥0 ∪ {∞} given inductively, again relative to the discounting factor λ with 0 < λ < 1, as follows:

tt s = 0 ff s = ∞ (φ 1 ∧ φ 2 ) s = max( φ 1 s, φ 2 s) (φ 1 ∨ φ 2 ) s = min( φ 1 s, φ 2 s) ℓ φ s = inf{d K (k, ℓ) + λ φ t) | s k -→ t, d K (k, ℓ) = ∞} [ℓ]φ s = sup{d K (k, ℓ) + λ φ t | s k t, d K (k, ℓ) = ∞}
Intuitively, [ℓ]φ s takes the value of the supremum over all outgoing s a,x t transitions and the respective match with x ∈ [x 1 , x 2 ] plus the discounted value of the property φ for t. Clearly if [ℓ]φ s = 0 then every s a,x t satisfies the property exactly, recovering the standard interpretation. Notice that by evaluating a logical specification φ for a WMTS specification S, we get a measure on the set of implementations of S which are not shared by the specification φ. The value is 0 if and only if there is a thorough refinement from S to φ, i.e. if and only if any implementation of S satisfies φ.

For a SMTS S we write φ S = φ s 0 . The first theorem below expresses 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. Note the special case that S ≤m T implies φ S ≤ φ T .

Theorem 8 For all φ ∈ L and WMTS S, T , φ S ≤ φ T + dm(S, T ).

Proof By standard structural induction in φ. The claim obviously holds for φ = tt and φ = ff .

For φ = φ 1 ∧ φ 2 , the induction hypothesis that φ i s 1 ≤ φ i s 2 + dm(s 1 , s 2 ) for i = 1, 2 implies that also max( φ 1 s 1 , φ 2 s 1 ) ≤ max( φ 1 s 2 , φ 2 s 2 ) + dm(s 1 , s 2 ). Similarly for φ = φ 1 ∨ φ 2 .

For the case φ = ℓ φ ′ , if The next theorem shows that the disjunction-free fragment of L is also 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 common assumption in this context, cf. [START_REF] Kim | Modal specifications[END_REF][START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF].

Theorem 9 For all disjunction-free φ ∈ L and locally consistent and compactly branching WMTS S, we have φ S = sup I∈ S φ I.

Proof Since dm(I, S) = 0 for all I ∈ S , Theorem 8 entails φ 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 0, 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 For the case φ = ℓ φ ′ , we are done if φ S = 0. Otherwise, to conclude that sup I∈ S ℓ φ ′ I ≥ ℓ φ ′ S we expose an I ∈ S for which α < φ I for any α < φ S. For a fixed α < φ S, start by letting I = {i 0 } and -→ I = ∅. Now for each transition s 0 k -→ S t we have α < d K (k, ℓ) + λ φ ′ t, so (assuming for the moment that φ ′ t = 0) by the density of the reals, there is a number α ′ k < φ ′ t for which α < d K (k, ℓ) + λα ′ k . By induction hypothesis, the sub-formula φ ′ satisfies sup J∈ S ′ φ ′ J = φ ′ S ′ for any S ′ , specifically when S ′ = (t, S) is taken as S with initial state replaced by t. Therefore, and as α ′ k < φ ′ t, there exists a J ∈ (t, S) with α ′ k < φ ′ J. Now let n ∈ Imp with n ⊑ k be such that d K (n, ℓ) + λ φ ′ J = d K (k, ℓ) + λ φ ′ J, and add J together with a transition i 0 n -→ I j 0 to I.

In case φ ′ t = 0, we have J ∈ t, S with φ ′ J = 0, and we can add J together with a transition i 0 n -→ I j 0 to I as above. For the so-constructed implementation I we have

φ I = inf{d K (m, ℓ) + λ φ ′ j | i 0 m -→ I j} = inf{d K (k, ℓ) + λ φ ′ J | s 0 k -→ S t, J ∈ t, S , φ ′ t = ∞ or α ′ k < φ ′ J} > inf({d K (k, ℓ) + λα ′ k | s 0 k -→ S t} ∪ {d K (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. If d K (k, ℓ) + λ φ ′ t = ∞ for all s 0 k S t, then φ S = sup ∅ = 0 and we are done. Otherwise let s 0 k S t be such that φ S = d K (k, ℓ) + λ φ ′ t, which exists because S is compactly branching. Then α < d K (k, ℓ) + λ φ ′ t, so (assuming that φ ′ t = 0) we have α ′ k < φ ′ t with d K (k, ℓ) + λα ′ k > α.

Let J ∈ t, S such that α ′ k < φ ′ J, let n ∈ Imp with n ⊑ k be such that d K (n, ℓ)+λ φ ′ J = d K (k, ℓ)+λ φ ′ J, and add J together with a transition i 0 n -→ I j 0 to I. Then

φ I = sup{d K (m, ℓ) + λ φ ′ n | i 0 m -→ I j} ≥ d K (n, ℓ) + λ φ ′ J = d K (k, ℓ) + λ φ ′ J ≥ F (k, ℓ, α ′ k ) > α.
In case φ ′ t = 0 instead, we again take some J ∈ t, S , and then φ I ≥ d K (k, ℓ) + λ φ ′ t > α. ⊓ ⊔ Other notions of completeness (see e.g. [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]) are subject of future work.

Conclusion and Further Work

We have shown in this paper that within the quantitative specification framework of weighted modal transition systems, refinement and implementation distances provide a useful tool for robust compositional reasoning. Note that these distances permit us not only to reason about differences between implementations and from implementations to specifications, but they also provide a means by which we can compare specifications directly at the abstract level.

We have shown that for some of the ingredients of our specification theory, namely structural composition and quotient, our formalism is a conservative extension of the standard Boolean notions. We have also noted however, that for determinization and logical conjunction, the properties of the Boolean notions are not preserved, and that this is a fundamental limitation of any reasonable quantitative specification theory. The precise practical implications of this for the applicability of our quantitative specification framework, and perhaps how to circumvent these limitations, are subject to future work.

Fig. 4

 4 Fig.[START_REF] Antonik | 20 years of modal and mixed specifications[END_REF] Four implementations of the simple email system in Figure3.

Fig. 5

 5 Fig. 5 Weighted modal transition system modeling a simple wiper control component of a car.

Fig. 6 Definition 4

 64 Fig. 6 Two weighted transition systems with branching distance d(I 1 , I 2 ) = 18.

  S 2 is deterministic, then d t (S 1 , S 2 ) = dm(S 1 , S 2 ). Proof If d t (S 1 , S 2 ) = ∞,we are done by Theorem 1. Otherwise, let R = {Rε | ε ≥ 0} be the smallest relation family for which -(s 0 1 , s 0

( 4 . 1 )

 41 D(S) is deterministic for any WMTS S, (4.2) S ≤m D(S) for any WMTS S, (4.3) S ≤ ε m D implies D(S) ≤ ε m D for any WMTS S, any deterministic WMTS D, and any ε ≥ 0. Proof There is a determinization operator D ′ on WMTS which satisfies Properties (4.1) and (4.2) above and a weaker version of Property (4.3) with ε = 0: (4.3 ′ ) S ≤m D implies D ′ (S) ≤m D for any WMTS S and any deterministic WMTS D.

DFig. 9

 9 Fig. 9 Counter-example for Theorem 4: dm D ′ (S), D = 3+3λ and dm(S, D) = max(3, 3λ) = 3, hence dm D ′ (S), D ≤ dm(S, D).

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

  and in the second case, we have s 2 k 2 -→ 2 t 2 , hence also s 2 k 2 2 t 2 , with the same property.

	For a transition s 2	k 2

  a,I 1 1 t 1 . Let x ∈ I 1 , then there is an implementation (p, P x ) ∈ (s 1 , S 1 ) with a transition p Now d t (p, P x ), (s 2 , S 2 ) ≤ ε, hence we have a transition s 2 K (a, x), (a, I x 2 ) ≤ ε. Also for any other x ′ ∈ I 1 we have a transition s 2 with d K (a, x ′ ), (a, I x ′ 2 ) ≤ ε, hence by determinism of S 2 , I x 2 = I x ′ 2 and t x 2 = t x ′ 2 . It follows that there is a unique transition 2 a,I 2 t 2 , and as d K (a, x), (a, I 2 ) ≤ ε for all x ∈ I 1 , we have d K (a, I 1 ), (a, I 2 ) ≤ ε, and (t 1 , t 2 ) ∈ R λ -1 (ε-dK((a,I1),(a,I2))) by definition. -→ 2 t 2 . Let (p 1 , P 1 ) ∈ (s 1 , S 1 ) , then we have (p 2 , P 2 ) ∈ (s 2 , S 2 ) with d (p 1 , P 1 ), (p 2 , P 2 ) ≤ ε. Now any (p 2 , P 2 ) ∈ (s 2 , S 2 ) has p 2

		a,I x 2 2 t x 2 with d a,I x ′ 2 2 t x ′
	Now assume s 2	a,I 2

m -→ q. 2 a,x 2

Definition 9

  Given δ ∈ ◆, the δ-widening of a WMTS S is the WMTS S +δ with transitions s a,I±δ t in S +δ for all s a,I t in S, and s

	a,I±δ -→ t in S +δ for all s	a,I -→ t in

S.

  any transition s 3 k 3 3 t 3 can be matched by u k 3 u, and then (t 3 , u) ∈ R 1 0 . Let now s 3 , (s 1 , s 2 ) ∈ R 1 ε for some ε ≥ 0, and assume s 3 k 3 3 t 3 . If k 2 ⊕ k 3 is undefined for all transitions s 2 k 2 2 t 2 , then by definition (s 1 , s 2 ) k 3 u, and again (t 3 , u) ∈ R 1 0 . If there is a transition s 2 k 2 2 t 2 such that k 2 ⊕k 3 is defined, then also (s 2 , s 3 ) k 2 ⊕k 3 (t 2 , t 3 ). Hence we have s 1

k 1 1 t 1 with

  1 , x 2 ]), writing ℓ φ means that we insist on implementations exhibiting a transition which reaches a state having property φ and is labeled by a and an integer x for which x 1 ≤ x ≤ x 2 . Dually, [ℓ]φ restricts the set of implementations to those where every transition labeled with a and an integer in [x 1 , x 2 ] reaches a state with property φ.

  dm(s 1 , s 2 ) = ∞ or if there are no transitions s 2 -→ the claim is trivial. Let thuss 2 k 2 -→ t 2 , then there exist s 1 k 1 -→ t 1 with d K (k 1 , k 2 ) + λdm(t 1 , t 2 ) ≤ dm(s 1 , s 2 ) (by definition of dm). Then d K (k 1 , ℓ) + λ φ ′ t 1 ≤ (d K (k 1 , k 2 ) + λdm(t 1 , t 2 )) + (d K (k 2 , ℓ) + λ φ ′ t 2) by induction hypothesis and the triangle inequalityfor d K , hence d K (k 1 , ℓ) + λ φ ′ t 1 ≤ dm(s 1 , s 2 )+d K (k 2 , ℓ)+λ φ ′ t 2 . As s 2 k 2 -→ t 2 was arbitrary, this entails inf{d K (k 1 , ℓ)+ λ φ ′ t 1 | s 1 k 1 -→ t 1 } ≤ inf{d K (k 2 , ℓ) + λ φ ′ t 2 | s 1 k 2 -→ t 2 } + dm(s 1 , s 2 ), which was to be shown.For the case of φ = [ℓ]φ ′ the proof is similar: We have nothing to prove if dm(s 1 , s 2 ) = ∞ or if there are no transitions s 1k 1 t 1 with d K (k 1 , ℓ) = ∞,so assume there is such a transition. Then we also have s 2k 2 t 2 with (d K (k 1 , k 2 ) + λdm(t 1 , t 2 )) ≤ dm(s 1 , s 2 ), and d K (k 1 , ℓ) + λ φ ′ t 1 ≤ (d K (k 1 , k 2 ) + λdm(t 1 , t 2 )) + d K (k 2 , ℓ) + λ φ ′ t 2 ≤ dm(s 1 , s 2 ) + d K (k 2 , ℓ) + λ φ ′ t 2 . ⊓ ⊔