Thi Thieu

Hoa Le

Roberto Passerone

Uli Fahrenberg

Axel Legay

Tag Machines for Modeling Heterogeneous Systems

Keywords: heterogeneity, tag machines, simulation

Embedded systems are often composed from components of very different natures, e.g., mechanical and electronic. Composition of heterogeneous components is generally not well-defined, making design and verification difficult. Denotational mathematical frameworks for reasoning effectively on heterogeneous composition have recently been made available. In this work, we propose an operational version of this formalism, based on tag machines, that can represent heterogeneous composition, and we provide conditions under which the heterogeneous composition can be captured soundly and completely. We have implemented our operational framework in a prototype tool which we use for experimental evaluation.

I. INTRODUCTION

Heterogeneity is a typical characteristic of embedded systems, which are composed from parts of different natures, such as mechanical, electronic and software components, interacting in feedback to optimize the system performance.

To deal with such heterogeneity, several modeling frameworks have been proposed, which are geared towards the representation and simulation of heterogeneous systems, e.g., Ptolemy II [START_REF] Liu | The Ptolemy II framework for visual languages[END_REF] or Metropolis [START_REF] Davare | METROII: A design environment for cyber-physical systems[END_REF]. Recently, Benveniste et al. [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF] have proposed a generic denotational framework based on tagged events where different notions of time and interaction paradigm, including physical time, logical time (synchronous and asynchronous), precedence relations, etc., can be captured and related by mapping tagged events over a common tag structure. The operational concept of Tag Machine [START_REF] Benveniste | Tag machines[END_REF] (TM), introduced earlier by the same authors, can be used to represent tag systems in a homogeneous context.

In this paper, we extend tag machines to the heterogeneous context. In particular, we study the relation between composition of denotational tag systems with that of tag machines. Our first contribution is to review and correct certain aspects of tag machines, and to provide conditions under which the operational model can fully and compositionally capture the denotational representation. Our second contribution is a simulation engine that supports heterogeneous tag machines, with which we experimentally evaluate our results on a significant case study.

The rest of the paper is organized as follows. In Section II, we recall notions of denotational tag systems and their composition. In Section III, we describe how tag machines are extended to represent heterogeneous tag systems. We discuss soundness and completeness of the TM composition in Section IV and V. Finally, we show the application of our prototype tool to an automotive use case in Section VI. Related Work. The theory of heterogeneous systems has been evolving actively in the last decade to assist embedded systems designers in dealing with composition of components with various Models of Computation and Communication (MoCC). Handling heterogeneous MoCC can be done strictly hierarchically in the pioneering framework of Ptolemy II [START_REF] Liu | The Ptolemy II framework for visual languages[END_REF], meaning that each level of the hierarchy is homogeneous while different interaction mechanisms are allowed to be specified at different levels in the hierarchy. This and other similar frameworks [START_REF] Davare | METROII: A design environment for cyber-physical systems[END_REF], [5] are oriented towards the representation and simulation of heterogeneous systems but lack formal semantics.

Another framework based on tags [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF] is instead oriented towards the formal verification and analysis of those systems. This framework was inspired by the Lee and Sangiovanni-Vincentelli formalism of tagged signal models [START_REF] Lee | A framework for comparing models of computation[END_REF], which has been long advocated as a unified modeling framework capable of capturing heterogeneous MoCC. In both models, tags play the important role of capturing various notions of time, where each tag system has its own tag structure that can be used to express an MoCC. By applying mappings between different tag structures, the authors define how to compose heterogeneous systems. Tag machines [START_REF] Benveniste | Tag machines[END_REF] are subsequently introduced as finite representations of tag systems, yet only their homogeneous composition has been defined. Tag machines are quite expressive. For instance, they have been applied to model a job-shop specification [START_REF] Dey | A tag machine based performance evaluation method for job-shop schedules[END_REF] where any trace of the composite tag machine from the start to the final state results in a valid job-shop schedule. Alternatively, tag systems can be represented by functional actors forming a Kleene algebra [START_REF]A Kleene algebra of tagged system actors[END_REF]. The approach is similar to that of Liu et al. [START_REF] Liu | The Ptolemy II framework for visual languages[END_REF] in that both use actors to represent basic components.

II. DENOTATIONAL TAG SYSTEMS

We use denotational tag systems as our semantic domain [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF], [START_REF] Lee | A framework for comparing models of computation[END_REF]. In intuitive terms, a tag system is a representation of the behaviors of a component in terms of sets of events that take place at its interface, intended as a collection of visible ports. Tags, which are associated to every event, characterize the temporal evolution of the behaviors.

By changing the structure of tags, one can choose among different notions of time. Formally, a tag structure T is a pair (T, ≤) where T is a set of tags and ≤ is a partial order on the tags. The ordering among tags is used to resolve the ordering among events at the system interface. For instance, by using the set of real numbers as tags, with their usual ordering, one can place events anywhere in real time. Conversely, a set of partially ordered symbolic tags can be used to express precedence between events in a branching-time setting.

Events occur at the interface of a component. A component exposes a set V of variables (or ports) which can take values from a set D. An event is a snapshot of a variable state, capturing the variable value at some point in time. Formally, an event e on a variable v ∈ V is a pair (τ, d) of a tag τ ∈ T and a value d ∈ D.

The simplest way of characterizing a behavior is as a collection of events for each variable. In this work, we are interested in constructing behaviors incrementally, using an executable model. For this reason, we index the events of a variable into a sequence, with the understanding that events later in the sequence have larger tags [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]. A behavior for a variable v is thus a function N → (T ×D). A behavior σ for a component assigns a sequence of events to every variable in V , and is then a function σ ∈ V → (N → (T × D)).

A component P with tag structure T , or tag system, is then a tuple P = (V, T , Σ), where Σ is a set of behaviors over the set of variables V . Individual events of a behavior σ ∈ Σ are identified by the tuple (v, n, τ, d), capturing the n-th occurrence of variable v as a pair of a tag τ and a value d. In the following, we denote with Σ(V, T ) the universe of all behaviors over a set of variables V and tag structure T . Homogeneous Composition. Combining tag systems over the same tag structure amounts to considering only those behaviors which are consistent with every component. When the sets of variables coincide, this operation corresponds to taking the intersection of the behaviors of all components. When the sets of variables are not the same, instead, two behaviors are considered consistent if they agree on the shared variables. In this case, we say that the behaviors are unifiable. Composition consists in retaining all and only the unifiable behaviors.

Formally, let

P 1 = (V 1 , T , Σ 1 ) and P 2 = (V 2 , T , Σ 2 ) be two tag systems over the same tag structure T . Two behaviors σ 1 ∈ Σ 1 and σ 2 ∈ Σ 2 are unifiable, written σ 1 σ 2 , whenever σ 1 | V1∩V2 = σ 2 | V1∩V2
, where σ| W denotes the restriction of behavior σ to the variables in set W . When unifiable, we may construct a new behavior σ = σ 1 σ 2 on the set of variables V 1 ∪V 2 as the combination of the two behaviors:

σ(v) = (σ 1 σ 2 )(v) def = σ 1 (v) for v ∈ V 1 , σ 2 (v) for v ∈ V 2 .
Composition for homogeneous tag systems, i.e., tag systems over the same tag structure, is therefore defined as follows.

Definition 1 (Composition [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]). The composition P of two tag systems P 1 = (V 1 , T , Σ 1 ) and P 2 = (V 2 , T , Σ 2 ), written P = P 1 P 2 , is the tag system

P = (V 1 ∪ V 2 , T , Σ 1 ∧ Σ 2 )
, where

Σ 1 ∧ Σ 2 def = {σ 1 σ 2 : σ 1 ∈ Σ 1 ∧ σ 2 ∈ Σ 2 ∧ σ 1 σ 2 }.
An alternative definition uses the inverse of the restriction operator σ| W , or inverse projection, to equalize the variables of the behaviors. If σ 1 is a behavior on variables V 1 , its inverse projection to the set

V = V 1 ∪ V 2 is the set of behaviors σ ∈ Σ(V ) whose restriction is σ 1 : proj -1 V (σ 1 ) = {σ ∈ Σ(V, T ) : σ| V1 = σ 1 }.
Inverse projection is naturally extended to sets of behaviors. Hence, Σ 1 ∧ Σ 2 can also be written as

Σ 1 ∧ Σ 2 def = proj -1 V1∪V2 (Σ 1 ) ∩ proj -1 V1∪V2 (Σ 2 )
, which makes the intersection operator involved with composition explicit. Heterogeneous Composition. When the tag systems have different tag structures, we must equalize also the set of tags. This is done by mapping the tag structures onto a third tag structure that functions as a common domain. The mappings are called tag morphisms and must preserve the order. Definition 2 (Tag morphism [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]). Let T and T be two tag structures. A tag morphism from T to T is a total map ρ:T → T such that ∀τ 1 , τ 2 ∈ T , τ 1 ≤ τ 2 ⇒ ρ(τ 1 ) ≤ ρ(τ 2 ).

Here, the tag orders must be taken on the respective domains. Using tag morphisms, we can turn a T -behavior

σ ∈ V → (N → (T × D)) into a T -behavior σ ρ ∈ V → (N → (T × D)
) by simply replacing all tags τ in σ with the image ρ(τ ). Abusing the function composition operator •, we may alternatively refer to σ ρ as σ • ρ.

Unification of heterogeneous behaviors can be done on the common tag structure. Let P 1 = (V 1 , T 1 , Σ 1 ) and P 2 = (V 2 , T 2 , Σ 2 ) be two tag systems, and let ρ 1 : T 1 → T and ρ 2 :T 2 → T be two tag morphisms into a tag structure T . We say that two behaviors σ 1 ∈ Σ 1 and σ 2 ∈ Σ 2 are unifiable in the heterogeneous sense, written σ 1 ρ1 ρ2 σ 2 , if and only if (σ 1 • ρ 1 ) (σ 2 • ρ 2 ). When σ 1 and σ 2 are unifiable, we may construct the unified behavior σ over T as usual, by considering the corresponding behaviors in

T σ = (σ 1 • ρ 1 ) (σ 2 • ρ 2 ),
and hence build the composed tag system P = (V, T , Σ) over the common tag structure T , where

Σ def = {(σ 1 • ρ 1 ) (σ 2 • ρ 2 ) : σ 1 ∈ Σ 1 ∧ σ 2 ∈ Σ 2 ∧ σ 1 ρ1 ρ2 σ 2 }.
It is convenient, however, to retain some information of the original tag structures in the composition, since they are often referred to in the heterogeneous composition, as we will see in the sequel. To do so, we construct the composition over the fibered product [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]

T 1 × ρ1 ρ2 T 2 = (T 1 × ρ1 ρ2 T 2 , ≤)
of the original tag structures, extending the order component-wise:

(τ 1 , τ 2 ) ≤ (τ 1 , τ 2 ) ⇐⇒ τ 1 ≤ τ 1 ∧ τ 2 ≤ τ 2 .
where

T 1 × ρ1 ρ2 T 2 = {(τ 1 , τ 2 ) ∈ T 1 ×T 2 : ρ 1 (τ 1 ) = ρ 2 (τ 2 )}.
We denote by σ| V1,T1 the restriction of σ to the variables in V 1 and to the element T 1 of the fibered product. 1 With this notion, we can define the heterogeneous composition.

Definition 3 (Heterogeneous composition [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]). Let P 1 = (V 1 , T 1 , Σ 1 ) and P 2 = (V 2 , T 2 , Σ 2 ) be tag systems and let ρ 1 : T 1 → T and ρ 2 : T 2 → T be tag morphisms. The heterogeneous composition P = P 1 ρ1 ρ2 P 2 is the tag system

P = (V 1 ∪ V 2 , T 1 × ρ1 ρ2 T 2 , Σ 1 ∧ ρ1 ρ2 Σ 2 ),
where

Σ 1 ∧ ρ1 ρ2 Σ 2 def = {σ ∈ Σ(V, T 1 × ρ1 ρ2 T 2 ) : σ| V1,T1 ∈ Σ 1 ∧ σ| V2,T2 ∈ Σ 2 }.

III. TAG MACHINES

Tag machines [START_REF] Benveniste | Tag machines[END_REF] (TM) have been introduced to represent tag systems in a homogeneous context. Since our aim is to provide an operational representation for heterogeneous systems, we extend the TM formalism to encompass the heterogeneous context.

In order to construct behaviors, the transitions of a tag machine must be able to increment time, i.e., to update the tags of the events. An operation of tag concatenation on a tag structure is used to accomplish this. Definition 4 (Algebraic tag structure [START_REF] Benveniste | Tag machines[END_REF]). An algebraic tag structure is a tag structure T = (T, ≤, •) where • is a binary operation on T called concatenation, such that:

i) (T, •) is a monoid with identity element î ii) ∀τ 1 , τ 1 , τ 2 , τ 2 ∈ T : τ 1 ≤ τ 1 , τ 2 ≤ τ 2 ⇒ τ 1 • τ 2 ≤ τ 1 • τ 2 iii) ∃ ∈ T : ∀τ ∈ T : ≤ τ ∧ • τ = τ • = .
We will organize tags in tag vectors τ = (τ v1 , . . . , τ vn ), where n is the number of variables in V . During transitions, tag vectors evolve according to a matrix µ : V × V → T called a tag piece [START_REF] Benveniste | Tag machines[END_REF]. Given a tag vector τ and a tag piece µ, the new tag vector is τ µ = τ • µ given by

τ v µ def = max u∈V (τ u • µ(u, v)),
where the maximum is taken with respect to the tag ordering.

In practice, one concatenates each element of the tag vector with the tags on a column of µ, and then takes the largest value; thus the new value of any tag may depend on the tag increments on the events of the other variables. As the order is partial, the maximum may not exist, in which case the operation is not defined.

Intuitively, a tag piece µ represents increments in all variable tags over a transition and provides a way to operationally renew them. To represent also changes in variable values, µ can be labeled with a partial assignment ν : V → D, which assigns new values to the variables. We say that a labeled tag piece µ has an event for all variables for which ν is defined, and denote by dom(ν) the domain of ν. In the following, we assume that tag pieces are always labeled and implicitly associate a labeling function ν to a tag piece µ.

Example 1. The algebraic tag structure (N ∪ {-∞}, ≤, +) can be used to capture logical time by structuring tag pieces µ so that they represent an integer increment of 1 as follows:

µ(u, v) =    0 if u = v and ν is not defined on v -∞ if u = v and ν is not defined on v 1 if ν is defined on v .
The least element = -∞ is used to cancel the contribution of an entry in the tag vector. With these definitions, every time a new value must be assigned to a variable (i.e., when ν(v) is defined), the tag is also incremented by 1. Otherwise, the tag is left unchanged and no new event is generated. For instance, 1 4 ]. The tag of the second variable is increased by 1 since the tag piece has an event for it.

[ 1 3 ]• 0 1 1 = [
Likewise, (R + ∪ {-∞}, ≤, +) can capture physical time.

A tag machine M is a finite automaton where transitions are marked by labeled tag pieces, or simply labels. Our definition below differs from that proposed by Benveniste et al. [START_REF] Benveniste | Tag machines[END_REF] for certain simplifications and for the addition of a set of accepting states. Definition 5. A tag machine M is a tuple (V, T , S, s 0 , F, L, E), where:

• V is a set of variables, • T is an algebraic tag structure,
• S is a finite set of states and s 0 ∈ S is the initial state, • F ⊆ S is a set of accepting states, • L is a set of labeled tag pieces defined on V and T ,

• E ⊆ S × L × S is the transition relation.
A run r of the tag machine is a sequence of states and transitions r :

s 0 µ0 -→ s 1 µ1 -→ s 2 . . . s m-1 µm-1 ----→ s m such that s m ∈ F and for all i, 1 ≤ i ≤ m, (s i-1 , µ i-1 , s i ) ∈ E.
Intuitively, a tag machine is used to construct a behavior by following its labeled transitions over a run, and applying the tag pieces sequentially to an initial vector of tags. A new event is added to the behavior whenever a new value is assigned by the label function ν i . In order to formalize the language of a tag machine, we must keep track of both the tags and the number of events that have occurred for each variable. Thus, for every state s i along run r, we define a tag vector τ i computed by accumulating the tag pieces:

τ i+1 = τ i • µ i ,
and an index vector k i computed by updating the event index at every new event:

k i+1 (v) = k i (v) if v ∈ dom(ν i ) k i (v) + 1 if v ∈ dom(ν i ) .
For state s 0 , the tag vector is initialized to the identity element î, while the index vector is initialized to 0. The behavior σ(r)2 of a run r is constructed incrementally by starting from an empty behavior σ 0 and computing:

σ i+1 (v, k) =    σ i (v, k) if v ∈ dom(ν i ) σ i (v, k) if v ∈ dom(ν i ) ∧ k < k i (v) ( τ i+1 (v), ν i (v)) if v ∈ dom(ν i ) ∧ k = k i (v)
A run r of M is valid if the concatenation is always defined along the run, and if s m ∈ F . The language L(M ) of M is given by the behaviors of all its valid runs.

A. Composition of Tag Machines

Tag machines are composed in parallel by taking a form of product between their structures. Synchronization occurs by sharing variables. In particular, over every transition, the tag machines involved in the composition must agree on the tag increment and on the value of the shared variables.

We first examine the composition of homogeneous tag machines, by adapting the original definition [START_REF] Benveniste | Tag machines[END_REF]. Consider two tag machines

M 1 = (V 1 , T , S 1 , s 01 , F 1 , L 1 , E 1 ) and M 2 = (V 2 , T , S 2 , s 02 , F 2 , L 2 , E 2 )
defined over the same tag structure T . Two labeled tag pieces µ 1 ∈ L 1 and µ 2 ∈ L 2 are unifiable, written µ 1 µ 2 , if and only if they are the same on the shared variables. That is, if we denote the set of shared variables with

W = V 1 ∩ V 2 , then for all pairs (w, v) ∈ W × W , µ 1 (w, v) = µ 2 (w, v), ν 1 (v) = ν 2 (v).
When unifiable, their unification µ = µ 1 µ 2 is given by

µ(w, v) =    µ 1 (w, v) if (w, v) ∈ V 1 × V 1 µ 2 (w, v) if (w, v) ∈ V 2 × V 2 otherwise , ν(v) = ν 1 (v) if v ∈ V 1 ν 2 (v) if v ∈ V 2 .
Homogeneous composition can then be defined as follows:

Definition 6 (Homogeneous composition). The parallel composition of homogeneous machines M 1 and M 2 is the machine

M = M 1 M 2 = (V, T , S, s 0 , F, L, E) such that • V = V 1 ∪ V 2 , • S = S 1 × S 2 , s 0 = (s 01 , s 02 ), F = F 1 × F 2 , • L = {µ 1 µ 2 : µ 1 ∈ L 1 ∧ µ 2 ∈ L 2 ∧ µ 1 µ 2 }, • E = {((s 1 , s 2 ), µ 1 µ 2 , (s 1 , s 2 )) : (s 1 , µ 1 , s 1 ) ∈ E 1 ∧ (s 2 , µ 2 , s 2 ) ∈ E 2 ∧ µ 1 µ 2 }. Definition 7. A tag morphism ρ : T → T is algebraic if ρ(î T ) = îT , ρ( T ) = T , and ρ(τ 1 • τ 2 ) = ρ(τ 1 ) • ρ(τ 2 ) for all τ 1 , τ 2 ∈ T .
The newly-composed TM will be defined on a unified tag structure and a unified label set. Referring to the previous notation, two tag pieces µ 1 and µ 2 are unifiable under morphisms ρ 1 and ρ 2 , written µ 1 ρ1 ρ2 µ 2 , whenever for all pairs (w, v) ∈ W × W ,

ρ 1 (µ 1 (w, v)) = ρ 2 (µ 2 (w, v)), ν 1 (v) = ν 2 (v).
When unifiable, their unification µ = µ 1 ρ1 ρ2 µ 2 defined over the tag structure T 1 × ρ1 ρ2 T 2 is a set of pieces given by

µ(w, v) =                (µ 1 (w, v), µ 2 (w, v)) if (w, v) ∈ W × W (µ 1 (w, v), τ 2 ) if w ∈ V 1 , v ∈ V 1 \ V 2 (µ 1 (w, v), τ 2 ) if w ∈ V 1 \ V 2 , v ∈ V 1 (τ 1 , µ 2 (w, v)) if w ∈ V 2 \ V 1 , v ∈ V 2 (τ 1 , µ 2 (w, v)) if w ∈ V 2 , v ∈ V 2 \ V 1 ( T1 , T2 ) otherwise where τ 2 ∈ T 2 is such that ρ 2 (τ 2 ) = ρ 1 (µ 1 (w, v))
, and similarly τ 1 ∈ T 1 is such that ρ 1 (τ 1 ) = ρ 2 (µ 2 (w, v)). The labeling function is the same as in the homogeneous case:

ν(v) = ν 1 (v) if v ∈ V 1 ν 2 (v) if v ∈ V 2 .
The composition M = M 1 ρ1 ρ2 M 2 of heterogeneous tag machines can then be defined exactly as in Definition 6, having replaced the operators for the unification of the tag pieces on the transition with the heterogeneous ones.

Definition 8 (Heterogeneous composition). The parallel composition of heterogeneous machines M 1 and M 2 under morphisms ρ 1 and ρ 2 is the machine

M = M 1 ρ1 ρ2 M 2 = (V, T 1 × ρ1 ρ2 T 2 , S, s 0 , F, L, E) such that • V = V 1 ∪ V 2 , • S = S 1 × S 2 , s 0 = (s 01 , s 02 ), F = F 1 × F 2 , • L = {µ 1 ρ1 ρ2 µ 2 : µ 1 ∈ L 1 ∧µ 2 ∈ L 2 ∧µ 1 ρ1 ρ2 µ 2 }, • E = {((s 1 , s 2 ), µ 1 ρ1 ρ2 µ 2 , (s 1 , s 2 )) : (s 1 , µ 1 , s 1 ) ∈ E 1 ∧ (s 2 , µ 2 , s 2 ) ∈ E 2 ∧ µ 1 ρ1 ρ2 µ 2 }

IV. INTEROPERABLE TAG MACHINES AND COMPOSITION SOUNDNESS

Ideally, we would like there to be a direct correspondence between tag systems and tag machines. So, if Σ i is the language of machine M i , and if Σ is the language of the composition M = M 1 ρ1 ρ2 M 2 , we expect that every behavior of Σ be obtained by composing some pair of (a)

(b) (c) Figure 1. Tag machines accepting (a) Σ 1 (b) Σ 2 (c)Σ 1 ∧ Σ 2
behaviors from Σ i . When this is the case, we say that composition is sound. Example 2 shows that this property generally does not hold even for homogeneous systems.

Example 2. We consider two sets of behaviors Σ 1 and Σ 2 defined on two sets, V 1 = {x, y} and V 2 = {x, z} respectively, of variables with values in D = {true}. Since D is a singleton set, we shall omit mentioning the variable value in the rest of the example. These behavioral sets are expressed formally as follows. Let σ i ∈ Σ i and enum σi (v i ) be the total number of events on variable v i ∈ V i in behavior σ i where i ∈ {1, 2} and let k ≥ 1:

Σ 1 :    σ 1 (x, k) = 2 * k -1 σ 1 (y, k) = k enum σ1 (y) = 2 * enum σ1 (x) -1 Σ 2 :    σ 2 (x, k) = 2 * k σ 2 (z, k) = k enum σ1 (z) = 2 * enum σ1 (x)
Let reaction be a maximal set of events with identical tags in a behavior, c.f. [START_REF] Benveniste | Tag machines[END_REF], these behavioral sets can then be organized in terms of successive reactions as follows:

Σ 1 :
x : 1 3 5 7 9 . . . y : 1 2 3 4 5 6 7 8 9 10 . . .

Σ 2 :
x : 2 4 6 8 10 . . . z : 1 2 3 4 5 6 7 8 9 10 . . . We use the algebraic tag structure (N ∪ { }, , +) and the tag piece structure described in Example 1 to model the behaviors in Σ i as TMs, shown in Fig. 1, where def = -∞, the row and column designation orders are (x, y) in Fig. 1(a), (x, z) in Fig. 1(b) and (x, y, z) in Fig. 1(c). The initial states are double-circled and the accepting states are shaded.

Tagging the shared variable x can depend on tagging non-shared variables y or z even though there is no real dependence between their tags. Going from s 1 0 to s 1 1 , the TM 1(a) tags x and y simultaneously and equally. It then can go back to s 1 0 , tagging only y and subsequently repeating the tagging cycle at this state. The TM 1(b) instead tags only z initially and goes to s 2 2 . It then tags both x and z at the same time and goes to s 2 1 where it again tags only z before returning to s 2 2 . It is easy to verify that TM 1(a) and 1(b) accept the behavioral sets Σ 1 and Σ 2 respectively. When composing them, the composed TM is expected not to accept any behavior since Σ 1 ∧Σ 2 = ∅. Its set of accepted behavior is, however, not empty as shown in Fig. 1(c). This is because TM 1(a) can stay silent while TM 1(b) is tagging z. The two TMs then synchronize and tag all variables simultaneously, after which they can go on tagging their own internal variable.

We remark that the fact that TM composition is not sound has not been observed in Benveniste et.al. [START_REF] Benveniste | Tag machines[END_REF]; clearly it also holds for heterogeneous composition. The consequence is that the operational model overestimates the behaviors of composition, therefore building an abstraction. This may or may not be a problem, depending on what is done with the models. For instance, verification of safety properties would be correct, albeit less precise. On the other hand, the emergence of unexpected behaviors may adversely affect the design process, where a refinement rather than an abstraction would instead be more appropriate. It is therefore useful to look for conditions that guarantee soundness. In our example, the dependency effects of tagging non-shared variables on others, especially shared ones, are shown to be the critical factor. The cause lies in the fact that in the applications of tag pieces, the max tag evaluations for a shared variable can be different even though the pieces are unifiable. It is therefore desirable to eliminate such effects to make the composition sound. To this end, we propose an interoperability condition to prevent TMs from producing such effects.

The intuition behind TM interoperability is that tagging shared variables should not depend on tagging non-shared variables. A set V ⊆ V is locally independent in M = (V, T , S, s 0 , F, L, E), written lind(M, V ), if tagging v ∈ V depends only on tagging other variables also in V . If we define the predicate lind(µ, V )

def = (∀w ∈ V \ V , ∀v ∈ V : µ(w, v) = ), then lind(M, V ) def = (∀(s, µ, s ) ∈ E : lind(µ, V )).
The interoperability between M 1 and M 2 is formally defined as follows.

Definition 9. Two TMs

M i = (V i , T i , S i , s 0i , F i , L i , E i ),
for i ∈ {1, 2}, are said to be interoperable, written M 1 M 2 , if their shared variables are locally independent in M i :

M 1 M 2 def = lind(M 1 , V 1 ∩ V 2 ) ∧ lind(M 2 , V 1 ∩ V 2 )
Interoperability behaves well under multiple composition. Lemma 1. Let M 1 , M 2 , . . . M n be n pair-wise interoperable TMs, where n ≥ 2. If M is the composition of M 1 , M 2 , . . . M n-1 , then M M n .

Proof: We prove the theorem by induction. The base case n = 2 is trivial, so assume now the statement holds for k = n -1, we prove that it also holds for k = n. Let V i , µ i be the variable set and label of M i , µ the unification of µ 1 , µ 2 . . . , µ n-1 , and

V = V 1 ∪ V 2 . . . ∪ V n-1 , we see that lind(µ, V ∩ V n ) holds. Indeed, if w ∈ V \ (V ∩ V n ), then w ∈ V j \ (V ∩ V n ) and hence w ∈ V j \ V n for some j. Likewise, if v ∈ V ∩ V n , then v ∈ V r ∩ V n for some r. Thus, if j = r then µ(w, v) = T because M r
M n implies µ r (w, v) = Tr . If instead j = r, the result remains the same because the composition on labels puts T whenever w and v are not in the same variable set. To prove that lind(µ n , V ∩ V n ) holds, we consider w ∈ V n \ (V ∩ V n ) and v ∈ V n ∩ V r for some r. The former implies w ∈ V n and w / ∈ V j for all j. This together with M n M r implies µ n (w, v) = T .

Example 3. We use the algebraic tag structure in Example 2 but restructure the tag pieces so that they can represent any integer time increment n ∈ N.

µ uv =    0 if u = v
and µ has no event for v n if u = v and µ has an event for v otherwise Interoperable TMs representing Σ i are depicted in Fig. 2(a) and 2(b). Tagging the shared interface x is now made locally independent in both machines, hence they can be composed interoperably. The composed TM is shown in Fig. 2(c) where no behavior can be accepted since the accepting state is not reachable from the initial state. This is because TM 2(a) has to stutter in s 1 0 while TM 2(b) tags its internal variable and moves to s 2 2 . The two TMs then have to stutter there forever since only the stuttering labels 0 0 are unifiable.

Example 4. We consider a simplified version of the water controlling system proposed by Benvenuti et al. [START_REF] Benvenuti | A contract-based formalism for the specification of heterogeneous systems[END_REF]. It consists of two components: a water tank and a water level controller, connected in a closed-loop fashion, c.f. Fig. 3. We assume that the water level x(t) is changed linearly as follows:

x(t) def = ∆ t * (f i -f o ) when command is Open H -∆ t * f o when command is Close (1)
where f i and f o denote the constant inlet and outlet flow, respectively, H denotes the height when the tank is full of water and ∆ t denotes the time elapsed since t 0 at which the tank reaches the maximum/minimum water level H, i.e. ∆ t = t -t 0 . Let P 1 = (V 1 , T 1 , Σ 1 ) and P 2 = (V 2 , T 2 , Σ 2 ) be two tag systems representing the tank and the water controller, respectively, where

T 1 = (R + ∪ { 1 }, +), T 2 = (N ∪ { 2 }, +), 1 = 2 = -∞, and V 1 = V 2 = {cmd, x}.
Variable cmd denotes the command values, which can be Open (op) or Close (cl), and variable x denotes the water level, which is of positive real type, i.e. D cmd = {op, cl} and

D x = R + . Assume that f i = 2, f o = 1, H = 1,
we model in this example a linear water level evolution of a water controlling system. The tank component shown in Fig. 4(a) depicts the water level linear evolution as specified in 1.

Upon knowing of the tank emptiness/fullness, the controller component in Fig. 4(b) will issue an Open/Close command. Intuitively, the controller behaviors ensure that controlling commands are always issued timely (i.e., Open when the tank is empty and Close when it is full), no matter how the water level evolves, while the tank behaviors accept untimely controlling commands and allow water spillages or shortages, given that the water level evolves linearly.

For the sake of simplicity, the events described by the tank component are timestamped periodically every 0.5 time unit. While the tank system uses physical time to stamp its behaviours, the controller system instead timestamps its events logically, described by the integer tag set N. For the Interoperable TM representing (a) the tank's behaviors (b) controller's behaviors (c) the tank-controller composition's behaviors sake of expressiveness, some of the labeled tag pieces can be represented symbolically. For example, to capture any event of variable x happening at a specific time point, we label with the tag piece capturing that time point expressions such as x ∈ D x , meaning that in such an event x can take any value in its domain. Since the tank and the controller capture different behaviors, composing them is only possible under the presence of morphisms such as ρ 1 : T 1 → T 1 and ρ 2 : T 2 → T 1 given by ρ 1 (τ 1 ) = τ 1 , ρ 2 (τ 2 ) = 0.5 * τ 2 . Fig. 4(c) shows their composition, where accepted behaviors ensure timely controlling commands and linear water evolution.

The following theorem shows that composition of interoperable TMs is sound. Theorem 1. For any behavior σ accepted by M 1 ρ1 ρ2 M 2 where M 1 M 2 , there exist behaviors σ 1 , σ 2 accepted by M 1 , M 2 such that σ can be obtained by composing σ 1 and σ 2 , i.e. Σ ⊆ Σ 1 ∧ ρ1 ρ2 Σ 2 .

Proof: Let r : s 0 µ1 -→ s 1 . . . µn --→ s n be a valid run in M 1 ρ1 ρ2 M 2 where s k = (s k1 , s k2 ) for 0 ≤ k ≤ n. There exists a valid run r i :

s 0i µ1i --→ s 1i . . . µni --→ s in in M i , for i ∈ {1, 2}
, where µ k1 ρ1 ρ2 µ k2 and µ k = µ k1 ρ1 ρ2 µ k2 . Inductively for tag vectors τ k / τ ki obtained at states

s k /s ki in (a) (b) Figure 5. Interoperable TMs accepting Σ 1 run r/r i we prove that first, ρ 1 (τ v k1 ) = ρ 2 (τ v k2 ) and second, τ w k ∈ T 1 × ρ1 ρ2 T 2 and τ k | V1 = τ k1 and τ k | V2 = τ k2 , where v ∈ V 1 ∩ V 2 and w ∈ V 1 ∪ V 2 . Let v ∈ V 1 ∩ V 2 , v i ∈ V i \ (V 1 ∩ V 2
) and µ vw denote µ(v, w). The base case k = 0 is trivial since τ v 0i = îTi by definition. Assuming the statements hold for any 0 ≤ k ≤ n -1, we prove that it also holds for k = n using the following fact for the first:

ρ i (τ v ni ) = ρ i (max(τ v (n-1)i • µ v v ni , τ vi (n-1)i • µ viv ni )) = max(ρ i (τ v (n-1)i ) • ρ i (µ v v ni ), ρ i (τ vi (n-1)i ) • ρ i (µ viv ni )
) and the interoperability condition and the inductive hypotheses for the second, e.g.

τ v n = max(τ v n-1 • µ v v n , τ v1 n-1 • µ v1v n , τ v2 n-1 • µ v2v n ) = max((τ v (n-1)1 • µ v v n1 , τ v (n-1)2 • µ v v n2 ))
and

ρ 1 (τ v (n-1)1 • µ v v n1 ) = ρ 2 (τ v (n-1)2 • µ v v n2
).

V. SELF-SYNCHRONIZING TAG MACHINES AND COMPOSITION COMPLETENESS

To establish the correspondence between tag systems and TMs, TM compositions need to be not only sound but also complete. Composition completeness requires two unifiable behaviors to always be operationally composed, and Example 5 below shows that this property generally does not hold even for homogeneous systems. The reason of this incompleteness is due to the TM non-unique behavioral representations. Indeed, different TM runs can represent the same behavior, which in turn causes the operational composition on two behaviors to sometimes become impossible (while the denotational one may be possible) when their representations contain non-unifiable labels.

Example 5. Fig. 5 shows two different TMs representing the same set of behaviors as Σ 1 , yet their composition does not accept Σ 1 . This is because the TMs cannot synchronize on updating their variable tags.

As demonstrated in Example 5, the TM composition represents incompletely the tag system composition when M i fails to include all representations of some behavior. Therefore, it is a natural condition for completeness that M i be self-synchronizing. The notion of self-synchronization for homogeneous composition [START_REF] Benveniste | Tag machines[END_REF] requires the language of M = (V, T , S, s 0 , F, L, E) to be ∼-closed, where ∼ is a binary relation s.t. ∀ω, ω ∈ Σ(V, T ) : ω ∼ ω ⇔ σ(ω) = σ(ω ).

In order to make machine M i self-synchronize, all possible runs of any behavior of M i must be added to the machine. In order for the TM semantics to remain unaffected, any sub-run's behavior should be excluded from the machine language. This, however, is not guaranteed in [START_REF] Benveniste | Tag machines[END_REF] because TMs there do not contain accepting states. Our TM definition (Def. 5) cares for such a need and thus can preserve the TM semantics under the self-synchronizing operation.

Self-synchronization is however not sufficient to guarantee completeness of composition, as two unifiable behaviors do not always have unifiable representations, which in turn is caused by the choice of tag structures and morphisms. We recall that events of a variable v are indexed into a sequence of (v, 1, τ 1 , d 1 ), (v, 2, τ 2 , d 2 ) . . . , (v, n, τ n , d n ) where τ 1 ≤ τ 2 . . . ≤ τ n . If the tag increments between two successive events can always be mapped into the same increment under morphisms ρ i , then completeness of composition is ensured by the following theorem.

Theorem 2. For behaviors σ 1 , σ 2 accepted by M 1 , M 2 such that σ 1 ρ1 ρ2 σ 2 where: i) M 1 and M 2 are self-synchronizing and M 1 M 2 , ii) ∀i ∈ {1, 2}, ∀(v, j, τ ji , d ji ) ∈ σ i :

∃δ ji ∈ T i : τ ji = τ (j-1)i • δ ji where τ 0i def = îTi , iii) ∀i ∈ {1, 2}, ∀δ i ∈ T i , ∀(τ 1 , τ 2 ), (τ 1 , τ 2 ) ∈ T 1 × ρ1 ρ2 T 2 : τ i = τ i •δ i ⇒ ∃(δ 1 , δ 2 ) ∈ T 1 × ρ1 ρ2 T 2 : τ 3-i = τ 3-i •δ 3-i if a behavior σ ∈ Σ(V 1 ∪ V 2 , T 1 × ρ1 ρ2 T 2 ) is such that σ| V1,T1 = σ 1 σ| V2,T2 = σ 2 , then σ is also accepted by M 1 ρ1 ρ2 M 2 , i.e. Σ 1 ∧ ρ1 ρ2 Σ 2 ⊆ Σ.
Proof: Let n i be the greatest number of events of all variables in σ i , then there exists a sequence of labels ω i = µ 1i µ 2i . . . µ nii where the diagonal entries of µ ji are δ ji specified in Theorem 2. ii and the entries outside the diagonal are all Ti . At the end, we pad ω i with max(n 1 , n 2 )-n i stuttering labels. Since σ(ω i ) = σ i , self-synchronization ensures the existence of a valid run r i in M i over ω i . By construction µ j1 ρ1 ρ2 µ j2 , and this implies that there exists a run r in M 1 ρ1 ρ2 M 2 over the following sequence of labels ω = (µ 11 ρ1 ρ2 µ 12 ) . . . (µ max(n1,n2)1 ρ1 ρ2 µ max(n1,n2 Being self-synchronizing is, however, not a trivial property for TMs in general and efficient methods of checking and providing this property is part of our on-going work.

VI. IMPLEMENTATION AND EVALUATION

In this section, we demonstrate the application of TM composition in dealing with the problem of heterogeneity in a practical use case of an automotive system.

A. Tag Machine Simulator

We have implemented a prototype tool to simulate the heterogeneous TM composition under morphisms. Our simulator, written in approximately 5000 lines of C++ code, supports a high level script language to specify tag machines. Each TM is described as a module consisting of a set of constraints on the declared variables. In particular, a module must contain declarations about the machine tag structure (TAGSTRUCT), the state (MVAR) and label (MLABEL) variable. Declarations about the machine variables (MVAR), initial state (INIT) and transitions (EDGE) are optional. A morphism associated with a machine can be declared likewise. Fig. 6 shows an example of our script language.

The inputs to our simulator are pairs of TMs and morphisms under which the TMs can be composed. At every step, our simulator explores all composition possibilities and provides the user with a set of simulation choices which can be carried out randomly or interactively.

B. An Automotive Example

We consider a simplified version of the automotive engine control model proposed by Balluchi et al. [START_REF] Balluchi | Hybrid control for automotive engine management: The cut-off case[END_REF]. It consists of a sub-model capturing the piston sequential behavior and another capturing the power-train behavior under a cut-off control policy. The goal of the control policy is to reduce the unpleasant oscillations when the driver releases the gas pedal and requests no torque to the engine. The piston model is naturally expressed by a finite state machine while the power-train model can be represented by a continuous time equation. Thus, in order to understand the behavior of the car, it is important for designers to be able to compose these heterogeneous models.

A piston abstractly cycles through four phases: 1) the intake (I) phase during which the piston loads the air-fuel

Figure 7. The automotive engine control model consisting of (a) a general view (b) pistons (c) a bang-bang controller, (d) the power-train mix q ∈ R + ; 2) the compression (C) phase in which the loaded mix is compressed; 3) the expansion (E) phase in which the compressed mix is combusted, producing the spark ignition; 4) the exhaust (H) phase during which the piston expels combustion exhaust gases. We assume the torque evolution u(t) to be a piece-wise constant function which is zero everywhere except in the E-phase when the spark ignition is set, i.e., u(t) = G * q and u(t) = 0 otherwise, where G is the mix-to-torque gain.

The continuous time power-train behavior is modeled by the following linear system:

.

ζ = A p ζ + b p u . φ c = ω c
where ζ = [α e , ω c , ω p ] represents the axle torsion angle, the crankshaft revolution speed and the wheel revolution speed, and φ c represents the crankshaft angle.

In this paper we model the bang-bang control law [START_REF] Balluchi | Hybrid control for automotive engine management: The cut-off case[END_REF] where the fuel injection is cut when v T x ≥ 0. The reduced state x = [x 1 , x 2 ] T represents the system's oscillation component and is obtained by applying the state transformation .

x(t) = Ax(t)+bu(t) where A = λ -µ µ λ and λ±jµ are the conjugate complex poles of A p . The oscillation acceleration can then be computed based on x as a(t) = cx(t). The starting point of the cut-off control horizon is the time at which all the loaded cylinders' potential torques are at the steady value M = G * q 0 .

The piston model needs only information about the sequencing of events, while the power-train model requires the exact timing of events. Thus we can use T 1 = (N ∪ { 1 }, +) and T 2 = (R + ∪ { 2 }, +) where 1 = 2 = -∞, to model them. Fig. 7(b) shows the piston behavior where the transitions of the automaton occur when a piston reaches the bottom or top dead point, i.e. when the flag rot is set. Fig. 7(c) and 7(d) describe the bang-bang control policy and the evolution of the power-train, respectively. We have approximated the power-train using the forward integration Euler method with a step of δ. The state variables are fixed as follows [START_REF] Balluchi | Hybrid control for automotive engine management: The cut-off case[END_REF]:

A p =   0

C. Evaluation

We have described the cut-off problem using our prototype TM-simulator and performed simulations of 2000 steps to evaluate the effect of the cut-off control on the oscillation acceleration. We present here the results of two such simulations on the above set of parameters and under the presence of morphisms such as ρ i : T i → T 2 given by ρ 1 (τ 1 ) = δ * τ 1 and ρ 2 (τ 2 ) = τ 2 .

Consistent with the previous result [START_REF] Balluchi | Hybrid control for automotive engine management: The cut-off case[END_REF], Fig. 8 shows that better acceleration peaks and driving comfort are obtained when cut-off control is enforced. This consistent result can assist automotive engineers and designers in estimating the impact of the control implementation on the engine performance, thereby justifying and selecting suitable system parameter values to obtain a desirable performance.

Another important advantage offered by the heterogeneity methodology is in terms of component modeling. While the components in [START_REF] Balluchi | Hybrid control for automotive engine management: The cut-off case[END_REF] had to be modeled in the same domain in order to solve the cut-off control problem, they can now be expressed in their natural domain. The component interaction can then be precisely quantified and modeled by means of morphisms. This advantage becomes much more crucial when designers have to deal with large and complex systems.

VII. CONCLUSION

We have developed an operational formalism for representing heterogeneous tag systems. To this end, we have extended tag machines, which were introduced to represent only homogeneous tag systems, to the heterogeneous context. Our heterogeneous TM formalism is able to operationally represent heterogeneous tag systems.

A natural concern is whether composition of TMs can soundly and completely represent the that of tag systems. The concern can be addressed under certain conditions such as interoperability and self-synchronization. Checking for self-synchronization in general, however, is a non-trivial property for which effective checking procedures are an important part of our future work.

Using an industrial case study and our prototype tool, we have demonstrated that TM modeling is useful in practice. This is especially important in systems consisting of components with differing natural domains, as in our case study. Contrary to previous work, our heterogeneous approach allows components to be modeled in their natural domain.

In the future, we aim at several extensions to our simulator. In particular, we plan to integrate it with a model checker and SMT solver, in order to enable automated compositional verification of heterogeneous systems and to support their contract-based design. Since our simulator is based on a formal representation, development and implementation of formal verification techniques is a natural extension which we will consider.

Figure 2 .Figure 3 .

 23 Figure 2. Interoperable TM accepting (a) Σ 1 (b) Σ 2 (c)Σ 1 ∧ Σ 2

) 2 )

 2 where σ(r)| V1∩V2 = σ| V1∩V2 since σ(r)| V1,T1 = σ 1 and σ(r)| V2,T2 = σ 2 , σ(r)| V1\V2 = σ| V1\V2 and σ(r)| V2\V1 = σ| V2\V1 because of condition iii, thus σ(r) = σ.

Figure 6 .

 6 Figure 6. High-level description of (a) a piston TM (b) its morphism

  0379945 -0.00257 , M = 12.41, δ = 0.001181.

Figure 8 .

 8 Figure 8. The evolution of x(t) and a(t) without and with control

The restriction to T 1 can be accomplished using a tag morphism π :T 1 × ρ 1 ρ

T 2 → T 1 with π((τ 1 , τ 2 )) = τ 1 .

We sometimes refer to σ(r) as σ(ω) where ω = µ 0 µ 1 . . . µ m-1Heterogeneous tag machines can be composed if there exists a pair of morphisms which map the tag structures T 1 and T 2 to a common tag structure T , preserving the concatenation operator. We refer to such morphisms as algebraic morphisms.


Uli Fahrenberg

Axel Legay

Generalized Quantitative Analysis of Metric Transition Systems

The formalism of metric transition systems, as introduced by de Alfaro, Faella and Stoelinga, is convenient for modeling systems and properties with quantitative information, such as probabilities or time. For a number of applications however, one needs other distances than the point-wise (and possibly discounted) linear and branching distances introduced by de Alfaro et.al. for analyzing quantitative behavior. In this paper, we show a vast generalization of the setting of de Alfaro et.al., to a framework where any of a large number of other useful distances can be applied. Concrete instantiations of our framework hence give e.g. limit-average, discounted-sum, or maximum-lead linear and branching distances; in each instantiation, properties similar to the ones of de Alfaro et.al. hold. In the end, we achieve a framework which is not only suitable for modeling different kinds of quantitative systems and properties, but also for analyzing these by using different application-determined ways of measuring quantitative behavior.

Introduction

During the last decade, formal verification has seen a trend towards modeling and analyzing systems which contain quantitative information. This is motivated by applications in real-time systems, hybrid systems, embedded systems and others. Quantitative information can thus be a variety of things: probabilities, time, tank pressure, energy intake, etc.

A number of quantitative models have hence been developed: probabilistic automata [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], stochastic process algebras [START_REF] Hillston | A Compositional Approach to Performance Modelling[END_REF], timed automata [START_REF] Alur | A theory of timed automata[END_REF], hybrid automata [START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF], continuous-time Markov chains [START_REF] Stewart | Introduction to the Numerical Solution of Markov Chains[END_REF], etc. Similarly, there is a number of specification formalisms for expressing quantitative properties: timed computation tree logic [START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF], probabilistic computation tree logic [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF], metric temporal logic [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF], stochastic continuous logic [START_REF] Aziz | Model-checking continous-time Markov chains[END_REF], etc.

Quantitative model checking, the verification of quantitative properties for quantitative systems, has also seen rapid development: for probabilistic systems in PRISM [START_REF] Kwiatkowska | Probabilistic symbolic model checking with PRISM: A hybrid approach[END_REF] and PEPA [START_REF] Gilmore | The PEPA workbench: A tool to support a process algebra-based approach to performance modelling[END_REF], for real-time systems in UPPAAL [START_REF] Larsen | UPPAAL in a nutshell[END_REF] and RED [START_REF] Wang | Symbolic model checking for distributed real-time systems[END_REF], and for hybrid systems in HyTech [START_REF] Henzinger | Hytech: A model checker for hybrid systems[END_REF] and SpaceEx [START_REF] Frehse | SpaceEx: Scalable verification of hybrid systems[END_REF], to name but a few.

Quantitative model checking has, however, a problem of robustness. When the answers to model checking problems are Boolean-either a system meets its specification or it does not-then small perturbations in the system's parameters may invalidate the result. This means that, from a model checking point of view, small, perhaps unimportant, deviations in quantities are indistinguishable from larger ones which may be critical.

As an example, Fig. 1 shows three simple timed-automata models of a train crossing, each modeling that once the gates are closed, some time will pass before the train arrives. Now if the specification of the system is "The gates have to be closed 60 seconds before the train arrives", then model A does satisfy the specification, and models B and C do not. What this does not tell us, however, is that model C is dangerously far away from the specification, whereas model B only violates it slightly (and may be acceptable from a practical point of view).

In order to address the robustness problem, one approach is to replace the Boolean yes-no answers of standard verification with distances. That is, the Boolean co-domain of model checking is replaced by the non-negative real numbers. In this setting, the Boolean true corresponds to a distance of zero and false to the non-zero numbers, so that quantitative model checking can now tell us not only that a specification is violated, but also how much it is violated, or how far the system is from corresponding to its specification.

In our example, and depending on precisely how one wishes to measure distances, the distance from A to our specification is 0, whereas the distances from B and C to the specification may be 2 and 59, respectively. Note that the precise interpretation of distance values will be application-dependent; but in any case, it is clear that C is much further away from the specification than B is.

The distance-based approach to quantitative verification has been developed the furthest for probabilistic and stochastic systems, perhaps akin to the fact that for these systems, the need for a truly quantitative verification is felt the most urgent. Panangaden and Desharnais et.al. have worked with distances for Markov processes e.g. in [START_REF] Bacci | On-the-fly exact computation of bisimilarity distances[END_REF][START_REF] Desharnais | Metrics for labelled Markov processes[END_REF][START_REF] Larsen | Taking it to the limit: Approximate reasoning for Markov processes[END_REF][START_REF] Panangaden | Labelled Markov Processes[END_REF], and van Breugel and Worrell et.al. have developed distances for probabilistic transition systems e.g. in [START_REF] Van Breugel | A behavioural pseudometric for probabilistic transition systems[END_REF][START_REF] Van Breugel | Approximating and computing behavioural distances in probabilistic transition systems[END_REF]. De Alfaro and Stoelinga et.al. have worked on distances between probabilistic systems and specifications in [START_REF] De Alfaro | Model checking discounted temporal properties[END_REF][START_REF] De Alfaro | Linear and branching metrics for quantitative transition systems[END_REF] and other papers.

For real-time and hybrid systems, some explicit work on distances is available in [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF][START_REF] Quesel | Crossing the bridge between similar games[END_REF]. Otherwise, distances have been used in approaches to robust verification [START_REF] Bouyer | Timed automata can always be made implementable[END_REF][START_REF] Larsen | Robust specification of real time components[END_REF], and Girard et.al. have developed a theory of approximate bisimulation for robust control [START_REF] Girard | Approximation metrics for discrete and continuous systems[END_REF][START_REF] Zheng | Bounded and unbounded safety verification using bisimulation metrics[END_REF].

Also general work on distances for quantitative systems where the precise meaning of the quantities remains unspecified has been done. Van Breugel has developed a general theory of behavioral pseudometrics, see e.g. [START_REF] Van Breugel | An introduction to metric semantics: operational and denotational models for programming and specification languages[END_REF], and Fahrenberg and Legay et.al. have introduced linear and branching distances for such systems in [START_REF] Bauer | Weighted modal transition systems[END_REF][START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF]. Henzinger et.al. have employed distances in a software engineering context in [START_REF] Černý | Simulation distances[END_REF] and for abstraction refinement and synthesis in [START_REF] Černý | Quantitative abstraction refinement[END_REF][START_REF] Chatterjee | Compositional quantitative reasoning[END_REF].

A different but related approach to quantitative verification is the theory of weighted automata and quantitative languages developed by Droste et.al. in [START_REF] Droste | Weighted automata and weighted logics[END_REF][START_REF] Droste | Weighted automata and weighted MSO logics for average and long-time behaviors[END_REF][START_REF] Droste | Weighted automata and weighted logics with discounting[END_REF] and by Henzinger and Chatterjee et.al. in [START_REF] Boker | Approximate determinization of quantitative automata[END_REF][START_REF] Chatterjee | Quantitative languages[END_REF].

Common to all the above distance-based approaches is that they introduce distances between systems, or between systems and specifications, and then employ these for approximate or quantitative verification. However, depending on the application context, a plethora of different distances are being used. Consequently, there is a need for a general theory of quantitative verification which depends as little as possible on the concrete distances being used. This is a point of view which is argued in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Černý | Quantitative abstraction refinement[END_REF][START_REF] Chatterjee | Compositional quantitative reasoning[END_REF][START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF], and a number of the above papers [START_REF] Boker | Approximate determinization of quantitative automata[END_REF][START_REF] Droste | Weighted automata and weighted logics[END_REF][START_REF] Droste | Weighted automata and weighted logics with discounting[END_REF][START_REF] Panangaden | Labelled Markov Processes[END_REF][START_REF] Van Breugel | An introduction to metric semantics: operational and denotational models for programming and specification languages[END_REF] attempt to develop the theory at this general level.

To be more specific, most of the above approaches can be classified according to the way they measure distances between executions, or system traces. The perhaps easiest such way is the point-wise distance, which measures the greatest individual distance between corresponding points in the traces. Theory for this specific distance has been developed e.g. in [START_REF] Bouyer | Timed automata can always be made implementable[END_REF][START_REF] De Alfaro | Model checking discounted temporal properties[END_REF][START_REF] De Alfaro | Linear and branching metrics for quantitative transition systems[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF]. Sometimes discounting is applied to diminish the influence of individual distances far in the future, e.g. in [START_REF] De Alfaro | Model checking discounted temporal properties[END_REF][START_REF] De Alfaro | Linear and branching metrics for quantitative transition systems[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF].

Another distance which has been used is the accumulating one, which sums individual distances along executions. Two major types have been considered here: the discounted accumulating distance e.g. in [START_REF] Bauer | Weighted modal transition systems[END_REF][START_REF] Černý | Simulation distances[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF] and the limit-average accumulating distance e.g. in [START_REF] Černý | Simulation distances[END_REF]. For real-time systems, a useful distance is the maximum-lead one of [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF] which measures the maximum difference between accumulated time delays along traces. For hybrid systems, things are more complicated, as distances between hybrid traces have to take into account both spatial and timing differences, see e.g. [START_REF] Girard | Synthesis using approximately bisimilar abstractions: Time-optimal control problems[END_REF][START_REF] Girard | Approximation metrics for discrete and continuous systems[END_REF][START_REF] Quesel | Crossing the bridge between similar games[END_REF][START_REF] Zheng | Bounded and unbounded safety verification using bisimulation metrics[END_REF].

It is our point of view that the differences between measuring distances between system traces are fundamental, in the sense that specifying one concrete way of measuring such trace distances fixes the quantitative semantics to a concrete application. Any general theory of quantitative verification should, then, be independent of the way one measures distances between traces.

In this paper we show how such a distance-independent theory of quantitative verification may be attempted. Taking as our model of quantitative systems the metric transition systems of [START_REF] De Alfaro | Linear and branching system metrics[END_REF] and starting out with an abstract distance on traces, we define linear and branching distances and show that they have the expected properties. Our linear distances generalize trace inclusion and equivalence to the general quantitative setting, and the branching distances generalize simulation and bisimulation.

As a central technical tool in our developments, we assume that the trace distance factors through a complete lattice, and that this lifted trace distance has a recursive characterization. We show that this assumption holds for most of the trace distances considered in the above-mentioned papers; specifically, our theory can be instantiated with the point-wise (and possibly discounted) distance, the accumulating distance (both discounted and limit-average), and the maximum-lead distance.

This paper follows up on work in [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF], where we develop a general quantitative theory for weighted transition systems, using the theory of quantitative games. Compared to this work, the present paper uses a different model for quantitative systems (namely, the one from [START_REF] De Alfaro | Linear and branching system metrics[END_REF]), hence the linear and branching distances have to be defined differently; also, no game theory is necessary for us here.

Metric Transition Systems

We recapitulate the setting and terminology of [START_REF] De Alfaro | Linear and branching system metrics[END_REF], adapting it slightly to our needs.

A hemimetric on a set X is a function d : X × X → R ≥0 ∪ {∞} which satisfies d(x, x) = 0 and d(x, y) + d(y, z) ≥ d(x, z) (the triangle inequality) for all x, y, z ∈ X. The hemimetric is said to be symmetric if also d(x, y) = d(y, x) for all x, y ∈ X; it is said to be separating if d(x, y) = 0 implies x = y. The terms "pseudometric" for a symmetric hemimetric, "quasimetric" for a separating hemimetric, and "metric" for a hemimetric which is both symmetric and separating are also in use, but we will not use them here. The tuple (X, d) is called a hemimetric space.

In [START_REF] De Alfaro | Linear and branching system metrics[END_REF], hemimetrics are called "directed metrics", "undirected" is used instead of "symmetric", and "proper" instead of "separating". Our choice of jargon is driven by a wish to follow more-or-less established terminology; specifically, the term "metric" has a standard meaning in mathematics, so that we find the term "directed metric" for what should better be called a "directed quasi metric" (or, "pseudometric") unfortunate. Similarly, our use of "separating" instead of "proper" is motivated by the use of this term in topology: the topology induced by a (separating) metric has the T 2 Hausdorff separation property, whereas the one induced by a pseudometric does not.

Note that our hemimetrics are extended in that they can take the value ∞. This is convenient for several reasons, cf. [START_REF] Lawvere | Metric spaces, generalized logic, and closed categories[END_REF], one of them being that it allows for a disjoint union, or coproduct, of hemimetric spaces: the disjoint union of

(X 1 , d 1 ) and (X 2 , d 2 ) is the hemimetric space (X 1 , d 1 )∪ + (X 1 , d 2 ) = (X 1 ∪ + X 2 , d)
where points from different components are infinitely far away from each other, i.e. with d defined by

d(x, y) =      d 1 (x, y) if x, y ∈ X 1 , d 2 (x, y) if x, y ∈ X 2 , ∞ otherwise.
We will need to generalize hemimetrics to codomains other than R ≥0 ∪ {∞}.

For a partially ordered monoid (M, , , ), an M -hemimetric on X is a function d : X × X → M which satisfies d(x, x) = and d(x, y) d(y, z) d(x, z) for all x, y, z ∈ X; symmetry and separation are generalized in similar ways. Let Σ be a set of atomic propositions and (X, d) a hemimetric space; these will be fixed throughout this paper. A valuation on Σ is a mapping u : Σ → X; the set of all valuations on Σ is denoted U[Σ]. Note that in the setting of [START_REF] De Alfaro | Linear and branching system metrics[END_REF], each proposition a takes values in a separate hemimetric space X a . Using extended hemimetrics allows us to unite all these spaces into one. The propositional distance [START_REF] De Alfaro | Linear and branching system metrics[END_REF] is the mapping pd :

U[Σ] × U[Σ] → R ≥0 defined by pd(u, v) = sup a∈Σ d(u(a), v(a)).
A metric transition system (MTS) S = (S, T, [•]) consists of sets S of states and T ⊆ S × S of transitions, together with a state valuation mapping [•] : S → U[Σ]. For s, t ∈ S, we write s → t iff (s, t) ∈ T . Fig. 2 shows a simple example of a MTS over Σ = {a} which we will use later.

A path in S is a (finite or infinite) sequence π = (π 0 , π 1 , . . . ) of states π i ∈ S in which π i → π i+1 for all i. Note that, extending [START_REF] De Alfaro | Linear and branching system metrics[END_REF], we also handle finite paths instead of only infinite ones.

A trace in Σ is a (finite or infinite) sequence σ = (σ 0 , σ 1 , . . . ) of valuations As usual, a relation R ⊆ S × S is called a simulation (on S) if it holds that [s] = [t] for all (s, t) ∈ S and for all s → s there is

σ i ∈ U[Σ]. The set of such traces is denoted U[Σ] ∞ . For a path π in S, its induced trace is [π] = ([π 0 ], [π 1 ], . . . ).
t → t such that (s , t ) ∈ R.
R is called a bisimulation if, additionally, for all t → t there is s → s such that (s , t ) ∈ R.

We write s t if there is a simulation R with (s, t) ∈ R, and s ≈ t if there is a bisimulation R with (s, t) ∈ R.

Examples of Trace Distances

We can now give concrete examples of trace distances which have been used in the literature.

The point-wise trace distance is

td pw : U[Σ] ∞ × U[Σ] ∞ → R ≥0 ∪ {∞} defined by td pw (σ, τ ) = ∞ if len(σ) = len(τ ), sup i pd(σ i , τ i ) otherwise.
This distance has been employed in [START_REF] Bouyer | Timed automata can always be made implementable[END_REF][START_REF] De Alfaro | Model checking discounted temporal properties[END_REF][START_REF] De Alfaro | Linear and branching metrics for quantitative transition systems[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF].

Using a discount factor λ ∈ R ≥0 with λ < 1, one may discount the influence of individual distances which occur further along the traces. The discounted point-wise trace distance, which has been used in [START_REF] De Alfaro | Model checking discounted temporal properties[END_REF][START_REF] De Alfaro | Linear and branching metrics for quantitative transition systems[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF], is thus td pw,λ :

U[Σ] ∞ × U[Σ] ∞ → R ≥0 ∪ {∞} defined by td pw,λ (σ, τ ) = ∞ if len(σ) = len(τ ), sup i λ i pd(σ i , τ i ) otherwise. The accumulating trace distance is td acc : U[Σ] ∞ × U[Σ] ∞ → R ≥0 ∪ {∞} defined by td acc (σ, τ ) = ∞ if len(σ) = len(τ ),
i pd(σ i , τ i ) otherwise. This distance is typically used with discounting or limit-averaging:

Using again a discount factor λ ∈ R ≥0 with λ < 1, the discounted accumulating trace distance is td acc,λ :

U[Σ] ∞ × U[Σ] ∞ → R ≥0 ∪ {∞} defined by td acc,λ (σ, τ ) = ∞ if len(σ) = len(τ ), i λ i pd(σ i , τ i ) otherwise.
This distance has been used in [START_REF] Bauer | Weighted modal transition systems[END_REF][START_REF] Černý | Simulation distances[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF]. The limit-average trace distance, which has been used in [START_REF] Černý | Simulation distances[END_REF], is td limavg :

U[Σ] ∞ × U[Σ] ∞ → R ≥0 ∪ {∞} defined by td limavg (σ, τ ) = ∞ if len(σ) = len(τ ), lim inf j 1 j+1 j i=0 pd(σ i , τ i ) otherwise.
This is generally defined only for infinite traces. If one wants it defined also for finite traces σ, τ (of equal length N ), one can patch σ and τ so that pd(σ i , τ i ) = 0 for i > N ; then td limavg (σ, τ ) = 0 in this case.

Both the discounted accumulating and limit-average trace distances are wellknown from the theory of discounted and mean-payoff games [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF][START_REF] Zwick | The complexity of mean payoff games[END_REF].

The maximum-lead trace distance td maxlead : [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF] is only defined for the case where the valuation space is X = R. It is given by

U[Σ] ∞ × U[Σ] ∞ → R ≥0 ∪ {∞} from
td maxlead (σ, τ ) = ∞ if len(σ) = len(τ ), sup j sup a∈Σ j i=0 σ i (a) - j i=0 τ i (a) otherwise.

Linear Distances

To generalize the examples of the previous section, we define a trace distance to be a general hemimetric on traces which specializes to the propositional distance on individual valuations and is finite only for traces of equal length:

Definition 1. A trace distance is a hemimetric td : U[Σ] ∞ × U[Σ] ∞ → R ≥0 ∪
{∞} for which td(u, v) = pd(u, v) for all u, v ∈ U[Σ] and td(σ, τ ) = ∞ whenever len(σ) = len(τ ).

We note that in case pd is separating, then also all example trace distances from Section 3 are separating, except for the limit-average distance. For the latter, td limavg (σ, τ ) = 0 iff either σ = τ are finite traces, or there exists an index k such that σ i = τ i for all i ≥ k. Also, the maximum-lead trace distance is symmetric; the others are symmetric iff pd is symmetric.

For any given trace distance, we can define the linear distance between states in S as the (asymmetric) Hausdorff distance between the corresponding sets of traces: Definition 2. For a given trace distance td, the linear distance induced by td is

ld : S × S → R ≥0 ∪ {∞} given by ld(s, t) = sup σ∈Tr(s) inf τ ∈Tr(t) td(σ, τ ).
The symmetric linear distance induced by td is ld : S × S → R ≥0 ∪ {∞} given by ld(s, t) = max(ld(s, t), ld(t, s)).

Continuing the example from Fig. 2, we compute the linear distances ld(s 1 , t 1 ) and ld(s 2 , t 2 ) induced by all our example trace distances, using the usual metric on R for valuations and a discount factor of λ = .9 where applicable:

ld pw (s 1 , t 1 ) = 4 ld pw (s 2 , t 2 ) = 4
ld pw,λ (s 1 , t 1 ) = 3.24 ld pw (s 2 , t 2 ) = 3.24

ld acc (s 1 , t 1 ) = 5 ld acc (s 2 , t 2 ) = ∞ ld acc,λ (s 1 , t 1 ) = 4.14 ld acc,λ (s 2 , t 2 ) = 33.3 ld limavg (s 1 , t 2 ) = 0 ld limavg (s 2 , t 2 ) = 4 ld maxlead (s 1 , t 1 ) = 5 ld maxlead (s 2 , t 2 ) = ∞
Our first theorem shows that for separating trace distances on finite transition systems, trace inclusion is the kernel of ld and trace equivalence the kernel of ld: Theorem 1. Let S be finite and td separating. For all s, t ∈ S, Tr(s) ⊆ Tr(t) iff ld(s, t) = 0 and Tr(s) = Tr(t) iff ld(s, t) = 0.

Proof. It is clear that Tr(s) ⊆ Tr(t) implies ld(s, t) = 0. For the opposite direction, assume ld(s, t) = 0 and let σ ∈ Tr(s). For every i ∈ N + , there exists τ i ∈ Tr(t) for which td(σ, τ i ) < 1 i . Because S is finite, there is an index N such that τ i = τ N for all i ≥ N . Then td(σ, τ N ) = 0 and thus, as td is separating, σ = τ N . The second bi-implication is now clear.

Note that we have also shown the statement that, whether td is separating or not, ld(s, t) = 0 implies that for every σ ∈ Tr(s), there exists τ ∈ Tr(t) with td(σ, τ ) = 0. An example in [START_REF] De Alfaro | Linear and branching system metrics[END_REF] shows that precisely this statement may fail in case S is not finite.

Branching Distances

We have seen in Theorem 1 that the linear distances of the previous section are generalizations of trace inclusion and trace equivalence. In order to generalize simulation and bisimulation in a similar manner, we define branching distances.

To be able to introduce these branching distances, we need to assume that our trace distance td factors through a complete lattice, and that the lifted trace distance has a recursive characterization as given below. We will see in Section 6 that this is the case for all the example trace distances of Section 3.

For any set M , let LM = (R ≥0 ∪ {∞}) M be the set of functions from M to R ≥0 ∪ {∞}. Then LM is a complete lattice with partial order given by α β iff α(x) ≤ β(x) for all x ∈ M , and with an addition given by

(α β)(x) = α(x) + β(x).
The bottom element of LM is also the zero of and given by ⊥(x) = 0, and the top element is (x) = ∞.

L (s, t) = sup s→s inf t→t F ([s], [t], sd L (s , t )), (1) bd L (s, t) = max    sup s→s inf t→t F ([s], [t], bd L (s , t )), sup t→t inf s→s F ([s], [t], bd L (s , t )).
(

2)

The simulation distance induced by td is sd : S × S → R ≥0 ∪ {∞} given by sd = eval•sd L ; the bisimulation distance induced by td is bd : S ×S → R ≥0 ∪{∞} given by bd = eval • bd L .

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

Lemma 1. The mappings sd and bd are well-defined hemimetrics on S.

Proof. We show the proof for sd; for bd it is similar. Let FS = LM S×S be the lattice of functions from S × S to LM, then FS is complete because LM is. Let I : FS → FS be defined by

I(f )(s, t) = sup s→s inf t→t F ([s], [t], f (s , t )), similarly to (1). Because F ([s], [t], •) : LM → LM is monotone for all s, t ∈ S,
I is monotone. Using Tarski's fixed-point theorem, we can hence conclude that I has a unique minimal fixed point, which is sd L . Clearly sd L (s, s) = ⊥ for all s ∈ S, and by induction one can show that sd L (s, t) sd L (t, u) sd L (s, u) for all s, t, u ∈ S. Hence sd L is an LM-hemimetric and sd is a hemimetric.

In order to show, similarly to Theorem 1, that simulation is the kernel of simulation distance, we need a condition on the recursive F which mimics the separation condition for hemimetrics. We say that a recursively specified trace distance td is recursively separating if F : U[Σ] × U[Σ] × LM → LM satisfies the condition that whenever F (u, v, x) = ⊥, then u = v and x = ⊥. Note that this condition implies that td L is separating.

Theorem 2. Let S be finite and td recursively specified and recursively separating. For all s, t ∈ S, s t iff sd L (s, t) = ⊥ and s ≈ t iff bd L (s, t) = ⊥.

Proof. It is clear that s t implies sd L (s, t) = ⊥. For the other direction, let R = {(s , t ) | sd L (s , t ) = ⊥} ⊆ S × S. Then (s, t) ∈ R. Let (s , t ) ∈ R, then sup s →s inf t →t F ([s ], [t ], sd L (s , t )) = ⊥.
As S is finite, this implies that for all s → s , there exists t → t with F ([s ], [t ], sd L (s , t )) = ⊥. By recursive separation, we hence have [s ] = [t ] and sd L (s , t ) = ⊥. We have shown that R is a simulation on S. The proof that s ≈ t iff bd L (s, t) = ⊥ is similar.

The next theorem gives the relations between the different distances we have introduced. Also these relations generalize the situation in the Boolean setting: in light of Theorems 1 and 2, they are quantitative analogues to the facts that simulation implies trace inclusion and that bisimulation implies simulation and trace equivalence. Theorem 3. Let td be recursively specified. For all s, t ∈ S, ld(s, t) ≤ sd(s, t) ≤ bd(s, t) and ld(s, t) ≤ bd(s, t).

Proof. The proof is best understood in a setting of quantitative games, cf. [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF]. In this setting, the standard simulation and bisimulation games [START_REF] Stirling | Modal and temporal logics for processes[END_REF] are generalized to games with quantitative objectives. One can then see that the linear distances can be computed by similar games, and that the only differences between these games are given by certain restrictions on the strategies available to the first player. The result follows from inclusions on these sets of restricted strategies.

We can, however, also give a direct proof of the fact that ld(s, t) ≤ sd(s, t) without resorting to games (and similar proofs may be given for the other inequalities). To do so, we need to lift ld to the lattice LM: for s, t ∈ S, define ld L (s, t) = sup σ∈Tr(s) inf τ ∈Tr(t) td L (σ, τ ), then ld = eval • ld L because eval is monotone. We show that ld L (s, t) sd L (s, t) for all s, t ∈ S, which will imply the result.

Let s, t ∈ S. We have

ld L (s, t) = sup σ∈Tr(s) inf τ ∈Tr(t) td L (σ, τ ) = sup s→s sup σ ∈Tr(s ) inf t→t inf τ ∈Tr(t ) td L ([s].σ , [t].τ ) = sup s→s sup σ ∈Tr(s ) inf t→t inf τ ∈Tr(t ) F ([s], [t], td L (σ , τ )) sup s→s inf t→t sup σ ∈Tr(s ) inf τ ∈Tr(t ) F ([s], [t], td L (σ , τ )) = sup s→s inf t→t F ([s], [t], sup σ ∈Tr(s ) inf τ ∈Tr(t ) td L (σ , τ )) = sup s→s inf t→t F ([s], [t], ld L (s , t )),
and the statement now follows by induction.

Examples Revisited

We can now apply the constructions of Section 5 to the example trace distances from Section 3. We give recursive specifications for all distances and deduce the corresponding branching distances. For ease of exposition, we will only consider ourselves with the simulation distances here, but similar things can be said about the bisimulation distances.

For the point-wise trace distance td pw , a recursive specification is given as follows (where { * } denotes the one-point set; hence LM is isomorphic to R ≥0 ∪ {∞}):

M = { * } eval(x) = x td L (σ, τ ) = sup i pd(σ i , τ i ) F (u, v, x) = max(pd(u, v), x)
Using Definition 4, the corresponding simulation distance sd pw = sd L pw is the least fixed point to the equations

sd pw (s, t) = sup s→s inf t→t max(pd([s], [t]), sd pw (s , t )).
This is similar to the formulation given in [START_REF] De Alfaro | Linear and branching metrics for quantitative transition systems[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF]. Note that if pd is separating, then F is recursively separating, hence Theorem 2 applies.

For the discounted point-wise trace distance td pw,λ the recursive specification is similar:

M = { * } eval(x) = x td L (σ, τ ) = sup i λ i pd(σ i , τ i ) F (u, v, x) = max(pd(u, v), λx)
The corresponding simulation distance is hence the least fixed point to the equations sd pw,λ (s, t) = sup

s→s inf t→t max(pd([s], [t]), λsd pw,λ (s , t )),
which is similar to what is in [START_REF] De Alfaro | Linear and branching metrics for quantitative transition systems[END_REF][START_REF] De Alfaro | Linear and branching system metrics[END_REF]. Note again that if pd is separating, then F is recursively separating, hence also here Theorem 2 applies. Also the accumulating trace distance td acc has a simple recursive specification with LM isomorphic to R ≥0 ∪ {∞}:

M = { * } eval(x) = x td L (σ, τ ) = i pd(σ i , τ i ) F (u, v, x) = pd(u, v) + x
The corresponding simulation distance is hence the least fixed point to the equations sd acc (s, t) = sup

s→s inf t→t (pd([s], [t]) + sd acc (s , t )).
Again, if pd is separating, then F is recursively separating, hence Theorem 2 applies.

A recursive specification for the discounted accumulating trace distance is given as follows:

M = { * } eval(x) = x td L (σ, τ ) = i λ i pd(σ i , τ i ) F (u, v, x) = pd(u, v) + λx
The corresponding simulation distance is then the least fixed point to the equations sd acc,λ (s, t) = sup

s→s inf t→t pd([s], [t]) + λsd acc,λ (s , t ),
similarly to what is in [START_REF] Černý | Simulation distances[END_REF]. If pd is separating, then F is recursively separating, hence Theorem 2 applies also in this case.

To obtain a recursive specification of the limit-average trace distance, we need a richer lattice:

M = N eval(x) = lim inf j x(j) td L (σ, τ )(j) = 1 j+1 j i=0 pd(σ i , τ i ) F (u, v, x)(j) = 1 j+1 pd(u, v) + j j+1 x(j -1)
Using Definition 4, we obtain the corresponding lifted simulation distance as the least fixed point to the equations sd L limavg (s, t)(j) = sup The limit-average simulation distance is then sd limavg (s, t) = lim inf j sd L limavg (s, t)(j).

To the best of our knowledge, this formulation of limit-average simulation distance is new. We again remark that if pd is separating, then F is recursively separating, hence Theorem 2 applies. For the maximum-lead trace distance, we need a lattice which maps leads to maximum leads. A recursive specification is as follows:

M = R eval(x) = x(0) td L (σ, τ )(δ) = max(|δ|, sup j sup a∈Σ |δ + j i=0 σ i (a) - j i=0 τ i (a)|) F (u, v, x)(δ) = sup a∈Σ max(|δ + u(a) -v(a)|, x(δ + u(a) -v(a)))
The lifted simulation distance is then the least fixed point to the equations

sd L maxlead (s, t)(δ) = sup s→s inf t→t sup a∈Σ max |δ + [s](a) -[t](a)|, sd L maxlead (s , t )(δ + [s](a) -[t](a)),
cf. [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF], and maximum-lead simulation distance is sd maxlead (s, t) = sd L maxlead (s, t)(0).

Also here it holds that if pd is separating, then F is recursively separating, hence Theorem 2 applies.

Finishing the example from Fig. 2, we compute the simulation distances sd(s 1 , t 1 ) and sd(s 2 , t 2 ) induced by all our example trace distances, using the usual metric on R for valuations and a discount factor of λ = .9 where applicable:

sd pw (s 1 , t 1 ) = 6 sd pw (s 2 , t 2 ) = 6
sd pw,λ (s 1 , t

A Note on Robustness

In [START_REF] De Alfaro | Linear and branching system metrics[END_REF] it is shown that with respect to the point-wise linear and branching distances, metric transition systems are robust to perturbations in the state valuations. To be precise, let

[•] 1 , [•] 2 : S → U[Σ]
be two different state valuations on a MTS S and define their valuation distance by vd(

[•] 1 , [•] 2 ) = sup s∈S pd([s] 1 , [s] 2 ).
This measures how close the state valuations are to each other. Now write ld i pw and sd i pw (with i ∈ {1, 2}) for the point-wise linear and simulation distances with respect to the valuation [•] i . It is shown in [START_REF] De Alfaro | Linear and branching system metrics[END_REF] that for all s, t ∈ S,

|ld 1 pw (s, t) -ld 2 pw (s, t)| ≤ vd([•] 1 , [•] 2 ) + vd([•] 2 , [•] 1 ), |sd 1 pw (s, t) -sd 2 pw (s, t)| ≤ vd([•] 1 , [•] 2 ) + vd([•] 2 , [•] 1 ).
This is, hence, a robustness result: given that the two valuations are close to each other, also the linear and branching distances will be. Similar results can easily be seen to hold also for the symmetric linear and the bisimulation distances, and also for the discounted point-wise versions of these distances. A result similar in spirit, also for the point-wise distance, is reported for robustness of timed automata in [START_REF] Bouyer | Timed automata can always be made implementable[END_REF].

Using almost the same arguments as in [START_REF] De Alfaro | Linear and branching system metrics[END_REF], one can show that for the discounted accumulating distances,

|ld 1 acc,λ (s, t) -ld 2 acc,λ (s, t)| ≤ 1 1-λ (vd([•] 1 , [•] 2 ) + vd([•] 2 , [•] 1 )), |sd 1 acc,λ (s, t) -sd 2 acc,λ (s, t)| ≤ 1 1-λ (vd([•] 1 , [•] 2 ) + vd([•] 2 , [•] 1 )).
Hence MTS are also robust with respect to the discounted accumulating distances. In the proof, one uses the convergence of the geometric series: after the ith step, distances are discounted by λ i , so no more than λ i (vd

([•] 1 , [•] 2 )+vd([•] 2 , [•] 1 )
) can be added to the total distance. Hence the distance is bounded above by

(vd([•] 1 , [•] 2 ) + vd([•] 2 , [•] 1 )) ∞ i=0 λ i = 1 1-λ (vd([•] 1 , [•] 2 ) + vd([•] 2 , [•] 1 )
). Unfortunately, no general robustness results are available, and our other example distances do not have similar properties. This is shown by the example in Fig. 3

Conclusion

We have shown how the model of metric transition systems from [START_REF] De Alfaro | Linear and branching system metrics[END_REF] can be embedded in a general quantitative framework which allows quantitative verification using a large number of different system distances. As these distances are an essential part of quantitative verification and, at the same time, typically depend on what precise application one has in mind, it is important to develop a general quantitative theory of systems which is independent of the employed distances. This is what we have done here.

Assuming an abstract trace distance as input, we have developed corresponding linear and branching distances. What we have not done, however, is to compare linear and branching distances which arise from different trace distances. One important question is, for example, whether the linear and branching distances one obtains from two Lipschitz equivalent, or topologically equivalent, trace distances will again be Lipschitz or topologically equivalent. This would be a crucial step in a classification of system distances and is part of our ongoing research.

Another issue which we have not treated here is the logical side of quantitative verification. In [START_REF] De Alfaro | Linear and branching system metrics[END_REF], the authors introduce a quantitative variant of LTL which characterizes the point-wise linear distance, and a quantitative µ-calculus which characterizes the point-wise simulation and bisimulation distances. We plan to work on similar logics for our general setting.

Fig. 1 .

 1 Fig. 1. Three timed automata modeling a train crossing.

15 Fig. 2 .

 152 Fig. 2. Example of a metric transition system

  For a state s ∈ S, we let Tr(s) = {[π] | π 0 = s} denote the set of traces emanating from s. We introduce some convenient notation for traces: denotes the empty trace, u.σ the concatenation of u ∈ U[Σ] with σ ∈ U[Σ] ∞ , and len(σ) the length (finite or ∞) of σ.

Definition 3 .Definition 4 .

 34 A recursive specification of a trace distance td consists of a set M , a lattice homomorphism eval : LM → R ≥0 ∪ {∞} and an LM-hemimetrictd L : U[Σ] ∞ ×U[Σ] ∞ → LM which together satisfy td = eval•td L , and a function F : U[Σ] × U[Σ] × LM → LM. F must be monotone in the third coordinate, i.e. F (u, v, •) : LM → LM is monotone for all u, v ∈ U[Σ], have F (u, u, ⊥) = ⊥ for all u ∈ U[Σ], and satisfy, for all u, v ∈ U[Σ] and σ, τ ∈ U[Σ] ∞ , that td L (u.σ, v.τ ) = F (u, v, td L (σ, τ )).Now if td is recursively specified as above, then we can use the recursion to introduce branching distances sd and bd which generalize simulation and bisimulation: For a recursively specified trace distance td, let sd L , bd L : S ×S → LM be the respective least fixed points to the equations sd

s→s inf t→t 1 j+1

 1 pd([s], [t]) + j j+1 sd L limavg (s , t )(j -1) .

= 1 Fig. 3 .

 13 Fig. 3. Example of a MTS with two different state valuations.

  1 ) = 5.46 sd pw,λ (s 2 , t 2 ) = 5.46 sd acc (s 1 , t 1 ) = 6 sd acc (s 2 , t 2 ) = ∞ sd acc,λ (s 1 , t 1 ) = 5.46 sd acc,λ (s 2 , t 2 ) = 54 sd limavg (s 1 , t 2 ) = 0 sd limavg (s 2 , t 2 ) = 6 sd maxlead (s 1 , t 1 ) = 6 sd maxlead (s 2 , t 2 ) = ∞

  . Here, vd([•] 1 , [•] 2 ) = vd([•] 2 , [•] 1 ) = 1,and the linear distances are as follows, with the usual metric on R and λ = .9 where applicable:

	ld 1 pw (s, t) = 0	ld 2 pw (s, t) = 1	ld 1 pw (t, s) = 0	ld 2 pw (t, s) = 1
	ld 1 pw,λ (s, t) = 0	ld 2 pw,λ (s, t) = 1	ld 1 pw,λ (t, s) = 0	ld 2 pw,λ (t, s) = 1
	ld 1 acc (s, t) = 0	ld 2 acc (s, t) = ∞	ld 1 acc (t, s) = 0	ld 2 acc (t, s) = ∞
	ld 1 acc,λ (s, t) = 0	ld 2 acc,λ (s, t) = 10	ld 1 acc,λ (t, s) = 0	ld 2 acc,λ (t, s) = 10
	ld 1 limavg (s, t) = 0	ld 2 limavg (s, t) = ∞	ld 1 limavg (t, s) = 0	ld 2

limavg (t, s) = ∞ ld 1 maxlead (s, t) = 0 ld 2 maxlead (s, t) = ∞ ld 1 maxlead (t, s) = 0 ld 2 maxlead (t, s) = ∞

(The branching distances are equal to the linear distances in all cases.)