Axel Legay

Louis-Marie Traonouez

PYECDAR: Towards Open Source Implementation for Timed Systems

PYECDAR is an open source implementation for reasoning on timed systems. PYECDAR's main objective is not efficiency, but rather flexibility to test and implement new results on timed systems.

Context

To solve complex problems such as scheduling tasks in embedded applications, the ability to reason on real time is mandatory. It is thus not a surprise that, over the last twenty years, the rigorous design of real-time systems has become a main research topic. Among major successes in the area, one finds the UPPAAL toolset [START_REF] Behrmann | Developing uppaal over 15 years[END_REF] that is promoted by industries, and that has been used to verify complex properties of complex protocols such as the Herschel-Planck, the root contention protocol, or Audio-Control Protocol developed by Philips. Recently, timed tools have been extended to reason not only on the properties of the system, but also on the effects of its interactions with a potentially unknown environment. Tools such as UPPAAL-TIGA do this via game-theory [START_REF] Behrmann | Uppaal-tiga: Time for playing games! In: CAV[END_REF]. The code of UPPAAL and related toolsets is not available and their interfaces are fixed in stone. Those choices shall not been seen as drawbacks, but rather as strategic choices for an industrial dissemination. However, from a scientific point of view, this makes it hard for researchers to reuse part of those toolsets to quickly implement and evaluate their new results without sharing them with tool makers.

We present PYECDAR (https://project.inria.fr/pyecdar/) that is a new python implementation of well-known results on timed systems and games. We then show that the tool can be used to implement new results in timed systems. Our main objective with PYECDAR is to offer an open source platform to quickly test new results on timed systems. Of course, this implementation is not as competitive as well-established toolsets, but it is very flexibility and easy to use and extend.

The PYECDAR Toolset in a Nutshell

As a foundation to develop new algorithms, PYECDAR offers an implementation of the reachability analysis for timed automata as well as an implementation of the forward algorithm from [START_REF] Behrmann | Uppaal-tiga: Time for playing games! In: CAV[END_REF] that is used to solve reachability problem for timed games. Then, the tool offers the implementation of a series of brand new results on timed systems. The first is the timed specification theory from [START_REF] David | Timed i/o automata: a complete specification theory for real-time systems[END_REF] that has been developed to reason on complex systems described as a combination of components. The specifications of those components are given by Timed Input/Output Automata (TIOA), where inputs represent behaviors of the environment, and outputs those of the system. The tool is able to 1. decide whether an implementation (e.g. Fig. 1b) conforms to a given specification (e.g. Fig. 1a), decide whether a specification can be implemented (consistency), 3. compare specifications (refinement -timed game), 4. logically/structurally compose two specifications, 5. synthesize a specification from a set of requirements (quotient), and 6. prune states from which the environment has no strategy to avoid bad behaviors (compatibility) -the operation requires the implementation of a timed game. The theory has also been implemented in ECDAR [START_REF] David | Ecdar: An environment for compositional design and analysis of real time systems[END_REF]. An advantage of PYECDAR is that its internal data structures can be used to save (and reuse) the result of composing/synthesizing specifications, while the one of ECDAR cannot. Also, PYECDAR can perform compatibility on combined systems while ECDAR cannot.

PYECDAR also offers the implementation of an extension of [START_REF] Chatterjee | Synthesis of memory-efficient "real-time" controllers for safety objectives[END_REF] to decide whether an implementation automaton is robust: i.e. if it remains conform to a specification when its output guards (resp. input) are exceeded (resp. restricted) by some ∆ value. The tool can also synthesize the maximal ∆ for which the implementation remains robust. The results extend to all the operations of the theory [START_REF] Larsen | Robust specification of real time components[END_REF]. As an example, implementation of Fig. 1b is robust with respect to specification of Fig. 1a up to ∆ = 1. Beyond that point, the perturbations of the output transitions, which is 5 -∆ ≤ y ≤ 5 + ∆, exceeds the guard y ≥ 4 and the invariant y ≤ 6 of the specification. It is worth mentioning that the internal structure of ECDAR does not permit to implement robustness on top of the specification theory. So, albeit the work in [START_REF] Larsen | Robust specification of real time components[END_REF] is an extension of the one in [START_REF] David | Timed i/o automata: a complete specification theory for real-time systems[END_REF], using ECDAR would require an entirely new implementation. Several robustness theories for timed automata have been implemented in tools such as shrinktech [START_REF] Bouyer | Robust reachability in timed automata: A game-based approach[END_REF], but PYECDAR is the first to offer this feature for a complete specification theory.

Finally, PYECDAR offers the ability to reason on variability [START_REF] Cordy | A framework for the rigorous design of highly adaptive timed systems[END_REF]. There, the model is an extended timed automata that permits to represent features of both the system and its environment -such features may appear or disappear at runtime. As an example, Fig. 1c represents a specification of the system using two adaptive features for the environment (out_of_tea and out_of_cof). These features may be enabled or disabled at runtime during input transitions, which may restrict the possible behaviors of the system. PYECDAR exploits an extension of timed game algorithms to synthesize e.g., the minimal set of features that are needed by a system so that it verifies a timed CTL property, whatever the environment does. To the best of our knowledge, PYECDAR is the first to offer a timed implementation of such a complex problem in software engineering.

3 Architecture of the Tool PYECDAR works inside an interactive python shell, and offers a set of modules and fonctions to load models and perform computations. In PYECDAR, models are written by using the interface of UPPAAL or ECDAR, and uploaded via an XML file. Once the models have been loaded, the user can perform one or several queries via the shell in an on-demand manner.

Input Language. PYECDAR supports the main language elements from ECDAR. That allows to design TIOAs with the syntax from [START_REF] David | Timed i/o automata: a complete specification theory for real-time systems[END_REF], and additionaly to use extended syntax elements, like constants and integer variables. See https://project.inria.fr/pyecdar/ for the grammar. TIOAs are specified with the ECDAR interface that is freely available, and then saved in XML. In case of features, Boolean variables are added to the model to witness the presence or absence of each feature. For the internal representation, PYECDAR relies on the UPPAAL DBMs library used to represent the timing constraints of the model and a classical graph-based structure to represent its syntax. Contrary to ECDAR, PYECDAR creates a dedicated structure for each component, including those that are obtained by combining existing ones. ECDAR is rigid and can only represent a new component by a pointer on states of the structures of those that participated to its creation. As a consequence, ECDAR cannot perform composability that consists in removing "bad states". Indeed, since new components do not have their own structure, this operation would eventually remove states of individual components that participated to its creation and hence falsify the design. If features are present, then PYECDAR combines BDDs used to logically represent sets of features on transitions with DBMs (see [START_REF] Cordy | A framework for the rigorous design of highly adaptive timed systems[END_REF] for details). Finally, PYECDAR also uses polyhedra, with bindings to the Parma Polyhedra Library, to encode parametric constraints in case the user wants to solve a robustness problem.

Queries. PYECDAR offers two types of queries. The first one comes as a set of operators such as composition or quotient to build complex systems from small ones. The second type concerns operational queries such as the one of checking consistency, refinement, robustness, or properties of adaptive systems (see https://project.inria.fr/pyecdar/ for the complete list of queries). Depending on the problem to be solved, PYECDAR outputs different kinds of results. As an example, if the tool is used to synthesize the set of features that allows to satisfy some temporal formula, this set is output as a binary expression. The tool can also be used to determine the winning states for a timed game, which allows to determine if the consistency, compatibility or refinement problems have been solved. Finally, using a counter-example refinement approach (CEGAR), it can compute the maximum perturbation allowed by the system to solve a robustness problem. PYECDAR offers some extra features such as saving TIOAs into a new XML file so that they can be reused in other designs.

Algorithms. 1. PYECDAR implements the on-the-fly safety game algorithm from [START_REF] Behrmann | Uppaal-tiga: Time for playing games! In: CAV[END_REF] that is used e.g. to check consistency and refinement. The tool also uses a model transformation to reduce robust consistency/compatibility to consistency/compatibility and hence reuse the former algorithm. 2. The CEGAR algorithm is a parametric extension of the first [START_REF] Traonouez | A parametric counterexample refinement approach for robust timed specifications[END_REF] that allows to compute the maximal delta for which an implementation

Fig. 1 :

 1 Fig. 1: Specifications of timed systems

remains robust. 3. The last algorithms are backward propagation game algorithms [START_REF] Cordy | A framework for the rigorous design of highly adaptive timed systems[END_REF] that compute the set of features that satisfies a formula for an adaptive system.

PYECDAR in Action

We quickly demonstrate how to use PYECDAR. Assume that the models presented in Fig. 1 are saved in an XML file machine.xml. We first load the XML file of the first two TIOAs:

In [START_REF] Behrmann | Developing uppaal over 15 years[END_REF]: W = pyecdar.loadModel("machine.xml") In [START_REF] Behrmann | Uppaal-tiga: Time for playing games! In: CAV[END_REF]: MS = W.getSpecification("MachineSpec") In [START_REF] David | Timed i/o automata: a complete specification theory for real-time systems[END_REF]: MI = W.getSpecification("MachineImpl")

We check if the implementation of Fig. 1b satisfies the specification in Fig. 1a:

We can then compute the maximum perturbation allowed by the implementation. This applies the CEGAR approach, starting with value 5, and with a confidence 0.1 for the result. The result is computed after 2 iterations and ∆ = 1 is returned. Other examples, e.g. checking a temporal formula on the adaptive specification of Fig. 1c, are described on https://project.inria.fr/pyecdar/


Uli Fahrenberg

Jan Křetínský

Axel Legay

Louis-Marie Traonouez

Compositionality for Quantitative Specifications

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

Introduction

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

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

A simple example of a vending machine specification, in Fig. 1 on the left, describes that any correct implementation must be ready to accept money, then may offer the customer to choose extras and must issue a beverage. While the must-transitions are preserved in the refinement process, the may-transitions can be either implemented and turned into must-transitions, or dropped. This low-level refinement process is, however, insufficient when the designer wants to get more specific about the implemented actions, such as going from the coarse specification just described to the more fine-grained specification on the right of Fig. 1. In order to relate such specifications, MTS with structured labels were introduced [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]. Given a preorder on labels, relating for instance coffee beverage, we can refine a transition label into one which is below, for example implement "beverage" with its refinement "coffee". Then t will be a refinement of s. This framework can be applied to various preorders. For example, one can use labels with a discrete component carrying the action information and an interval component to model time durations or energy consumption. As an example, consider the simple real-time property to the right: "after a req(uest), grant has to be executed within 5 time units without the process being idle meanwhile". The transition (grant, [0,[START_REF] Bauer | Extending modal transition systems with structured labels[END_REF]) could be safely refined to (grant, [l, r]) for any 0 ≤ l ≤ r ≤ 5.

However, here we identify several shortcomings of the current approaches:

Expressive power. The current theory of structured labels is available only for the basic MTS. Very often one needs to use richer structures such as disjunctive MTS (DMTS) [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF][START_REF] Larsen | Equation solving using modal transition systems[END_REF] or acceptance automata [START_REF] Hennessy | Acceptance trees[END_REF][START_REF] Raclet | Residual for component specifications[END_REF]. While MTS generally cannot express disjunction of properties, DMTS can express any Boolean combinations of properties. This allows, for instance, to prohibit deadlocks as in the example to the left in Fig. 2. The disjunctive must, depicted as a branching arrow, requires at least one of the transitions to be present. Thus we allow the deadline for grant to be reset as long as additional work is generated. Note that specifying grant and work as two separate must-transitions would not allow postponing the deadline; and two separate may-transitions would not guarantee any progress, as none of them has to be implemented.

The additional expressive power of DMTS is also justified by the fact that DMTS are equivalent to the modal ν-calculus [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. We hence propose DMTS with structured labels and also extend the equivalence between DMTS and the ν-calculus to our setting. Fig. 2 (right) shows a ν-calculus translation of the DMTS on its left.

Robustness. Consider again the request-grant example x in Fig. 2, together with the two labeled transition systems in Fig. 3 (left). While i 1 , issuing grant after precisely 5 time units, is a valid implementation of x, if there is but a small positive drift in the timing, like in i 2 , it is not an implementation anymore. However, this drift might be easily mended or just might be due to measuring errors. Therefore, when models and specifications contain such quantitative information, the standard Boolean notions of satisfaction and refinement are of limited utility [START_REF] Henzinger | The embedded systems design challenge[END_REF] and should be replaced by notions more robust to perturbations. For another example, the DMTS to the right of Fig. 3 is not a refinement of the second one in Fig. 2, but for all practical purposes, it is very close.

One approach to robustness is to employ metric distances instead of Boolean relations; this has been done for example in [START_REF] De Alfaro | Model checking discounted temporal properties[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF][START_REF] Desharnais | Metrics for labelled Markov processes[END_REF][START_REF] Henzinger | Quantifying similarities between timed systems[END_REF][START_REF] Romero-Hernández | Defining distances for all process semantics[END_REF][START_REF] Van Breugel | A behavioural pseudometric for probabilistic transition systems[END_REF][START_REF] Černý | Simulation distances[END_REF] and many other papers. An advantage of behavioral specification formalisms is that models and specifications are closely related, hence distances between models can easily be extended to distances between specifications. We have developed a distancebased approach for MTS in [START_REF] Bauer | Weighted modal transition systems[END_REF][START_REF] Bauer | General quantitative specification theories with modalities[END_REF] and shown in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Fahrenberg | The quantitative linear-timebranching-time spectrum[END_REF] that a good general setting is given by recursively specified trace distances on an abstract quantale. Here we extend this to DMTS.

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

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

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

Further related work. Refinement of components is a frequently used design approach in various areas, ranging from subtyping [START_REF] Liskov | A behavioral notion of subtyping[END_REF] over the Java modeling language JML [START_REF] Jacobs | A logic for the Java modeling language JML[END_REF] or correct-by-design class diagrams operations [START_REF] Fahrenberg | Sound merging and differencing for class diagrams[END_REF] to interface theories close to MTS such as interface automata [START_REF] Alfaro | Interface automata[END_REF] based on alternating simulation. A variant of alternating simulation called covariant-contravariant simulation has been compared to MTS modal refinement in [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF]. The graphical representability of these variants was studied in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Boudol | Graphical versus logical specifications[END_REF]. Quantities have been introduced also to the modal mu-calculus. At first, the focus lied on probabilities [START_REF] Huth | Quantitative analysis and model checking[END_REF][START_REF] Mio | Probabilistic modal mu-calculus with independent product[END_REF][START_REF] Morgan | A probabilistic temporal calculus based on expectations[END_REF], but later predicates with values in arbitrary metric spaces were also introduced [START_REF] De Alfaro | Linear and branching system metrics[END_REF]. However, no refinement has been considered.

Structured Labels

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

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

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

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

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

Γ = U × {[x, x] | x ∈ Ê} ≈ U × Ê.
For a quite general setting, we can instead start with an arbitrary set Γ of implementation labels, let Σ = 2 Γ , the powerset, and = ⊆ be subset inclusion.

Then a = a for all a ∈ Σ. (Hence we identify implementation labels with oneelement subsets of Σ.) ⊓ ⊔

Label operations

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

In order to provide them for DMTS, we first need the respective atomic operations on their action labels. We hence assume that Σ comes equipped with a partial conjunction, i.e., an operator : Σ × Σ ⇀ Σ for which it holds that (1) if a 1 a 2 is defined, then a 1 a 2 a 1 and a 1 a 2 a 2 , and (2) if a 3 a 1 and a 3 a 2 , then a 1 a 2 is defined and a 3 a 1 a 2 .

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

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

a 1 a 2 = a 1 if a 1 = a 2 , undef. otherwise .
For labels in U × {[l, r] | l, r ∈ Ê, l ≤ r}, the unique conjunction is

(u 1 , [l 1 , r 1 ]) (u 2 , [l 2 , r 2 ]) = undef. if u 1 = u 2 or [l 1 , r 1 ] ∩ [l 2 , r 2 ] = ∅ , (u 1 , [l 1 , r 1 ] ∩ [l 2 , r 2 ])
otherwise .

Finally, for the case of specification labels as sets of implementation labels, the unique conjunction is a 1 a 2 = a 1 ∩ a 2 .

⊓ ⊔

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

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

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

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

(u 1 , [l 1 , r 1 ]) max (u 2 , [l 2 , r 2 ]) = undef. if u 1 = u 2 , (u 1 , [max(l 1 , l 2 ), max(r 1 , r 2 )])
otherwise .

Here we wait for the slower action. This models a blocking synchronization where both synchronized actions have to be performed before we can continue. Yet another operator uses interval intersection instead, i.e., ∩ = ; this is useful if the intervals model deadlines.

For set-valued specification labels, we may take any synchronization operator given on implementation labels Γ and lift it to one on Σ by a

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

Specification Formalisms

In this section we introduce the specification formalisms which we use in the rest of the paper. The universe of models for our specifications is the one of standard labeled transition systems. For simplicity of exposition, we work only with finite specifications and implementations, but most of our results extend to the infinite (but finitely branching) case. A labeled transition system (LTS) is a structure I = (S, s 0 , -→) consisting of a finite set S of states, an initial state s 0 ∈ S, and a transition relation -→ ⊆ S × Γ × S. We usually write s a -→ t instead of (s, a, t) ∈ -→. Note that transitions are labeled with implementation labels.

Disjunctive Modal Transition Systems

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

Note that we allow multiple (or zero) initial states. We write s a t instead of (s, a, t) ∈ and s -→ N instead of (s,

N ) ∈ -→. A DMTS (S, S 0 , , -→) is an implementation if ⊆ S × Γ × S, -→ = {(s, {(a, t)}) | s
a t}, and S 0 = {s 0 } is a singleton; DMTS implementations are hence isomorphic to LTS. DMTS were introduced in [START_REF] Larsen | Equation solving using modal transition systems[END_REF] in the context of equation solving, or quotient of specifications by processes. They are a natural extension of modal transition systems [START_REF] Larsen | A modal process logic[END_REF], which are DMTS in which all disjunctive must-transitions s -→ N lead to singletons N = {(a, t)}; in fact, DMTS are the closure of MTS under quotient [START_REF] Larsen | Equation solving using modal transition systems[END_REF].

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

Definition 4. Let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ) be DMTS. A relation R ⊆ S 1 × S 2 is a modal refinement if it holds for all (s 1 , s 2 ) ∈ R that -for all s 1 a1 1 t 1 there is s 2 a2 2 t 2 such that a 1 a 2 and (t 1 , t 2 ) ∈ R, and -for all s 2 -→ 2 N 2 there is s 1 -→ 1 N 1 such that for all (a 1 , t 1 ) ∈ N 1 there is (a 2 , t 2 ) ∈ N 2 with a 1 a 2 and (t 1 , t 2 ) ∈ R. D 1 refines D 2 , denoted D 1 ≤ m D 2 ,
if there exists a modal refinement R for which it holds that for every s 0

1 ∈ S 0 1 there is s 0 2 ∈ S 0 2 for which (s 0 1 , s 0 2 ) ∈ R. We write D 1 ≡ m D 2 if D 1 ≤ m D 2 and D 2 ≤ m D 1 . The implementation semantics of a DMTS D is D = {I ≤ m D | I implementation}. We say that D 1 thoroughly refines D 2 , and write D 1 ≤ th D 2 , if D 1 ⊆ D 2 .
The below proposition, which follows directly from transitivity of modal refinement, shows that modal refinement is sound with respect to thorough refinement; in the context of specification theories, this is what one would expect.

Proposition 5. For all DMTS D 1 , D 2 , D 1 ≤ m D 2 implies D 1 ≤ th D 2 .
⊓ ⊔

Acceptance automata

A (non-deterministic) acceptance automaton (AA) is a structure A = (S, S 0 , Tran), with S ⊇ S 0 finite sets of states and initial states and Tran : S → 2 2 Σ×S an assignment of transition constraints. The intuition is that a transition constraint Tran(s) = {M 1 , . . . , M n } specifies a disjunction of n choices M 1 , . . . , M n as to which transitions from s have to be implemented. An AA is an implementation if S 0 = {s 0 } is a singleton and it holds for all s ∈ S that Tran(s) = {M } ⊆ 2 Γ ×S is a singleton; hence AA implementations are isomorphic to LTS. Acceptance automata were first introduced in [START_REF] Raclet | Residual for component specifications[END_REF], based on the notion of acceptance trees in [START_REF] Hennessy | Acceptance trees[END_REF]; however, there they are restricted to be deterministic. We employ no such restriction here.

Let

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

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

) = {M ⊆ Σ × S | ∀(a, t) ∈ M : s a t, ∀s -→ N : N ∩ M = ∅} and define the AA da(D) = (S, S 0 , Tran).
For an AA A = (S, S 0 , Tran), define the DMTS ad(A) = (D, D 0 , , -→) by

D = {M ∈ Tran(s) | s ∈ S}, D 0 = {M 0 ∈ Tran(s 0 ) | s 0 ∈ S 0 }, -→ = M, {(a, M ′ ) | M ′ ∈ Tran(t)} (a, t) ∈ M , = {(M, a, M ′ ) | ∃M -→ N : (a, M ′ ) ∈ N }.
Similarly to a theorem of [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF], we can now show the following:

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

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

The Modal ν-Calculus

In [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF], translations were discovered between DMTS and the modal ν-calculus, and refining the translations in [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF], we could show that for discrete labels, these formalisms are structurally equivalent. We use the representation of the modal ν-calculus by equation systems in Hennessy-Milner logic developed in [START_REF] Larsen | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF]. For a finite set X of variables, let H(X) be the set of Hennessy-Milner formulae, generated by the abstract syntax H(X) ∋ φ ::

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

i∈I σ i (x) = i∈I σ i (x).
The semantics of a formula in H(X) is a function from assignments to subsets of S defined as follows: tt σ = S, ff σ = ∅, x σ = σ(x), φ∧ψ σ = φ σ∩ ψ σ, φ ∨ ψ σ = φ σ ∪ ψ σ, and

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

An LTS I = (S, s 0 , -→) implements (or models) the expression N , denoted

I |= N , if there is x 0 ∈ X 0 such that s 0 ∈ ∆ (x 0 ).
In [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF] we have introduced another semantics for ν-calculus expressions, which is given by a notion of refinement, like for DMTS and AA. For this we need a normal form for ν-calculus expressions:

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

⊓ ⊔

As this is a type of conjunctive normal form, it is clear that translating a ν-calculus expression into normal form may incur an exponential blow-up. We introduce some notation for ν-calculus expressions in normal form. Let N = (X, X 0 , ∆) be such an expression and x ∈ X, with ∆(x) = i∈I j∈Ji a ij x ij ∧ a∈Σ [a] j∈Ja y a,j as in the lemma. Define ♦(x) = {{(a ij , x ij ) | j ∈ J i } | i ∈ I} and, for each a ∈ Σ, a (x) = {y a,j | j ∈ J a }. Intuitively, ♦(x) collects all arequirements from x, whereas a (x) specifies the disjunction of [a]-properties which must hold from x. Note that now,

∆(x) = N ∈♦(x) (a,y)∈N a y ∧ a∈Σ [a] y∈ a (x)
y .

(

) 2
Let

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

We say that a ν-calculus expression (X,

X 0 , ∆) in normal form is an imple- mentation if X 0 = {x 0 } is a singleton, ♦(x) = {{(a, y)} | y ∈ a (x), a ∈ Σ} and a (x) = ∅ for all a / ∈ Γ , for all x ∈ X. We can translate a LTS (S, S 0 , -→) to a ν-calculus expression (S, S 0 , ∆) in normal form by setting ♦(s) = {{(a, t)} | s a -→ t} and a (s) = {t | s a -→ t} for all s ∈ S, a ∈ Σ.
This defines a bijection between LTS and ν-calculus implementations, hence, like for DMTS and AA, an embedding of LTS into ν-calculus. One of the main results of [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF] is that for discrete labels, the refinement semantics and the fixed point semantics of the modal ν-calculus agree; the proof can easily be extended to our case of structured labels: Theorem 8. For any LTS I and any ν-calculus expression N in normal form,

I |= N iff I ≤ m N . ⊓ ⊔
For a DMTS D = (S, S 0 , , -→) and all s ∈ S, let ♦(s) = {N | s -→ N } and, for each a ∈ Σ, a (s) = {t | s a t}. Define the (normal-form) νcalculus expression dn(D) = (S, S 0 , ∆), with ∆ given as in [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]. For a ν-calculus

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

Theorem 9. For DMTS D 1 , D 2 and ν-calculus expressions N 1 , N 2 , D 1 ≤ m D 2 iff dn(D 1 ) ≤ m dn(D 2 ) and N 1 ≤ m N 2 iff nd(N 1 ) ≤ m nd(N 2 ).
⊓ ⊔

Specification theory

Structural specifications typically come equipped with operations which allow for compositional reasoning, viz. conjunction, structural composition, and quo-tient, cf. [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]. On deterministic MTS, these operations can be given easily using simple structural operational rules (for such semantics of weighted systems, see e.g., [START_REF] Klin | Structural operational semantics for stochastic and weighted transition systems[END_REF]). For non-deterministic systems this is significantly harder; in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] it is shown that DMTS and AA permit these operations and, additionally but trivially, disjunction. Here we show how to extend these operations on nondeterministic systems to our quantitative setting with structured labels. We remark that structural composition and quotient operators are wellknown from some logics, such as, e.g., linear [START_REF] Girard | Linear logic[END_REF] or spatial logic [START_REF] Caires | A spatial logic for concurrency[END_REF], and were extended to quite general contexts [START_REF] Cardelli | Modular Markovian logic[END_REF]. However, whereas these operators are part of the formal syntax in those logics, for us they are simply operations on logical expressions (or DMTS, or AA). Consequently [START_REF] Fahrenberg | Structural refinement for the modal nu-calculus[END_REF], structural composition is generally only a sound over-approximation of the semantic composition.

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

Disjunction and conjunction

Disjunction of specifications is easily defined as we allow multiple initial states.

For DMTS D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ), we can hence define D 1 ∨ D 2 = (S 1 ∪ S 2 , S 0 1 ∪ S 0 2 , 1 ∪ 2 , -→ 1 ∪ -→ 2 ) (with all unions disjoint). For conjunction, we let D 1 ∧ D 2 = (S 1 × S 2 , S 0 1 × S 0 2 , , -→), with -(s 1 , s 2 ) a1 a2 (t 1 , t 2 ) whenever s 1 a1 1 t 1 , s 2 a2 2 t 2 and a 1 a 2 is defined, -for all s 1 -→ N 1 , (s 1 , s 2 ) -→ {(a 1 a 2 , (t 1 , t 2 )) | (a 1 , t 1 ) ∈ N 1 , s 2 a2 2 t 2 , a 1 a 2 defined}, -for all s 2 -→ N 2 , (s 1 , s 2 ) -→ {(a 1 a 2 , (t 1 , t 2 )) | (a 2 , t 2 ) ∈ N 2 , s 1 a1 1 t 1 , a 1 a 2 defined}. Theorem 10. For all specifications S 1 , S 2 , S 3 , -S 1 ∨ S 2 ≤ m S 3 iff S 1 ≤ m S 3 and S 2 ≤ m S 3 , -S 1 ≤ m S 2 ∧ S 3 iff S 1 ≤ m S 2 and S 1 ≤ m S 3 , -S 1 ∨ S 2 = S 1 ∪ S 2 , and S 1 ∧ S 2 = S 1 ∩ S 2 .
With bottom and top elements given by ⊥ = (∅, ∅, ∅) and ⊤ = ({s}, {s}, Tran ⊤ ) with Tran ⊤ (s) = 2 2 Σ×{s} , our classes of specifications form bounded distributive lattices up to ≡ m .

Structural composition

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

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

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

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

⊓ ⊔

Quotient

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

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

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

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

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

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

Example 13. Consider the two simple systems in Fig. 4 and their quotient under ∩ , i.e., where label synchronization is intersection. During the construction and the translation back to DMTS, many states were eliminated as they were inconsistent (their Tran-set was empty). For instance, there is no may transition to state {s 2 /t 2 }, because when it is composed with t 2 there is no guarantee of late-transition, hence no guarantee to refine s 2 . Theorem 14. For all specifications S 1 , S 2 , S 3 , S 1 S 2 ≤ m S 3 iff S 2 ≤ m S 3 /S 1 .

Robust Specification Theories

We proceed to lift the results of the previous sections to a quantitative setting, where the Boolean notions of modal and thorough refinement are replaced by refinement distances. We have shown in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Fahrenberg | The quantitative linear-timebranching-time spectrum[END_REF] that a good setting for quantitative analysis is given by the one of recursively specified trace distances on an abstract commutative quantale as defined below; we refer to the above-cited papers for a detailed exposition of how this framework covers all common approaches to quantitative analysis.

Denote by Σ ∞ = Σ * ∪ Σ ω the set of finite and infinite traces over Σ.

Recursively specified trace distances

Recall that a (commutative) quantale consists of a complete lattice (Ä, ⊑ Ä ) and a commutative, associative addition operation Ä which distributes over arbitrary suprema; we denote by ⊥ Ä , ⊤ Ä the bottom and top elements of Ä. We call a function d : X × X → Ä, for a set X and a quantale Ä, an Ä-hemimetric if it satisfies d(x, x) = ⊥ Ä for all x ∈ X and d(x, z) ⊑ Ä d(x, y) Ä d(y, z) for all x, y, z ∈ X. Ä-hemimetrics are generalizations of distances: for Ä = Ê ≥0 ∪ {∞} the extended real line, an (Ê ≥0 ∪ {∞})-hemimetric is simply an extended hemimetric.

A recursive trace distance specification F = (Ä, eval, d Ä tr , F ) consists of a quantale Ä, a quantale morphism eval : Ä → Ê ≥0 ∪ {∞}, an Ä-hemimetric d Ä tr : Σ ∞ ×Σ ∞ → Ä (called lifted trace distance), and a distance iterator function F : Σ × Σ × Ä → Ä. F must be monotone in the third and anti-monotone in the second coordinate and satisfy an extended triangle inequality: for all a, b, c ∈ Σ

and α, β ∈ Ä, F (a, b, α) Ä F (b, c, β) ⊒ Ä F (a, c, α Ä β).
F is to specify d Ä tr recursively in the sense that for all a, b ∈ Σ and all σ, τ ∈ Σ ∞ (and with "." denoting concatenation),

d Ä tr (a.σ, b.τ ) = F (a, b, d Ä tr (σ, τ )) . (3)
The trace distance associated with such a distance specification is

d tr : Σ ∞ × Σ ∞ → Ê ≥0 given by d tr = eval • d Ä tr .
Note that d Ä tr specializes to a distance on labels (because Σ ⊆ Σ ∞ ); we require that this is compatible with label refinement in the sense that a b

implies d Ä tr (a, b) = ⊥ Ä . Then (3) implies that whenever a b, then F (a, b, ⊥ Ä ) = d Ä tr (a, b) = ⊥ Ä .
As an inverse property, we say that F is recursively separating if F (a, b, α) = ⊥ Ä implies that a b and α = ⊥ Ä .

Example 15. It is shown in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Fahrenberg | The quantitative linear-timebranching-time spectrum[END_REF] that all commonly used trace distances obey recursive characterizations as above. We give a few examples, all of which are recursively separating:

-The point-wise distance from [START_REF] De Alfaro | Model checking discounted temporal properties[END_REF], for example, has Ä = Ê ≥0 ∪{∞}, eval = id

((u 1 , [l 1 , r 1 ]), (u 2 , [l 2 , r 2 ])) = sup x1∈[l1,r1] inf x2∈[l2,r2] |x 1 -x 2 | = max(l 2 -l 1 , r 1 -r 2 , 0) if u 1 = u 2 and ∞ otherwise, cf. [3].
-The discounting distance, also used in [START_REF] De Alfaro | Model checking discounted temporal properties[END_REF], again uses Ä = Ê ≥0 ∪ {∞} and

eval = id, but d Ä tr (a.σ, b.τ ) = d(a, b) + λd Ä tr (σ, τ ) for a constant λ ∈ [0, 1[.
-For the limit-average distance used in [START_REF] Černý | Simulation distances[END_REF] and others, Ä = (Ê ≥0 ∪ {∞}) AE , eval(α) = lim inf j∈AE α(j), and

d Ä tr (a.σ, b.τ )(j) = 1 j + 1 d(a, b) + j j + 1 d Ä tr (σ, τ )(j -1) .
-The discrete trace distance is given by d tr (σ, τ ) = 0 if σ τ and ∞ otherwise For the rest of this paper, we fix a recursively specified trace distance.

Refinement distances

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

Definition 16. The lifted refinement distance on the states of DMTS

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

d Ä m (s 1 , s 2 ) = max      sup s1 a 1 t1 inf s2 a 2 t2 F (a 1 , a 2 , d Ä m (t 1 , t 2 )) , sup s2-→N2 inf s1-→N1 sup (a1,t1)∈N1 inf (a2,t2)∈N2 F (a 1 , a 2 , d Ä m (t 1 , t 2 ))
.

For AA A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), the equations are instead d Ä m (s 1 , s 2 ) = sup M1∈Tran1(s1) inf M2∈Tran2(s2) max      sup (a1,t1)∈M1 inf (a2,t2)∈M2 F (a 1 , a 2 , d Ä m (t 1 , t 2 )) , sup (a2,t2)∈M2 inf (a1,t1)∈M1 F (a 1 , a 2 , d Ä m (t 1 , t 2 )) ,
and for ν-calculus expressions

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

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

The lifted refinement distance between specifications is defined by

d Ä m (S 1 , S 2 ) = sup s 0 1 ∈S 0 1 inf s 0 2 ∈S 0 2 d Ä m (s 0 1 , s 0 2 ) .
Analogously to thorough refinement, there is also a lifted thorough refinement distance, given by d Ä th , with values in Ê ≥0 ∪ {∞}, which will be the ones one is interested in for concrete applications.

th (S 1 , S 2 ) = sup I1∈ S1 inf I2∈ S2 d Ä m (I 1 , I 2 ).
Example 17. We compute the discounting refinement distance between the DMTS x and x ′ in Figs. 2 and3, assuming sup-inf distance on quantitative labels. We have

d m (x, x ′ ) = max(0 + λd m (x, x ′ ), 0 + λd m (y, y ′ )) , d m (y, y ′ ) = max(0 + λd m (x, x ′ ), 1 + λd m (y, y ′ ) , the least fixed point of which is d m (x, x ′ ) = λ 1-λ . Similarly, d m (x ′ , x) = λ 1-λ . Note that x ≤ m x ′ and x ′ ≤ m x.
The following quantitative extension of Theorems 6 and 9 shows that our translations preserve and reflect refinement distances.

Theorem 18. For all DMTS D 1 , D 2 , all AA A 1 , A 2 and all ν-calculus expressions N 1 , N 2 :

d Ä m (D 1 , D 2 ) = d Ä m (da(D 1 ), da(D 2 )) d Ä m (A 1 , A 2 ) = d Ä m (ad(A 1 ), ad(A 2 )) d Ä m (D 1 , D 2 ) = d Ä m (dn(D 1 ), dn(D 2 )) d Ä m (N 1 , N 2 ) = d Ä m (nd(N 1 ), nd(N 2 ))
We sum up important properties of our distances:

Proposition 19. The functions d Ä m , d Ä th are Ä-hemimetrics, and d m , d th are hemimetrics. For specifications S 1 , S 2 , S 1 ≤ m S 2 implies d Ä m (S 1 , S 2 ) = ⊥ Ä , and S 1 ≤ th S 2 implies d Ä th (S 1 , S 2 ) = ⊥ Ä .
If F is recursively separating, then also the reverse implications hold.

For the discrete distances,

d m (S 1 , S 2 ) = 0 if S 1 ≤ m S 2 and ∞ otherwise. Similarly, d th (S 1 , S 2 ) = 0 if S 1 ≤ th S 2 and ∞ otherwise.
As a quantitative analogy to the implication from (Boolean) modal refinement to thorough refinement (Proposition 5), the next theorem shows that thorough refinement distance is bounded above by modal refinement distance. Note that for the discrete trace distance (and using Proposition 19), this is equivalent to the Boolean statement.

Theorem 20. For all specifications S 1 , S 2 , d Ä th (S 1 , S 2 ) ⊑ Ä d Ä m (S 1 , S 2 ).

Disjunction and conjunction

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

Definition 21. The α-relaxed implementation semantics of S, for a specifica-

tion S and α ∈ Ä, is S α = {I implementation | d Ä m (I, S) ⊑ α}.
Hence, S α comprises all labeled transition systems which are implementations of S up to α. Note that by Proposition 19 and for F recursively separating, S ⊥Ä = S . Theorem 22. For all specifications S 1 , S 2 , S 3 and α ∈ Ä, -

-d Ä m (S 1 ∨ S 2 , S 3 ) = max(d Ä m (S 1 , S 3 ), d Ä m (S 2 , S 3 )), I a, 2 D1 a, [0, 1] D2 a, [3, 4] D1 ∧ D2
d Ä m (S 1 , S 2 ∧ S 3 ) ⊒ Ä max(d Ä m (S 1 , S 2 ), d Ä m (S 1 , S 3 )), -S 1 ∨ S 2 α = S 1 α ∪ S 2 α , and S 1 ∧ S 2 α ⊆ S 1 α ∩ S 2 α .
The below example shows why the inclusions above cannot be replaced by equalities. To sum up, disjunction is quantitatively sound and complete, whereas conjunction is only quantitatively sound.

Example 23. For the point-wise or discounting distances, the DMTS in Fig. 5 are such that d m (I,

D 1 ) = d m (I, D 2 ) = 1, but d m (I, D 1 ∧ D 2 ) = ∞. Hence d m (I, S 1 ∧ S 2 ) = max(d m (I, S 1 ), d m (I, S 2 )), and I ∈ D 1 1 ∩ D 2 1 , but I / ∈ D 1 ∧ D 2 1 .

Structural composition and quotient

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

Let P : Ä × Ä → Ä be a function which is monotone in both coordinates, has P (α, ⊥ Ä ) = P (⊥ Ä , α) = α and P (α, ⊤ Ä ) = P (⊤ Ä , α) = ⊤ Ä for all α ∈ Ä. We require that for all a 1 , b 1 , a 2 , b 2 ∈ Σ and α, β ∈ Ä with F (a 1 , a 2 , α) = ⊤ and

F (b 1 , b 2 , β) = ⊤, a 1 b 1 is defined iff a 2 b 2
is, and if both are defined, then

F (a 1 b 1 , a 2 b 2 , P (α, β)) ⊑ Ä P (F (a 1 , a 2 , α), F (b 1 , b 2 , β)) . (4) Note that (4) implies that d tr (a 1 a 2 , b 1 b 2 ) ⊑ Ä P (d tr (a 1 , b 1 ), d tr (a 2 , b 2 )).
Hence P provides a uniform bound3 on distances between synchronized labels, and (4) extends this property so that it holds recursively. Also, this is a generalization of the condition that we imposed on in Section 2; it is shown in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF] that it holds for all common label synchronizations.

The following theorems show that composition is uniformly continuous (i.e., a quantitative generalization of independent implementability; Corollary 12) and that quotient preserves and reflects refinement distance (a quantitative generalization of Theorem 14).

Theorem 24.

For all specifications

S 1 , S 2 , S 3 , S 4 , d Ä m (S 1 S 2 , S 3 S 4 ) ⊑ Ä P (d Ä m (S 1 , S 3 ), d Ä m (S 2 , S 4 )). Theorem 25. For all specifications S 1 , S 2 , S 3 , d Ä m (S 1 S 2 , S 3 ) = d Ä m (S 2 , S 3 /S 1 ).

Conclusion

We have presented a framework for compositional and iterative design and verification of systems which supports quantities and system and action refinement. Moreover, it is robust, in that it uses distances to measure quantitative refinement and the operations preserve distances. The framework is very general. It can be applied to a large variety of quantities (energy, time, resource consumption etc.) and implement the robustness notions associated with them. It is also agnostic with respect to the type of specifications used, as it applies equally to behavioral and logical specifications. This means that logical and behavioral quantitative specifications can be freely combined in quantitative system development.

Appendix: Proofs

Proof (of Theorem 10).

The proof that S 1 ∨S 2 ≤ m S 3 iff S 1 ≤ m S 3 and S 2 ≤ m S 3 is trivial: any modal refinement R ⊆ (S 1 ∪ S 2 ) × S 3 splits into two refinements R 1 ⊆ S 1 × S 3 , R 2 ⊆ S 2 × S 3 and vice versa.
For the proof of the second claim, which we show for DMTS, we prove the back direction first. Let

R 2 ⊆ S 1 × S 2 , R 3 ⊆ S 1 × S 3 be initialized (DMTS) modal refinements and define R = {(s 1 , (s 2 , s 3 )) | (s 1 , s 2 ) ∈ R 1 , (s 1 , s 3 ) ∈ R 3 } ⊆ S 1 × (S 2 × S 3 ). Then R is initialized. Now let (s 1 , (s 2 , s 3 )) ∈ R, then (s 1 , s 2 ) ∈ R 2 and (s 1 , s 3 ) ∈ R 3 . Assume that s 1 a1 1 t 1 , then by S 1 ≤ m S 2 , we have s 2 a2 2 t 2 with a 1 a 2 and (t 1 , t 2 ) ∈ R 2 .
Similarly, by S 1 ≤ m S 3 , we have s 3

a3 3 t 3 with a 1 a 3 and (t 1 , t 3 ) ∈ R 3 .
But then also a 1 a 2 a 3 and (t 1 , (t 2 , t 3 )) ∈ R, and (s 2 , s 3 ) a2 a3 (t 2 , t 3 ) by definition. Assume that (s 2 , s 3 ) -→ N . Without loss of generality we can assume that there is

s 2 -→ 2 N 2 such that N = {(a 2 a 3 , (t 2 , t 3 )) | (a 2 , t 2 ) ∈ N 2 , s 3 a3 3 t 3 }. By S 1 ≤ m S 2 , we have s 1 -→ 1 N 1 such that ∀(a 1 , t 1 ) ∈ N 1 : ∃(a 2 , t 2 ) ∈ N 2 : a 1 a 2 , (t 1 , t 2 ) ∈ R 2 .
Let (a 1 , t 1 ) ∈ N 1 , then also s 1 a1 1 t 1 , so by S 1 ≤ m S 3 , there is s 3 a3 3 t 3 with a 1 a 3 and (t 1 , t 3 ) ∈ R 3 . By the above, we also have (a 2 , t 2 ) ∈ N 2 such that a 1 a 2 and (t 1 , t 2 ) ∈ R 2 , but then (a 2 a 3 , (t 2 , t 3 )) ∈ N , a 1 a 2 ∧ a 3 , and (t 1 , (t 2 , t 3 )) ∈ R.

For the other direction of the second claim, let R ⊆ S 1 ×(S 2 ×S 3 ) be an initialized (DMTS) modal refinement. We show that S 1 ≤ m S 2 , the proof of S 1 ≤ m S 3 being entirely analogous. Define R 2 = {(s 1 , s 2 ) | ∃s 3 ∈ S 3 : (s 1 , (s 2 , s 3 )) ∈ R} ⊆ S 1 × S 2 , then R 2 is initialized.

Let (s 1 , s 2 ) ∈ R 2 , then we must have s 3 ∈ S 3 such that (s 1 , (s 2 , s 3 )) ∈ R. Assume that s 1 a1 1 t 1 , then also (s 2 , s 3 ) a (t 2 , t 3 ) for some a with a 1 a and (t 1 , (t 2 , t 3 )) ∈ R. By construction we have s 2 a2 2 t 2 and s 3 a3 3 t 3 such that a = a 2 a 3 , but then a 1 a 2 a 3 a 2 and (t 1 , t 2 ) ∈ R 2 .

Assume that s 2 -→ 2 N 2 , then by construction, (s 2 , s 3 )

-→ N = {(a 2 a 3 , (t 2 , t 3 )) | (a 2 , t 2 ) ∈ N 2 , s 3 a3 3 t 3 }. By S 1 ≤ m S 2 ∧ S 3 , we have s 1 -→ 1 N 1 such that ∀(a 1 , t 1 ) ∈ N 1 : ∃(a, (t 2 , t 3 )) ∈ N : a 1 a, (t 1 , (t 2 , t 3 )) ∈ R.
Let (a 1 , t 1 ) ∈ N 1 , then we have (a, (t 2 , t 3 )) ∈ N for which a 1 a and (t 1 , (t 2 , t 3 )) ∈ R. By construction of N , this implies that there are (a 2 , t 2 ) ∈ N 2 and s 3 a3 3 t 3 such that a = a 2 a 3 , but then a 1 a 2 a 3 a 2 and (t 1 , t 2 ) ∈ R. As to the last claims of the theorem, S 1 ∧S 2 = S 1 ∩ S 2 is clear from what we just proved: for all implementations I, I ≤ m S 1 ∧S 2 iff I ≤ m S 1 and I ≤ m S 2 . For the other part, it is clear by construction that for any implementation I, any witness R for I ≤ m S 1 is also a witness for I ≤ m S 1 ∨ S 2 , and similarly for S 2 , hence S 1 ∪ S 2 ⊆ S 1 ∨ S 2 .

To show the other inclusion, we note that an initialized refinement R witnessing I ≤ m S 1 ∨ S 2 must relate the initial state of I either to an initial state of

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

1 ) ∈ M 1 , there is (a 2 , t 2 ) ∈ M 2 and β = d Ä m (t 1 , t 2 )
such that F (a 1 , a 2 , β) ⊑ Ä α, and that for all (a 2 , t 2 ) ∈ M 2 , there is (a

1 , t 1 ) ∈ M 1 and β = d Ä m (t 1 , t 2 ) such that F (a 1 , a 2 , β) ⊑ Ä α. ⊓ ⊔ Proof (of Theorem 18). d Ä m (da(D 1 ), da(D 2 )) ⊑ Ä d Ä m (D 1 , D 2 ): Let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ) be DMTS. There exists a DMTS refinement family R = {R α ⊆ S 1 × S 2 | α ∈ Ä} such that for all s 0 1 ∈ S 0 1 , there is s 0 2 ∈ S 0 2 with (s 0 1 , s 0 2 ) ∈ R d Ä m (D1,D2
) . We show that R is an AA refinement family.

Let α ∈ Ä and (s 1 , s 2 ) ∈ R α . Let M 1 ∈ Tran 1 (s 1 ) and define

M 2 = {(a 2 , t 2 ) | s 2 a2 2 t 2 , ∃(a 1 , t 1 ) ∈ M 1 : ∃β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) ⊑ Ä α}.
The condition

∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) ⊑ α
is satisfied by construction. For the inverse condition, let (a 1 , t 1 ) ∈ M 1 , then s 1 a1 1 t 1 , and as R is a DMTS refinement family, this implies that there is s 2 a2 2 t 2 and β ∈ Ä for which (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) ⊑ Ä α, so that (a 2 , t 2 ) ∈ M 2 by construction.

We are left with showing that M 2 ∈ Tran 2 (s 2 ). First we notice that by construction, indeed s 2 a2 2 t 2 for all (a 2 , t 2 ) ∈ M 2 . Now let s 2 -→ N 2 ; we need to show that N 2 ∩ M 2 = ∅.

We have s

1 -→ N 1 such that ∀(a 1 , t 1 ) ∈ N 1 : ∃(a 2 , t 2 ) ∈ N 2 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) ⊑ Ä α. We know that N 1 ∩M 1 = ∅, so let (a 1 , t 1 ) ∈ N 1 ∩M 1 . Then there is (a 2 , t 2 ) ∈ N 2 and β ∈ Ä such that (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) ⊑ Ä α. But (a 2 , t 2 ) ∈ N 2 implies s 2 a2 2 t 2 , hence (a 2 , t 2 ) ∈ M 2 . d Ä m (D 1 , D 2 ) ⊑ Ä d Ä m (da(D 1 ), da(D 2 )): Let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ) be DMTS. There exists an AA refinement family R = {R α ⊆ S 1 × S 2 | α ∈ Ä} such that for all s 0 1 ∈ S 0 1 , there is s 0 2 ∈ S 0 2 with (s 0 1 , s 0 2 ) ∈ R d Ä m (da(D1),da(D2)) . We show that R is a DMTS refinement family. Let α ∈ Ä and (s 1 , s 2 ) ∈ R α . Let s 1 a1 1 t 1 , then we cannot have s 1 -→ ∅. Let M 1 = {(a 1 , t 1 )} ∪ {N 1 | s 1 -→ N 1 }, then M 1 ∈ Tran 1 (s 1
) by construction. This implies that there is M 2 ∈ Tran 2 (s 2 ), (a 2 , t 2 ) ∈ M 2 and β ∈ Ä such that (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) ⊑ Ä α, but then also s 2 a2 t 2 as was to be shown.

Let s 2 -→ N 2 and assume, for the sake of contradiction, that there is no

s 1 -→ N 1 for which ∀(a 1 , t 1 ) ∈ N 1 : ∃(a 2 , t 2 ) ∈ N 2 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) ⊑ Ä α holds. Then for each s 1 -→ N 1 , there is an element (a N1 , t N1 ) ∈ N 1 such that ∃(a 2 , t 2 ) ∈ N 2 , β ∈ Ä : (t N1 , t 2 ) ∈ R β , F (a N1 , a 2 , β) ⊑ Ä α does not hold. Let M 1 = {(a N1 , t N1 ) | s 1 -→ N 1 }, then M 1 ∈ Tran 1 (s 1 ) by construction.
Hence we have

M 2 ∈ Tran 2 (s 2 ) such that ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 2 ) ∈ M 1 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) ⊑ α. Now N 2 ∩ M 2 = ∅, so let (a 2 , t 2 ) ∈ N 2 ∩ M 2 , then there is (a 1 , t 1 ) ∈ M 1 and β ∈ Ä such that (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) ⊑ Ä α, in contradiction to how M 1 was constructed. d Ä m (ad(A 1 ), ad(A 2 )) ⊑ Ä d Ä m (A 1 , A 2 ): Let A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ) be AA, with DMTS trans- lations (D 1 , D 0 1 , -→ 1 , 1 ), (D 2 , D 0 2 , -→ 2 , 2 ). There is an AA refinement family R = {R α ⊆ S 1 × S 2 | α ∈ Ä} such that for all s 0 1 ∈ S 0 1 , there is s 0 2 ∈ S 0 2 with (s 0 1 , s 0 2 ) ∈ R d Ä m (A1,A2) . Define a relation family R ′ = {R ′ α ⊆ D 1 × D 2 | α ∈ Ä} by R ′ α = {(M 1 , M 2 ) | ∃(s 1 , s 2 ) ∈ R α : M 1 ∈ Tran 1 (s 1 ), M 2 ∈ Tran(s 2 ), ∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) ⊑ Ä α, ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) ⊑ Ä α. We show that R ′ is a witness for d Ä m (ad(A 1 ), ad(A 2 )) ⊑ Ä d Ä m (A 1 , A 2 ). Let α ∈ Ä and (M 1 , M 2 ) ∈ R ′ α . Let M 2 -→ 2 N 2 . By construction of -→, there is (a 2 , t 2 ) ∈ M 2 such that N 2 = {(a 2 , M ′ 2 ) | M ′ 2 ∈ Tran 2 (t 2 )}. Then (M 1 , M 2 ) ∈ R ′ α implies that there must be (a 1 , t 1 ) ∈ M 1 and β ∈ Ä such that (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) ⊑ Ä α. Let N 1 = {(a 1 , M ′ 1 ) | M ′ 1 ∈ Tran 1 (t 1 )}, then M 1 -→ 1 N 1 . We show that ∀(a 1 , M ′ 1 ) ∈ N 1 : ∃(a 2 , M ′ 2 ) ∈ N 2 : (M ′ 1 , M ′ 2 ) ∈ R ′ β : Let (a 1 , M ′ 1 ) ∈ N 1 , then M ′ 1 ∈ Tran 1 (t 1 ). From (t 1 , t 2 ) ∈ R β we get M ′ 2 ∈ Tran 2 (t 2 ) such that ∀(b 1 , u 1 ) ∈ M ′ 1 : ∃(b 2 , u 2 ) ∈ M ′ 2 , γ ∈ Ä : (u 1 , u 2 ) ∈ R γ , F (b 1 , b 2 , γ) ⊑ Ä β, ∀(b 2 , u 2 ) ∈ M ′ 2 : ∃(b 1 , u 1 ) ∈ M ′ 1 , γ ∈ Ä : (u 1 , u 2 ) ∈ R γ , F (b 1 , b 2 , γ) ⊑ Ä β, hence (M ′ 1 , M ′ 2 ) ∈ R ′ β ; also, (a 2 , M ′ 2 ) ∈ N 2 by construction of N 2 . Let M 1 a1 1 M ′ 1 , then we have M 1 -→ 1 N 1 for which (a 1 , M ′ 1 ) ∈ N 1 by construction of 1 .
This in turn implies that there must be (a

1 , t 1 ) ∈ M 1 such that N 1 = {(a 1 , M ′′ 1 ) | M ′′ 1 ∈ Tran 1 (t 1 )}. By (M 1 , M 2 ) ∈ R ′ α , we get (a 2 , t 2 ) ∈ M 2 and β ∈ Ä such that (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) ⊑ Ä α. Let N 2 = {(a 2 , M ′ 2 ) | M ′ 2 ∈ Tran 2 (t 2 )}, then M 2 -→ 2 N 2 and hence M 2 a2 2 M ′ 2 for all (a 2 , M ′ 2 ) ∈ N 2 .
By the same arguments as above, there is

(a 2 , M ′ 2 ) ∈ N 2 for which (M ′ 1 , M ′ 2 ) ∈ R ′ β . Let (s 1 , s 2 ) ∈ R 0 and M 1 ∈ Tran 1 (s 1 ), then we have M 2 ∈ Tran 2 (s 2 ) such that ∀(a 1 , t 1 ) ∈ M 1 : ∃(a 2 , t 2 ) ∈ M 2 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) = 0, ∀(a 2 , t 2 ) ∈ M 2 : ∃(a 1 , t 1 ) ∈ M 1 , β ∈ Ä : (t 1 , t 2 ) ∈ R β , F (a 1 , a 2 , β) = 0. (10)
Using the definition of the distance, we see that the condition F (a 1 , a 2 , β) = 0 is equivalent to a 1 a 2 and β = 0, hence [START_REF] Caires | A spatial logic for concurrency[END_REF] degenerates to

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

Again by definition, we see that for any AA A

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

d th (A 1 , A 2 ) = sup I1∈ A1 inf I2∈ A2 d m (I 1 , I 2 ) = 0 if ∀I 1 ∈ A 1 : ∃I 2 ∈ A 2 : I 1 ≤ m I 2 , ∞ otherwise, = 0 if A 1 ⊆ A 2 , ∞ otherwise. Hence d th (A 1 , A 2 ) = 0 if A 1 ≤ th A 2 and d th (A 1 , A 2 ) = ∞ otherwise. ⊓ ⊔
Proof (of Theorem 20). We prove the statement for AA; for DMTS and νcalculus expressions it then follows from Theorem 18.

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

R 2 = {R 2 α ⊆ S × S 2 | α ∈ Ä} by R 2 α = R 1 • R α = {(s, s 2 )
| ∃s 1 ∈ S : (s, s 1 ) ∈ R 1 , (s 1 , s 2 ) ∈ R α . We define a LTS I 2 = (S 2 , S 0 2 , T 2 ) as follows:

For all α ∈ Ä with α = ⊤ Ä and (s, s 2 ) ∈ R 2 α : We must have s 1 ∈ S 1 with (s, s 1 ) ∈ R 1 and (s 1 , s 2 ) ∈ R α . Then there is M 1 ∈ Tran 1 (s 1 ) such that for all s a -→ t, there is (a, t 1 ) ∈ M 1 with (t, t 1 ) ∈ R 1 , -for all (a 1 , t We show that R 2 is a witness for d Ä m (I, I 2 ); clearly, R 2 is initialized. Let α ∈ Ä with α = ⊤ Ä and (s, s 2 ) ∈ R 2 α , then there is s 1 ∈ S 1 with (s, s 1 ) ∈ R 1 and (s 1 , s 2 ) ∈ R α . We also have M 1 ∈ Tran 1 (s 1 ) such that for all s a -→ t, there is (a, t 1 ) ∈ M 1 with (t, t 1 ) ∈ R 1 , -for all (a 1 , t This implies that there is M 1 ∈ Tran 1 (s 1 ), β ∈ Ä and (a 1 , t 1 ) ∈ M 1 with (t 1 , t 2 ) ∈ R β and F (a 1 , a 2 , β) ⊑ α. But then there is also s a1 -→ t with (t, t 1 ) ∈ R 1 , hence (t, t 2 ) ∈ R Let α ∈ Ä and (s 1 , s 2 ) ∈ R 2 α , then we have s 3 ∈ S 3 for which (s 1 , (s 2 , s 3 )) ∈ R α . Assume first that s 1 a1 t 1 , then there is (s 2 , s 3 ) a (t 2 , t 3 ) and β ∈ Ä such that F (a 1 , a, β) ⊑ Ä α and (t 1 , (t 2 , t 3 )) ∈ R β , hence (t 1 , t 2 ) ∈ R 2 β . By construction of D 2 ∧ D 3 , there are s 2 a2 t 2 and s 3 a3 t 3 such that a = a 2 a 3 , but then by anti-monotonicity, F (a 1 , a 2 , β) ⊑ Ä F (a 1 , a, β) ⊑ α. Now assume s 2 -→ N 2 , then by construction, (s 2 , s 3 ) -→ N = {(a 2 a 3 , (t 2 , t 3 )) | (a 2 , t 2 ) ∈ N 2 , s 3 a3 3 t 3 }. Hence we have s 1 -→ 1 N 1 such that ∀(a 1 , t 1 ) ∈ N 1 : ∃(a, (t 2 , t 3 )) ∈ N, β ∈ Ä : F (a 1 , a, β) ⊑ α, (t 1 , (t 2 , t 3 )) ∈ R β .

Let (a 1 , t 1 ) ∈ N 1 , then we have (a, (t 2 , t 3 )) ∈ N and β ∈ Ä for which F (a 1 , a, β) ⊑ Ä α and (t 1 , (t 2 , t 3 )) ∈ R β , hence (t 1 , t 2 ) ∈ R 2 β . By construction of N , this implies that there are (a 2 , t 2 ) ∈ N 2 and s 3 a3 3 t 3 such that a = a 2 a 3 , but then by anti-monotonicity, F (a 1 , a 2 , β) ⊑ Ä F (a 1 , a, β) ⊑ α.

We

Fig. 1 .

 1 Fig. 1. Two specifications of a vending machine

Fig. 2 .Fig. 3 .

 23 Fig. 2. A DMTS and its ν-calculus translation

Fig. 4 .

 4 Fig. 4. Two DMTS and their quotient.

  and d Ä tr (a.σ, b.τ ) = max(d(a, b), d Ä tr (σ, τ )) , where d : Σ × Σ → Ê ≥0 ∪ {∞} is a hemimetric on labels. For the label set Σ = U × {[l, r] | l ∈ Ê ∪ {-∞}, r ∈ Ê ∪ {∞}, l ≤ r} from Example 1, one useful example of such a hemimetric is d

  (here we have extended to traces in the obvious way). It has a recursive characterization with Ä = Ê ≥0 ∪ {∞}, eval = id, and d tr (a.σ, b.τ ) = d tr (σ, τ ) if a b and ∞ otherwise.

  Using the eval function, one gets distances d m = eval • d Ä m and d th = eval • d Ä

Fig. 5 .

 5 Fig. 5. LTS I together with DMTS D1, D2 and their conjunction. For the point-wise or discounting distances, dm(I, D1) = dm(I, D2) = 1, but dm(I, D1 ∧ D2) = ∞.

  Theorem 22). We show the proof for DMTS.The proof that d Ä m (D 1 ∨D 2 , D 3 ) = max(d Ä m (D 1 , D 3 ), d Ä m (D 2 , D 3 )) is trivial: any refinement family witnessing d Ä m (D 1 ∨ D 2 , D 3 ) splits into two families witnessing d Ä m (D 1 , D 3 ) and d Ä m (D 2 , D 3) and vice versa.To show that d Ä m (D 1 , D 2 ∧ D 3 ) ⊒ Ä max(d Ä m (D 1 , D 2 ), d Ä m (D 1 , D 3 )), let R = {R α ⊆ S 1 × (S 2 × S 3 ) | α ∈ Ä} be a witness for d Ä m (D 1 , D 2 ∧ D 3 ) and define R 2 = {R 2 α ⊆ S 1 × S 2 | α ∈ Ä} by R 2 α = {(s 1 , s 2 ) | ∃s 3 ∈ S 3 : (s 1 , (s 2 , s 3 )) ∈ R α }for all α ∈ Ä.

  have shown that d Ä m (D 1 , D 2 ∧D 3 ) ⊑ Ä d Ä m (D 1 , D 2 ); the proof of d Ä m (D 1 , D 2 ∧ D 3 ) ⊑ Ä d Ä m (D 1 , D 3 ) is entirely analogous. The inclusion D 1 ∧ D 2 α ⊆ D 1 α ∩ D 2 α is clear now: If I ∈ D 1 ∧ D 2 α , i.e., d Ä m (I, D 1 ∧ D 2 ) ⊑ Ä α, then also d Ä m (I, D 1 ) ⊑ Ä α and d Ä m (I, D 2 ) ⊑ Ä α, thus I ∈ D 1 α ∩ D 2 α .

  1 ) ∈ M 1 , there is s a -→ t with (t, t 1 ) ∈ R 1 .This in turn implies that there is M 2 ∈ Tran 2 (s 2 ) satisfying the conditions in Definition 26. For all (a 2 , t 2 ) ∈ M 2 : add a transition s 2 a2 -→ t 2 to T 2 . We show that the identity relation{(s 2 , s 2 ) | s 2 ∈ S 2 } is a witness for I 2 ≤ m A 2 . Let s 2 ∈ S 2 and s 2 a2 -→ t 2 .By construction, there is M 2 ∈ Tran 2 (s 2 ) with (a 2 , t 2 ) ∈ M 2 , and for all (a ′ 2 , t ′ 2 ) ∈ M 2 , s 2

	a ′ 2 -→ t ′ 2 .

  1 ) ∈ M 1 , there is s a1 -→ t with (t, t 1 ) ∈ R 1 and thus M 2 ∈ Tran 2 (s 2 ) satisfying the conditions in Definition 26. Let s a -→ t, then there is (a, t 1 ) ∈ M 1 with (t, t 1 ) ∈ R 1 , hence also (a 2 , t 2 ) ∈ M 2 and β ∈ Ä with (t 1 , t 2 ) ∈ R β and F (a, a 2 , β) ⊑ Ä α. But then (t, t 2 ) ∈ R 2 . By construction, there is M 2 ∈ Tran 2 (s 2 ) with (a 2 , t 2 ) ∈ M 2 .

	and s 2 Let s 2 a2 -→ t 2 by construction. a2 -→ t 2	β ,

Indeed, P bears some similarity to the concept of modulus of continuity used in analysis.

⋆ This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.

S 1 or to an initial state of S 2 . In the first case, and by disjointness, R witnesses I ≤ m S 1 , in the second, I ≤ m S 2 .

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

⊓ ⊔

Proof (of Theorem 14). We show the proof for AA; for DMTS and ν-calculus expressions it will follow through the translations. Let A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), A 3 = (S 3 , S 0 3 , Tran 3 ); we show that

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

First we note that by construction, s ⊇ t implies s ≤ m t for all s, t ∈ S. Now assume that A 2 ≤ m A 3 /A 1 and let R = {(s 1 s 2 , s 3 ) | s 2 ≤ m s 3 /s 1 }; we show that R is a witness for A 1 A 2 ≤ m A 3 .

Let (s 1 s 2 , s 3 ) ∈ R and M ∈ Tran (s 1 s 2 ). Then M = M 1 M 2 with M 1 ∈ Tran 1 (s 1 ) and M 2 ∈ Tran 2 (s 2 ). As s 2 ≤ m s 3 /s 1 , we can pair M 2 with an M / ∈ Tran / (s 3 /s 1 ), i.e., such that the conditions in (1) are satisfied.

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

-Let (a, t 1 t 2 ) ∈ M , then there are a 1 , a 2 ∈ Σ with a = a 1 a 2 and (a 1 , t 1 ) ∈ M 1 , (a 2 , t 2 ) ∈ M 2 . By [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF], there is (a ′ 2 , t) ∈ M / such that a 2 a ′ 2 and t 2 ≤ m t. Note that a 3 = a 1 a ′ 2 is defined and a a 3 . Write t = {t 1 3 /t Assume, for the other direction of the proof, that

3 ) such that (1) holds for the pair M i,j , M i,j 3 .

Now define

We need to show that M ∈ Tran / (s). Let i ∈ {1, . . . , n} and M i,j

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

3 as was to be shown. For the reverse inclusion, let (a 3 , t 3 ) ∈ M i,j 3 . By [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF] and definition of M i,j , there are (a 1 , t 1 ) ∈ M i,j

1 and (a 2 , t 2 ) ∈ M 2 for which a 1 a 2 a 3 and t 1 t 2 ≤ m t 3 . Thus j = δ i (a 1 , t 1 ), so that there must be (a 2 , t) ∈ M for which t 3 /t 1 ∈ t, but then also (a 1 a 2 , t 3 ) ∈ M ⊲ M i,j

1 . We show that M 2 R M .

-Let (a 2 , t 2 ) ∈ M 2 . For every i = 1, . . . , n and every (a 1 , t 1 ) ∈∈ Tran 1 (t i 1 ), we can use [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF] to choose an element

-Let (a 2 , t) ∈ M , then we have (a 2 , t 2 ) ∈ M 2 satisfying the conditions in [START_REF] Bauer | Extending modal transition systems with structured labels[END_REF].

Hence t 1 t 2 ≤ m t 3 for all t 3 /t 1 ∈ t, so that (t 2 , t) ∈ R.

⊓ ⊔

Before we attempt any more proofs, we need to recall the notion of refinement family from [START_REF] Bauer | General quantitative specification theories with modalities[END_REF] and extend it to AA. We give the definition for AA only; for DMTS and the modal ν-calculus it is similar.

2 ) for some s 0 2 ∈ S 0 2 , and then

Let α ∈ Ä and (s 1 , s 2 ) ∈ R α , and assume that s 1 a1 1 t 1 . Then t 1 ∈ a1 1 (s 1 ), so that there is a 2 ∈ Σ, t 2 ∈ a2 2 (s 2 ) and β ∈ Ä for which (t 1 , t 2 ) ∈ R β and

Let α ∈ Ä and (x 1 , x 2 ) ∈ R α , and assume that x 1 a1

Proof (of Proposition 19, first part). We show the proposition for AA. First, if

, then there is an initialized refinement relation R ⊆ S 1 × S 2 , i.e., such that for all (s 1 , s 2 ) ∈ R and all M 1 ∈ Tran 1 (s 1 ), there is

As a special case, we conclude that d Ä th (A, A) = ⊥ Ä for all AA A. Next we show the triangle inequality for d Ä m . The triangle inequality for d Ä th will then follow from standard arguments used to show that the Hausdorff metric satisfies the triangle inequality. Let

This in turn implies that there is M 3 ∈ Tran 3 (s 3 ) with

Now let (a 1 , t 1 ) ∈ M 1 , then we get (a 2 , t 2 ) ∈ M 2 , (a 3 , t 3 ) ∈ M 3 and β 1 , β 2 ∈ Ä as in ( 6) and [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF]. Let β = β 1 Ä β 2 , then (t 1 , t 3 ) ∈ R β , and by the extended triangle inequality for F , F (a

Similarly, given (a 3 , t 3 ) ∈ M 3 , we can apply ( 9) and ( 7) to get (a

We have shown that d Ä m and d Ä tr are Ä-hemimetrics. Using monotonicity of the eval function, it follows that d m and d tr are hemimetrics.

⊓ ⊔

Proof (of Proposition 19, second part). We already know that, also for the discrete distances, Proof (of Theorem 24). We show the proof for AA. For i = 1, 2, 3, 4, let

be refinement families such that ∀s 0 1 ∈ S 0 1 :

Let α ∈ Ä and ((s 1 , s 2 ), (s 3 , s 4 )) ∈ R α , then we have α 1 , α 2 ∈ Ä with

then there must be

Thus we also have M 3 ∈ Tran 3 (s 3 ) and M 4 ∈ Tran 4 (s 4 ) such that

Let M 34 = M 3 M 4 ∈ Tran((s 3 , s 4 )). Let (a 12 , (t 1 , t 2 )) ∈ M 12 , then there are (a 1 , t 1 ) ∈ M 1 and (a 2 , t 2 ) ∈ M 2 for which a 12 = a 1 a 2 . Using [START_REF] Cardelli | Modular Markovian logic[END_REF] and ( 13), we get (a 3 , t 3 ) ∈ M 3 , (a 4 , t 4 ) ∈ M 4 and

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

We have shown that ∀(a 12 , (t 1 , t 2 )) ∈ M 12 : ∃(a 34 , (t 3 , t 4 )) ∈ M 34 , β ∈ Ä :

((t 1 , t 2 ), (t 3 , t 4 )) ∈ R β , F (a 12 , a 34 , β) ⊑ Ä α. To show the reverse property, start- ing from an element (a 34 , (t 3 , t 4 )) ∈ M 34 , we can proceed entirely analogous, using ( 12) and ( 14).

⊓ ⊔

Now define

We need to show that M ∈ Tran / (s). Let i ∈ {1, . . . , n} and M i,j 1 ∈ Tran 1 (s i 1 ); we claim that M ⊲ M i,j 1 R M i,j 3 . Let (a 3 , t 3 ) ∈ M ⊲ M i,j 1 , then a 3 = a 1 a 2 for some a 1 , a 2 such that t 3 /t 1 ∈ t, (a 1 , t 1 ) ∈ M i,j 1 and (a 2 , t) ∈ M . By disjointness, j = δ i (a 1 , t 1 ), hence by definition of M , (a 3 , t 3 ) ∈ M i,j

3 as was to be shown. For the reverse inclusion, let (a 3 , t 3 ) ∈ M i,j 3 . By definition of M i,j , there are (a 1 , t 1 ) ∈ M i,j 1 , (a 2 , t 2 ) ∈ M 2 and β for which F (a 1 a 2 , a 3 , β) ⊑ Ä α and d Ä m (t 1 t 2 , t 3 ) ⊑ Ä β. Thus j = δ i (a 1 , t 1 ), so that there must be (a 2 , t) ∈ M for which t 3 /t 1 ∈ t, but then also (a 1 a 2 , t 3 ) ∈ M ⊲ M i,j

1 . We show that the pair M 2 , M satisfies the conditions of Definition 26.

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

-Let (a 2 , t) ∈ M , then we have (a 2 , t 2 ) ∈ M 2 satisfying the conditions in [START_REF] Alfaro | Interface automata[END_REF].

Hence for all t 3 /t 1 ∈ t, there are i, a 1 , a 3 , β(t 3 /t 1 ) such that (a 3 , t 3 ) ∈ M i,δi(a1,t1) 3

, F (a 1 a 2 , a 3 , β(t 3 /t 1 )) ⊑ Ä α and d Ä m (t 1 t 2 , t 3 ) ⊑ Ä β(t 3 /t 1 ). Let β = sup{β(t 3 /t 1 ) | t 3 /t 1 ∈ t}, then d Ä m (t 1 t 2 , t 3 ) ⊑ Ä β for all t 3 /t 1 ∈ t, hence (t 2 , t) ∈ R β . ⊓ ⊔