Uli Fahrenberg

Axel Legay

The Quantitative Linear-Time-Branching-Time Spectrum

Keywords: Quantitative verification, system distance, distance hierarchy, linear time, branching time

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time-branching-time spectrum to a quantitative setting, parametrized by trace distance. We also prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.

Introduction

For rigorous design and verification of embedded systems, both qualitative and quantitative information and constraints have to be taken into account [START_REF] Henzinger | The embedded systems design challenge[END_REF][START_REF] Lee | Absolutely positively on time: What would it take[END_REF][START_REF] Stankovic | Opportunities and obligations for physical computing systems[END_REF]. This applies to the models considered, to the properties one wishes to be satisfied, and to the verification itself. Hence the question asked in quantitative verification is not "Does the system satisfy the requirements?", but rather "To which extent does the system satisfy the requirements?" Standard qualitative verification techniques are inherently fragile: either the requirements are satisfied, or they are not, regardless of how close the actual system might come to the specification. To overcome this lack of robustness, notions of distance between systems are essential.

As pointed out in [START_REF] Henzinger | The embedded systems design challenge[END_REF], qualitative and quantitative aspects of verification are best treated orthogonally in any theory of quantitative verification. In practical applications these aspects may indeed interfere with each other, but for the purpose of theory, they are best treated separately. The formalism we propose in this paper addresses this separation by modeling qualitative aspects using standard labeled transition systems and expressing the quantitative aspects using trace distances, or distances on system executions. Based on these ingredients, we develop a comprehensive theory of system distances which generalizes the standard linear-time-branching-time spectrum [START_REF] De | Bi)simulations up-to characterise process semantics[END_REF][START_REF] De | On the unification of process semantics: Equational semantics[END_REF][START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF] to a quantitative setting, see Figure 1. Similarly to [START_REF] Chen | Game characterizations of process equivalences[END_REF], our theory relies on Ehrenfeucht-Fraïssé games and allows for a more refined analysis of systems. More precisely, our parametrized framework forms a hierarchy of games, for each trace distance used in its instantiation. In the quantitative setting, using games with quantitative objectives as opposed to discrete games, effectively allows us to obtain a continuous verdict on the relationship between systems, and hence to detect the difference between minor and major discrepancies between systems. We refer to [START_REF] Ferguson | Game theory[END_REF] for a good introduction to the theory of quantitative games.

Indeed the view of this paper is that in a theory of quantitative verification, the quantitative aspects should be treated just as much as an input to a verification problem as the qualitative aspects are. Hence it is of limited use to develop a theory pertaining only to some specific quantitative measures like the ones in [START_REF] Černý | Simulation distances[END_REF][START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF] and other papers which all treat only a few specific ways of measuring distances; any theory of quantitative verification should work just as well regardless of the way the engineers decide to measure differences between system executions. We note that the framework we lay out here may be equally instantiated with labels (or propositions) in states rather than on transitions, hence it also generalizes the formalisms of [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Franck Van Breugel | A behavioural pseudometric for metric labelled transition systems[END_REF].

We take as input a labeled transition system and a trace distance; both are unspecified except for some general characteristic properties. Based on this information and using the theory of quantitative games, we lift most of the linear-time-branching-time spectrum of van Glabbeek [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF] to the quantitative setting, while the rest may be obtained in a similar way using minor additional conditions as described in [START_REF] Chen | Game characterizations of process equivalences[END_REF]. We show that all the distinct equivalences in van Glabbeek's spectrum correspond to topologically inequivalent distances in the quantitative setting.

As our framework is independent of the chosen trace distance, we are essentially adding a second, quantitative, dimension to the linear-time-branching-time spectrum. In this terminology, the first dimension is the qualitative one which concerns the different linear and branching ways of specifying qualitative constraints, and the second dimension bridges the gap between the trivial van-Glabbeek spectrum in which everything is equivalent, and the discrete spectrum in which everything is fragile.

We start the paper by recalling some preliminaries and fixing notation in Section 2. Section 3 then shows that our general framework of trace distances is applicable to a large number of system distances found in the literature [2, 3, 5-8, 10-12, 20, 22, 24, 32, 33, 35, 37]; indeed we show in Section 8 that it generalizes all of them.

Before this, we devote Section 4 to introducing a game with quantitative objectives on which all the subsequent developments build, and Section 5 to show some general properties of this game. In Section 6 we reap the fruits of our labor and develop all of the quantitative linear-time-branching-time spectrum of Figure 1. Section 7 then prepares for Section 8 by treating an important special case where the trace distance in question has a certain recursive characterization.

Here we show that in this case, all distances in the spectrum can be expressed as fixed points of certain functionals.

Seeing in Section 8 that all known applications of our framework are instantiations of the special case of recursively defined trace distances, it is most probable that the fixed-point characterizations of Section 7 will be the most important part of this work, and that the game-based framework introduced and used in the preceding sections should be seen only as a justification of Section 7.

This paper is an extended and revised version of papers which have appeared as [START_REF] Fahrenberg | The quantitative lineartime-branching-time spectrum[END_REF][START_REF] Fahrenberg | Distances for weighted transition systems: Games and properties[END_REF]. Compared to these papers, some more background and motivation has been added to Sections 4 and 6, Section 7 has been greatly extended, and all proofs are included in the paper.

The authors wish to thank Claus Thrane, Kim G. Larsen and Igor Walukiewicz for interesting and fruitful discussions on the subject, and Luca Aceto for some insightful comments on a previous version of this paper.

Traces, Trace Distances, and Transition Systems

In this paper, the set ◆ of natural numbers includes 0; the set of positive natural numbers is denoted by ◆ + . For a finite non-empty sequence a = (a 0 , . . . , a n ), we write last(a) = a n and len(a) = n + 1 for the length of a; for an infinite sequence a we let len(a) = ∞. Concatenation of finite sequences a and b is denoted a • b. We denote by a k = (a k , a k+1 , . . . ) the k-shift, and by a i the (i + 1)st element, of a (finite or infinite) sequence, and by ǫ the empty sequence.

We need to recall some terminology and constructions regarding distances.

A hemimetric on a set X is a function d : X × X → | ≥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. 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.
The product of two hemimetric spaces

(X 1 , d 1 ) and (X 2 , d 2 ) is the hemimetric space (X 1 , d 1 ) × (X 2 , d 2 ) = (X 1 × X 2 , d) with d given by d((x 1 , x 2 ), (y 1 , y 2 )) = max(d 1 (x 1 , y 1 ), d 2 (x 2 , y 2 )).
The symmetrization of a hemimetric d on X is the symmetric hemimetric

d : X × X → | ≥0 ∪ {∞} defined by d(x, y) = max(d(x, y), d(y, x)); this is the smallest of all symmetric hemimetrics d ′ on X for which d ≤ d ′ .
The topology generated by a hemimetric d on X is the same as the one generated by its symmetrization d; it has as open sets all unions of open balls B(x; r) = {y ∈ X | d(x, y) < r}, for x ∈ X and r > 0. Two hemimetrics d 1 and d 2 on X are said to be topologically equivalent if the topologies on X generated by d 1 and d 2 coincide. Topological equivalence hence preserves topological notions such as convergence of sequences: If a sequence (x j ) of points in X converges in one hemimetric, then it also converges in the other. As a consequence, topological equivalence of d 1 and d 2 implies that for all x, y ∈ X, d 1 (x, y) = 0 if, and only if, d 2 (x, y) = 0.

Topological equivalence is the weakest of the common notions of equivalence for metrics; it does not preserve geometric properties such as distances or angles. We are hence mainly interested in topological equivalence as a tool for showing negative properties; we will later prove a number of results on topological inequivalence of hemimetrics which imply that any other reasonable metric equivalence, such as uniform or Lipschitz equivalence, also fails for these cases.

Throughout this paper we fix a set ❑ of labels, and we let ❑ ∞ = ❑ * ∪ ❑ ω denote the set of finite and infinite traces (i.e. sequences) in ❑. A hemimetric

d T : ❑ ∞ × ❑ ∞ → | ≥0 ∪ {∞} is called a trace distance if len(σ) = len(τ ) implies d T (σ, τ ) = ∞.
A labeled transition system (LTS) is a pair (S, T ) consisting of states S and transitions T ⊆ S × ❑ × S. We often write s x -→ t to signify that (s, x, t) ∈ T . Given e = (s, x, t) ∈ T , we write src(e) = s, tgt(e) = t for the source and target of e. A path in (S, T ) is a finite or infinite sequence π = ((s 0 , x 0 , t 0 ), (s 1 , x 1 , t 1 ), . . . ) of transitions (s j , x j , t j ) ∈ T which satisfy t j = s j+1 for all j. We denote by tr(π) = (x 0 , x 1 , . . . ) the trace induced by such a path π. For s ∈ S we denote by Pa(s) the set of (finite or infinite) paths from s and by Tr(s) = {tr(π) | π ∈ Pa(s)} the set of traces from s.

Examples of Trace Distances

We show here a number of trace distances with which our quantitative framework can be instantiated. Note that each such distance gives rise to its own linear-time-branching-time spectrum in the quantitative dimension.

Most of the trace distances one finds in the literature are defined by giving a hemimetric d on ❑ and a method to combine the so-defined distances on individual symbols to a distance on traces. Three general methods are used for this combination (recall that σ j denotes the (j +1)-th symbol in σ = (σ 0 , σ 1 , . . . )):

• The point-wise trace distance: PW λ (d)(σ, τ ) = sup j λ j d(σ j , τ j );

• the accumulating trace distance: ACC λ (d)(σ, τ ) = j λ j d(σ j , τ j );

• The limit-average trace distance:

AVG(d)(σ, τ ) = lim inf j 1 j+1 j i=0 d(σ i , τ i ).
Note that the trace distances are parametrized by the label distance d : ❑×❑ → | ≥0 ∪ {∞}. Also, λ is a discounting factor with 0 < λ ≤ 1, and we assume that the involved traces have equal length; otherwise any trace distance has value ∞. The point-wise distance thus measures the (discounted) greatest individual symbol distance in the traces, whereas accumulating and limit-average distance accumulate these individual distances along the traces.

If the distance on ❑ is the discrete distance given by d disc (x, x) = 0 and d disc (x, y) = ∞ for x = y, then all trace distances above agree, for any λ. This defines the discrete trace distance

d T disc = PW λ (d disc ) = ACC λ (d disc ) = AVG(d disc )
given by d T disc (σ, τ ) = 0 if σ = τ and ∞ otherwise. We will show below that for the discrete trace distance, our quantitative linear-time-branching-time spectrum specializes to the qualitative one of [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF].

If one lets d(x, x) = 0 and d(x, y) = 1 for x = y instead, then ACC 1 (d) is Hamming distance [START_REF] Hamming | Error detecting and error correcting codes[END_REF] for finite traces, and ACC λ (d) with λ < 1 and AVG(d) are two sensible ways to define Hamming distance also for infinite traces. PW 1 (d) is topologically equivalent to the discrete distance; indeed, PW 1 (d)(σ, τ ) = 1 if, and only if,

d T disc (σ, τ ) = ∞.
A generalization of the above distances may be obtained by equipping ❑ with a preorder ⊑ ⊆ ❑ × ❑ indicating that a label x ∈ ❑ may be replaced by any y ∈ ❑ with x ⊑ y, as e.g. in [START_REF] Thomsen | An extended bisimulation induced by a preorder on actions[END_REF]. If we define d(x, y) = 0 if x ⊑ y and d(x, y) = ∞ otherwise (note that this is a hemimetric which is not necessarily symmetric), then again PW λ (d) = ACC λ (d) = AVG(d) for any λ.

Point-wise and accumulating distances have been studied in a number of papers [START_REF] Černý | Simulation distances[END_REF][START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF][START_REF] Franck Van Breugel | A behavioural pseudometric for metric labelled transition systems[END_REF]. PW 1 (d) is the point-wise distance from [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Desharnais | Approximate analysis of probabilistic processes[END_REF][START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF], and PW λ (d) for λ < 1 is the discounted distance from [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Luca De Alfaro | Discounting the future in systems theory[END_REF]. Accumulating distance ACC λ (d) has been studied in [START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF], and AVG(d) e.g. in [START_REF] Černý | Simulation distances[END_REF][START_REF] Chatterjee | Quantitative languages[END_REF]. Both ACC λ (d) and AVG(d) are well-known 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].

All distances above were obtained from distances on individual symbols in ❑. A trace distance for which this is not the case is the maximum-lead distance from [22, 33] defined for ❑ ⊆ Σ × |, where Σ is a finite alphabet. Writing x ∈ ❑ as x = (x ℓ , x w ), it is given by

d T ± (σ, τ ) = sup j j i=0 σ w i - j i=0 τ w i if σ ℓ j = τ ℓ j for all j, ∞ otherwise.
As this measures differences of accumulated labels along runs, it is especially useful for real-time systems, cf. [START_REF] Fahrenberg | A robust specification theory for modal event-clock automata[END_REF][START_REF] Henzinger | Quantifying similarities between timed systems[END_REF]. As a last example of a trace distance we mention the Cantor distance given by d

T C (σ, τ ) = (1 + inf{j | σ j = τ j }) -1 .
Cantor distance hence measures the (inverse of the) length of the common prefix of the sequences and has been used for verification e.g. in [START_REF] Doyen | Robustness of sequential circuits[END_REF]. Both Hamming and Cantor distance have applications in information theory and pattern matching.

We will return to our example trace distances in Section 8 to show how our framework may be applied to yield concrete formulations of distances in the linear-time-branching-time spectrum relative to these.

Quantitative Ehrenfeucht-Fraïssé Games

To lift the linear-time-branching-time spectrum to the quantitative setting, we define below a quantitative Ehrenfeucht-Fraïssé game [START_REF] Ehrenfeucht | An application of games to the completeness problem for formalized theories[END_REF][START_REF] Fraïssé | Sur quelques classifications des systèmes de relations[END_REF] on a given LTS (S, T ) which is similar to the game hierarchy in [START_REF] Chen | Game characterizations of process equivalences[END_REF] and the well-known bisimulation game of [START_REF] Stirling | Modal and temporal logics for processes[END_REF].

The intuition of the game is as follows: The two players, with Player 1 starting the game, alternate to choose transitions, or moves, in T , starting with transitions from given start states s and t and continuing their choices from the targets of the transitions chosen in the previous step. At each of his turns, Player 1 also makes a choice whether to choose a transition from the target of his own previous choice, or from the target of his opponent's previous choice (to "switch paths"). We use a switch counter to keep track of how often Player 1 has chosen to switch paths. Player 2 has then to respond with a transition from the remaining target. This game is played for an infinite number of rounds, or until one player runs out of choices, thus building two finite or infinite paths. The value of the game is then the trace distance of the traces of these two paths.

We proceed to formalize the above intuition. A Player-1 configuration

of the game is a tuple (π, ρ, m) ∈ T n × T n × ◆, for n ∈ ◆, such that for all i ∈ {0, . . . , n -2}, either src(π i+1 ) = tgt(π i ) and src(ρ i+1 ) = tgt(ρ i ), or src(π i+1 ) = tgt(ρ i ) and src(ρ i+1 ) = tgt(π i ). Similarly, a Player-2 configuration is a tuple (π, ρ, m) ∈ T n+1 × T n × ◆ such that for all i ∈ {0, . . . , n -2}, either src(π i+1 ) = tgt(π i ) and src(ρ i+1 ) = tgt(ρ i ), or src(π i+1 ) = tgt(ρ i ) and src(ρ i+1 ) = tgt(π i ); and src(π n ) = tgt(π n-1 ) or src(π n ) = tgt(ρ n-1
). The set of all Player-i configurations is denoted Conf i . Intuitively, the configuration (π, ρ, m) keeps track of the history of the game; π stores the choices of Player 1, ρ the choices of Player 2, and m is the switch counter. Hence π and ρ are sequences of transitions in T which can be arranged by suitable swapping to form two paths (π,ρ). How exactly these sequences are constructed is determined by a pair of strategies which specify for each player which edge to play from any configuration.

A Player-1 strategy is hence a partial mapping θ 1 :

Conf 1 → T × ◆ such that for all (π, ρ, m) ∈ Conf 1 for which θ 1 (π, ρ, m) = (e ′ , m ′ ) is defined, • src(e ′ ) = tgt(last(π)) and m ′ = m or m ′ = m + 1, or • src(e ′ ) = tgt(last(ρ)) and m ′ = m + 1. A Player-2 strategy is a partial mapping θ 2 : Conf 2 → T × ◆ such that for all (π • e, ρ, m) ∈ Conf 2 for which θ 2 (π • e, ρ, m) = (e ′ , m ′ ) is defined, m ′ = m, and src(e ′ ) = tgt(last(ρ)) if src(e) = tgt(last(π)), src(e ′ ) = tgt(last(π)) if src(e) = tgt(last(ρ)).
The sets of Player-1 and Player-2 strategies are denoted Θ 1 and Θ 2 .

Note that if Player 1 chooses a transition from the end of the previous choice of Player 2 (case src(e ′ ) = tgt(last(ρ)) above), then the switch counter is increased; but Player 1 may also choose to increase the switch counter without switching paths. Player 2 does not touch the switch counter.

We can now define what it means to update a configuration according to a strategy: For

θ 1 ∈ Θ 1 and (π, ρ, m) ∈ Conf 1 , upd θ1 (π, ρ, m) is defined if θ 1 (π, ρ, m) = (e ′ , m ′ ) is defined, and then upd θ1 (π, ρ, m) = (π•e ′ , ρ, m ′ ). Similarly, for θ 2 ∈ Θ 2 and (π • e, ρ, m) ∈ Conf 2 , upd θ2 (π • e, ρ, m) is defined if θ 2 (π • e, ρ, m) = (e ′ , m ′ ) is defined, and then upd θ2 (π • e, ρ, m) = (π • e, ρ • e ′ , m ′ ).
For any pair of states (s, t) ∈ S × S, a pair of strategies (θ 1 , θ 2 ) ∈ Θ 1 × Θ 2 inductively determines a sequence (π j , ρ j , m j ) of configurations, by

(π 0 , ρ 0 , m 0 ) = (s, t, 0); (π 2j+1 , ρ 2j+1 , m 2j+1 ) = undefined if upd θ1 (π 2j , ρ 2j , m 2j ) is undefined, upd θ1 (π 2j , ρ 2j , m 2j ) otherwise; (π 2j , ρ 2j , m 2j ) =      undefined if upd θ2 (π 2j-1 , ρ 2j-1 , m 2j-1 ) is undefined, upd θ2 (π 2j-1 , ρ 2j-1 , m 2j-1 ) otherwise.
Note that indeed, we are updating configurations by alternating between the two strategies θ 1 , θ 2 . The configurations in this sequence satisfy π j ⊑ π j+1 , ρ j ⊑ ρ j+1 for all j, where ⊑ denotes prefix ordering, hence the limits π = lim -→ π j , ρ = lim -→ ρ j exist (as infinite paths). By our conditions on configurations, the pair (π, ρ) in turn determines a pair (π, ρ) of paths in S, as follows:

(π 1 , ρ1 ) = (π 1 , ρ 1 ) if src(π 1 ) = s (ρ 1 , π 1 ) if src(π 1 ) = t (π j , ρj ) = (π j , ρ j ) if src(π j ) = tgt(π j-1 ) (ρ j , π j ) if src(π j ) = tgt(ρ j-1 )
The outcome of the game when played from (s, t) according to a strategy pair (θ 1 , θ 2 ) is defined to be out(θ 1 , θ 2 )(s, t) = (π, ρ), and its utility is defined by

util(θ 1 , θ 2 )(s, t) = d T (tr(out(θ 1 , θ 2 )(s, t))) = d T (tr(π), tr(ρ)).
Recall that d T is given as a parameter to the game; if we want to make explicit the parametrization on the trace distance d T which utility depends on, we write util d T (θ 1 , θ 2 )(s, t).

Note that util(θ 1 , θ 2 )(s, t) is defined both in case the paths π and ρ are finite and in case they are infinite (the case where one is finite and the other is infinite cannot occur). Also, if the paths are finite because θ 1 (π j , ρ j , m j ) was undefined for some configuration (π j , ρ j , m j ) in the sequence, then π and ρ have the same length; if on the other hand the reason is that θ 2 (π j , ρ j , m j ) was undefined, then the paths have different length, and util(θ 1 , θ 2 )(s, t) = ∞. Hence if the game reaches a configuration in which Player 2 has no moves available, the utility is ∞.

The objective of Player 1 in the game is to maximize utility, whereas Player 2 wants to minimize it. Hence we define the value of the game from (s, t) to be

v(s, t) = sup θ1∈Θ1 inf θ2∈Θ2 util(θ 1 , θ 2 )(s, t) .
For a given subset Θ ′ 1 ⊆ Θ 1 we will write

v(Θ ′ 1 )(s, t) = sup θ1∈Θ ′ 1 inf θ2∈Θ2 util(θ 1 , θ 2 )(s, t) ,
and if we need to emphasize dependency of the value on the given trace distance, we write v(d T , Θ ′ 1 ). The following lemma states the immediate fact that if Player 1 has fewer strategies available, the game value decreases.

Lemma 1. For all Θ ′ 1 ⊆ Θ ′′ 1 ⊆ Θ 1 and all s, t ∈ S, v(Θ ′ 1 )(s, t) ≤ v(Θ ′′ 1 )(s, t).
We introduce two technical conditions on strategies and on trace distances. We say that a strategy

θ 1 ∈ Θ 1 is uniform if it holds for all configurations (π, ρ, m), (π, ρ ′ , m), (π ′ , ρ, m) ∈ Conf 1 that whenever θ 1 (π, ρ, m) = (e ′ , m ′ ) is defined,
• if src(e ′ ) = tgt(π), then also θ 1 (π, ρ ′ , m) is defined, and

• if src(e ′ ) = tgt(ρ), then also θ 1 (π ′ , ρ, m) is defined.
Uniformity of strategies is used to combine paths built from different starting states in the proof of Proposition 3 below. A subset

Θ ′ 1 ⊆ Θ 1 is uniform if all strategies in Θ ′
1 are uniform; the concrete strategy subsets we will consider in later sections will all be uniform.

We say that a pair

(Θ ′ 1 , d T ) of a strategy subset Θ ′ 1 ⊆ Θ 1 and a trace distance is well-behaved if sup θ1∈Θ ′ 1 inf θ2∈Θ2 util(θ 1 , θ 2 )(s, t) = inf θ2∈Θ2 sup θ1∈Θ ′ 1 util(θ 1 , θ 2 )(s, t)
for all s, t ∈ S. This assumption is related to determinacy of the quantitative path-building game, asserting that each pair of states has a value. We will need well-behavedness in our proof of Proposition 3 below; whether a pair (Θ ′ 1 , d T ) is well-behaved depends on both Θ ′ 1 and d T , and to consider any necessary or sufficient conditions for well-behavedness for concrete strategy subsets or concrete trace distances is beyond the scope of this paper.

However, we will later see that for the important special case where the trace distance d T is given by a recursive characterization, cf. Section 7, another, simpler proof may be given for Proposition 3 which does not need well-behavedness.

Remark 1. The type of games we have defined here are Blackwell games as introduced in [START_REF] Blackwell | Infinite G δ games with imperfect information[END_REF]; note however that we do not need randomized strategies, as our games are turn-based. In [START_REF] Martin | The determinacy of Blackwell games[END_REF], it is shown that all Borel Blackwell games are determined, and that also for other aspects, the situation is similar to the one for infinite games with qualitative objectives [START_REF] Martin | Borel determinacy[END_REF]. In particular, determinacy for any interesting bigger class than Borel Blackwell games is not provable in Zermelo-Fränkel set theory including the axiom of choice.

General Properties

We show here that under certain conditions, the game value is indeed a distance, and that results concerning inequalities in the qualitative dimension can be transfered to topological inequivalences in the quantitative setting. Say that a Player-1 strategy θ 1 ∈ Θ 1 is non-switching if it holds for all (π, ρ, m) for which θ 1 (π, ρ, m) = (e ′ , m ′ ) is defined that m = m ′ , and let Θ 0 1 be the set of non-switching Player-1 strategies. We first show a lemma which shows that any pair of traces can be generated by a non-switching strategy: Lemma 2. For all s, t ∈ S and all σ ∈ Tr(s), τ ∈ Tr(t) there exist θ 1 ∈ Θ 0 1 and

θ 2 ∈ Θ 2 for which util(θ 1 , θ 2 )(s, t) = d T (σ, τ ). Proof. Let (π, ρ, 0) ∈ Conf 1 for finite paths π, ρ with len(π) = len(ρ) = k ≥ 0 and tr(π) = σ 0 . . . σ k-1 , tr(ρ) = τ 0 . . . τ k-1 . If len(σ) ≥ k,
then there is e = (last(π), σ k , s ′ ) ∈ T , and we define θ 1 (π, ρ, 0) = (e, 0). If also len(τ ) ≥ k, then there is e ′ = (last(ρ), τ k , t ′ ) ∈ T , and we let θ 2 (π • e, ρ, 0) = (e ′ , 0).

Let (π, ρ) = out(θ 1 , θ 2 )(s, t). If both σ and τ are infinite paths, then tr(π) = σ and tr(ρ) = τ ; otherwise, tr(π) and tr(ρ) will be finite prefixes of σ and τ for which d T (tr(π), tr(ρ)) = d T (σ, τ ).

The following proposition shows under which conditions we can expect the distance defined by our quantitative game to be a hemimetric. Well-behavednes is used in the proof of the triangle inequality.

Proposition 3. If Θ ′ 1 ⊆ Θ 1 is uniform and Θ 0 1 ⊆ Θ ′ 1 , and if (Θ ′ 1 , d T ) is well- behaved, then v(Θ ′
1 ) is a hemimetric on S.

Proof. We write v = v(Θ ′ 1 ) during this proof. It is clear that v(s, s) = 0 for all s ∈ S: if the players are making their choices from the same state, Player 2 can always answer by choosing exactly the same transition as Player 1. For proving the triangle inequality v(s, u) ≤ v(s, t) + v(t, u), let ε > 0 and use well-behavedness of d T to choose Player-2 strategies θ s,t 2 , θ t,u 2 ∈ Θ 2 for which

sup θ1∈Θ ′ 1 util(θ 1 , θ s,t 2 )(s, t) < v(s, t) + ε 2 , sup θ1∈Θ ′ 1 util(θ 1 , θ t,u 2 )(t, u) < v(t, u) + ε 2 .
(

) 1
We define a strategy θ s,u 2 ∈ Θ 2 which uses three paths and two configurations in S as extra memory. This is only for convenience, as these can be reconstructed by Player 2 at any time; hence we do not extend the capabilities of Player 2:

θ s,u 2 (π • e, χ, m; π, ρ′ , χ, π ′ , ρ ′ 1 , ρ ′ 2 , χ ′ ) =                                                                    θ t,u 2 ρ ′ 2 • θ s,t 2,1 (π ′ • e, ρ ′ 1 , m), χ ′ , m ; π • e, ρ′ • θ s,t 2,1 (π ′ • e, ρ ′ 1 , m), χ • θ t,u 2,1 ρ ′ 2 • θ s,t 2,1 (π ′ • e, ρ ′ 1 , m) , π ′ • e, ρ ′ 1 • θ s,t 2,1 (π ′ • e, ρ ′ 1 , m), ρ ′ 2 • θ s,t 2,1 (π ′ • e, ρ ′ 1 , m), χ ′ • θ t,u 2,1 ρ ′ 2 • θ s,t 2,1 (π ′ • e, ρ ′ 1 , m) if src(e) = tgt(last(π)), θ s,t 2 π ′ • θ t,u 2,1 (ρ ′ 2 • e, χ ′ , m), ρ ′ 1 , m ; π • θ s,t 2,1 π ′ • θ t,u 2,1 (ρ ′ 2 • e, χ ′ , m) , ρ′ • θ t,u 2,1 (ρ ′ 2 • e, χ ′ , m), χ • e, π ′ • θ t,u 2,1 (ρ ′ 2 • e, χ ′ , m), ρ ′ 1 • θ s,t 2,1 π ′ • θ t,u 2,1 (ρ ′ 2 • e, χ ′ , m) ρ ′ 2 • e, χ ′ • θ t,u 2,1 (ρ ′ 2 • e, χ ′ , m) if src(e) = tgt(last( χ)).
In the beginning of the game, all memory paths are initialized to be empty. In the expression above, the strategy θ s,u 2 is constructed from the strategies θ s,t 2 and θ t,u 2 by using the answer to the move of Player 1 in one of the games as an emulated Player-1 move in the other. The paths π, χ are constructed from the configuration (π, χ) of the (s, u)-game and are only kept in memory so that we can see whether Player 1 is playing an edge prolonging π or χ. The pair (π ′ , ρ ′ 1 ) is the configuration in the (s, t)-game we are emulating, and (ρ ′ 2 , χ ′ ) is the (t, u)-configuration. The path ρ′ = ρ′ 1 = ρ′ 2 is common for the paths (π ′ , ρ′ 1 ), (ρ ′ 2 , χ′ ) constructed from (π ′ , ρ ′ 1 ) and (ρ ′ 2 , χ ′ ). If Player 1 has played an edge e prolonging π (first case above), we compute an answer move (e ′ , m) = θ s,t 2 (π ′ • e, ρ ′ 1 , m) to this in the (s, t)-game. This answer is then used to emulate a Player-1 move in the (t, u)-game, and the answer θ t,u 2 (ρ ′ 2 • e ′ , χ ′ , m) to this is what Player 2 plays in the (s, u)-game. The memory is updated accordingly. If on the other hand, Player 1 has played an edge e prolonging χ, we play in the (t, u)-game first and use the answer

(e ′ , m) = θ t,u 2 (ρ ′ 2 •e, χ ′ , m) in the (s, t)-game to compute θ s,t 2 (π ′ •e ′ , ρ ′ 1 , m). Figure 2
gives an illustration of how the configurations are updated during the game; note that uniformity of Θ ′ 1 is necessary for being able to emulate Player-1 moves from one game in another.

Take now any θ s,u

1 ∈ Θ ′ 1 , let (π, χ) = out(θ s,u 1 , θ s,u 2
)(s, u), and let ρ′ be the corresponding memory path. By Lemma 2 there exist θ s,t 1 , θ t,u Using Equation (1) we have

1 ∈ Θ ′ 1 for which d T (tr(π), tr(ρ ′ )) = util(θ s,t 1 , θ s,t 2 )(s, t) and d T (tr(ρ ′ ), tr( χ)) = util(θ t,u 1 , θ t,u 2 )(t, u). s t u π π π π χ χ χ χ π ′ π ′ π ′ π ′ ρ ′ 1 ρ ′ 1 ρ ′ 1 ρ ′ 1 ρ ′ 2 ρ ′ 2 ρ ′ 2 ρ ′ 2 χ ′ χ ′ χ ′ χ ′
util(θ s,u 1 , θ s,u 2 )(s, u) = d T (tr(π), tr( χ)) ≤ d T (tr(π), tr(ρ)) + d T (tr(ρ), tr( χ)) < v(s, t) + v(t, u) + ε and hence also inf θ2∈Θ2 util(θ s,u 1 , θ 2 )(s, u) < v(s, t) + v(t, u) + ε.
As the choice of θ s,u 1 was arbitrary, this implies

sup θ1∈Θ ′ 1 inf θ2∈Θ2 util(θ 1 , θ 2 )(s, u) ≤ v(s, t) + v(t, u) + ε ,
and as also ε was chosen arbitrarily, we have v(s, u) ≤ v(s, t) + v(t, u).

Next we show a transfer principle which allows us to generalize counterexamples regarding the equivalences in the qualitative linear-time-branching-time spectrum [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF] to the qualitative setting. We will make use of this principle later to show that all distances we introduce are topologically inequivalent.

Lemma 4. Let Θ ′ 1 , Θ ′′ 1 ⊆ Θ 1 ,
v(d T disc , Θ ′ 1 )(s, t) = 0 and v(d T disc , Θ ′′ 1 )(s, t) = ∞, then v(d T , Θ ′ 1 ) and v(d T , Θ ′′ 1 ) are topologically inequivalent. Proof. By v(d T disc , Θ ′ 1 )(s, t) = 0, we know that for any θ 1 ∈ Θ ′ 1 there exists θ 2 ∈ Θ 2 for which (π, ρ) = out(θ 1 , θ 2 )(s, t) satisfy tr(π) = tr(ρ), hence also v(d T , Θ ′ 1 )(s, t) = 0.
Conversely, and as d T is separating, v(d T , Θ ′′ 1 )(s, t) = 0 would imply that also v(d T disc , Θ ′′ 1 )(s, t) = 0, hence we must have v(d T , Θ ′′ 1 )(s, t) = 0, entailing topological inequivalence.

The Distance Spectrum

In this section we introduce the distances depicted in Figure 1 and show their relationship. Note again that the results obtained here are independent of the particular trace distance considered; in the terminology of the introduction we are developing a linear-time-branching-time spectrum at every point of the quantitative dimension. In order to capture the remaining relations in the original spectrum, we may easily adopt the approach from [START_REF] Chen | Game characterizations of process equivalences[END_REF] which imposes one of three extra conditions which Player 1 may choose to invoke and thereby terminate the game.

Throughout this section, we fix a LTS (S, T ⊆ S ×❑×S) and a trace distance

d T : ❑ ∞ × ❑ ∞ → | ≥0 ∪ {∞}.

Branching Distances

If the switching counter in the game introduced in Section 4 is unbounded, Player 1 can choose at any move whether to prolong the previous choice or to switch paths, hence this resembles the bisimulation game [START_REF] Stirling | Modal and temporal logics for processes[END_REF].

Definition 5. The bisimulation distance between s and t is d bisim (s, t) = v(s, t). Theorem 6. For d T = d T disc the discrete trace distance, d bisim disc (s, t) = 0 if, and only if, s and t are bisimilar.

Proof. By discreteness of d T disc , we have d bisim disc (s, t) = 0 if, and only if, it holds that for all θ 1 ∈ Θ 1 there exists θ 2 ∈ Θ 2 for which util(θ 1 , θ 2 )(s, t) = 0. Hence for each reachable Player-1 configuration (π, ρ, m) with θ 1 (π, ρ, m) = (e ′ , m ′ ), we have θ 2 (π • e ′ , ρ, m ′ ) = (e ′′ , m ′ ) with tr(e ′ ) = tr(e ′′ ), i.e. Player 2 matches the labels chosen by Player 1 precisely, implying that s and t are bisimilar. The proof of the other direction is trivial.

We can restrict the strategies available to Player 1 by allowing only a predefined finite number of switches:

Θ k-sim 1 = {θ 1 ∈ Θ 1 | if θ 1 (π, ρ, m) = (e ′ , m ′ ) is defined, then m ′ ≤ k -1}
In the so-defined k-nested simulation game, Player 1 is only allowed to switch paths k -1 times during the game. Note that Θ 1-sim 1 = Θ 0 1 is the set of nonswitching strategies. Definition 7. The k-nested simulation distance from s to t, for k ∈ ◆ + , is

d k-sim (s, t) = v(Θ k-sim 1 )(s, t). The k-nested simulation equivalence distance be- tween s and t is d k-sim-eq (s, t) = max(v(Θ k-sim 1 )(s, t), v(Θ k-sim 1 )(t, s)). Theorem 8. For d T = d T disc the discrete trace distance, • d k-sim
disc (s, t) = 0 if, and only if, there is a k-nested simulation from s to t,

• d k-sim-eq disc (s, t) = 0 if, and only if, there is a k-nested simulation equivalence between s and t.

Especially, d 1-sim disc corresponds to the usual simulation preorder, and d 2-sim disc to nested simulation. Similarly, d 1-sim-eq disc is similarity, and d 2-sim-eq disc is nested similarity. We refer to [START_REF] Friso Groote | Structured operational semantics and bisimulation as a congruence[END_REF][START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] for definitions and discussion of nested and k-nested simulations.

Proof. This is similar to the proof of Theorem 6: If d k-sim disc (s, t) = 0, then any θ 1 ∈ Θ k-sim 1 has a counter-strategy θ 2 ∈ Θ 2 which matches the labels chosen by Player 1 precisely, implying k-nested simulation from s to t. The other direction is again trivial. Theorem 9. For all k, ℓ ∈ ◆ + with k < ℓ and all s, t ∈ S, d k-sim-eq (s, t) ≤ d ℓ-sim (s, t) ≤ d ℓ-sim-eq (s, t) ≤ d bisim (s, t).

If the trace distance d T is separating and, together with the involved strategy subsets, well-behaved, then all distances above are topologically inequivalent.

Proof. The first part of the theorem follows from Θ k-sim-eq 1 ⊆ Θ ℓ-sim 1 ⊆ Θ ℓ-sim-eq 1 ⊆ Θ 1 and Lemma 1. Topological inequivalence follows from Lemma 4 and the fact that for the discrete relations corresponding to the distances above (obtained by letting d T = d T disc ), the inequalities are strict [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF]. As a variation of k-nested simulation, we can consider strategies which allow Player 1 to switch paths k times during the game, but at the last switch, he may only pose one transition as a challenge, to which Player 2 must answer, and then the game finishes:

Θ k-rsim 1 = {θ 1 ∈ Θ 1 | if θ 1 (π, ρ, m) is defined, then m ≤ k -1}
Hence after his kth switch, Player 1 has no more moves available, and the game finishes after the answer move of Player 2. Again, we allow Player 1 to increase the switch counter without actually switching paths.

Definition 10. The k-nested ready simulation distance from s to t, for k ∈ ◆ + , is d k-rsim (s, t) = v(Θ k-rsim 1 )(s, t). The k-nested ready simulation equivalence distance between s and t is d k-rsim-eq (s, t) = max(v(Θ k-rsim 1 )(s, t), v(Θ k-rsim 1 )(t, s)).

For the discrete case, it seems only the case k = 1 has been considered; the proof is similar to the one of Theorem 6.

Theorem 11. For d T = d T disc the discrete trace distance, • d 1-rsim disc (s, t) = 0 if, and only if, there is a ready simulation from s to t, • d 1-rsim-eq disc (s, t) = 0 if, and only if, s and t are ready simulation equivalent.

The next theorem finishes our work on the right half of Figure 1.

Theorem 12. For all k, ℓ ∈ ◆ + with k < ℓ and all s, t ∈ S,

d k-sim (s, t) ≤ d k-rsim (s, t) ≤ d ℓ-sim (s, t) , d k-sim-eq (s, t) ≤ d k-rsim-eq (s, t) ≤ d ℓ-sim-eq (s, t) .
Additionally, d k-rsim and d k-sim-eq are incomparable, and also d k-rsim-eq and d (k+1)-sim are incomparable. If the trace distance d T is separating and, together with the involved strategy subsets, well-behaved, then all distances above are topologically inequivalent.

Proof. Like in the proof of Theorem 9, the inequalities follow from strategy set inclusions and topological inequivalence from Lemma 4. The incomparability results follow from the corresponding results for d T disc and Lemma 4.

Linear Distances

Above we have introduced the distances in the right half of the quantitative linear-time-branching-time spectrum in Figure 1 and shown the relations claimed in the diagram. To develop the left half, we need the notion of blind strategies. For any subset Θ ′ 1 ⊆ Θ 1 we define the set of blind Θ ′ 1 -strategies by

Θ′ 1 = {θ 1 ∈ Θ ′ 1 | ∀π, ρ, ρ ′ , m : θ 1 (π, ρ, m) = θ 1 (π, ρ ′ , m), or θ 1 (π, ρ, m) = (e, m + 1) and tgt(last(ρ)) = tgt(last(ρ ′ ))}.
Hence in such a blind strategy, either the edge chosen by Player 1 does not depend on the choices of Player 2, or the switch counter is increased, in which case the Player-1 choice only depends on the target of the last choice of Player 2 (note that this dependency is necessary if Player 1 wants to switch paths). Now we can define, for s, t ∈ S and k ∈ ◆ + ,

• the ∞-nested trace equivalence distance: d ∞-trace-eq (s, t) = v( Θ1 )(s, t),

• the k-nested trace distance:

d k-trace (s, t) = v( Θk-sim 1 )(s, t),
• the k-nested trace equivalence distance: d k-trace-eq (s, t) = max(v( Θk-sim )(s, t), v( Θk-sim 1 )(t, s)),

• the k-nested ready distance:

d k-ready (s, t) = v( Θk-rsim 1
)(s, t), and

• the k-nested ready equivalence distance: d k-ready-eq (s, t) = max(v( Θk-rsim )(s, t), v( Θk-rsim 1 )(t, s)).

Our approach is justified by the following lemma which shows that the (1nested) trace distance from s to t is precisely the Hausdorff distance between the sets of traces available from s and t, respectively. Lemma 13. For s, t ∈ S, d 1-trace (s, t) = sup σ∈Tr(s) inf τ ∈Tr(t) d T (σ, τ ).

Proof. We have d 1-trace (s, t) = v( Θ0 1 )(s, t), with Θ0 1 = {θ 1 ∈ Θ 0 1 | ∀π, ρ, ρ ′ , m : θ 1 (π, ρ, m) = θ 1 (π, ρ ′ , m)}.
Hence, and as strategies in Θ 0 1 are non-switching, every strategy θ 1 ∈ Θ0

1 gives rise to precisely one trace σ = σ(θ 1 ) ∈ Tr(s) independently of Player-2 strategy θ 2 ∈ Θ 2 . Conversely, by Lemma 2 (noticing that indeed, we have constructed a blind Player-1 strategy in the proof of that lemma), every trace σ ∈ Tr(s) is generated by a strategy θ 1 ∈ Θ0

1 with σ = σ(θ 1 ). We can finish the proof by showing that for all

θ 1 ∈ Θ0 1 , inf θ2∈Θ2 d T (σ(θ 1 ), tr(ρ(θ 1 , θ 2 ))) = inf τ ∈Tr(t) d T (σ(θ 1 ), τ ) .
But again using Lemma 2, we see that any τ ∈ Tr(t) is generated by a strategy θ 2 ∈ Θ 2 , hence this is clear.

Using the discrete trace distance, we recover the following standard relations [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF]. The theorem follows by Lemma 13 and arguments similar to the ones used in the proofs of the corresponding theorems in the preceding section. We refer to [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF][START_REF] Rounds | Possible futures, acceptances, refusals, and communicating processes[END_REF] for definitions and discussion of possible-futures inclusion and equivalence.

Theorem 14. For d T = d T disc the discrete trace distance and s, t ∈ S we have • d 1-trace disc (s, t) = 0 if, and only if, there is a trace inclusion from s to t,

• d 1-trace-eq disc (s, t) = 0 if, and only if, s and t are trace equivalent,

• d 2-trace disc (s, t) = 0 if, and only if, there is a possible-futures inclusion from s to t,

• d 2-trace-eq disc (s, t) = 0 if, and only if, s and t are possible-futures equivalent,

• d 1-ready disc (s, t) = 0 if, and only if, there is a readiness inclusion from s to t,

• d 1-ready-eq disc (s, t) = 0 if, and only if, s and t are ready equivalent.

The following theorem entails all relations in the left side of Figure 1; the right-to-left arrows follow from the strategy set inclusions Θ′ 1 ⊆ Θ ′ 1 for any Θ ′ 1 ⊆ Θ 1 and Lemma 1. As with Theorems 9 and 12, the theorem follows by strategy set inclusion, Lemma 4, and corresponding results for the discrete relations.

Theorem 15. For all k, ℓ ∈ ◆ + with k < ℓ and s, t ∈ S, d k-trace-eq (s, t) ≤ d ℓ-trace (s, t) ≤ d ℓ-trace-eq (s, t) ≤ d ∞-trace-eq (s, t), d k-trace (s, t) ≤ d k-ready (s, t) ≤ d ℓ-trace (s, t), d k-trace-eq (s, t) ≤ d k-ready-eq (s, t) ≤ d ℓ-trace-eq (s, t).

Additionally, d k-ready and d k-trace-eq are incomparable, and also d k-ready-eq and d (k+1)-trace are incomparable. If the trace distance d T is separating and, together with the involved strategy subsets, well-behaved, then all distances above are topologically inequivalent.

Recursive Characterizations

We now turn our attention to an important special case in which the given trace distance has a specific recursive characterization; we show that in this case, all distances in the spectrum can be characterized as least fixed points. We will see in Section 8 that this can be applied to all examples of trace distances mentioned in Section 3.

Note that all theorems require the LTS in question to be finitely branching; this is a standard assumption which goes back to [START_REF] Stirling | Modal and temporal logics for processes[END_REF]. In most cases it may be relaxed to compact branching in the sense of [START_REF] Franck Van Breugel | A theory of metric labelled transition systems[END_REF], but to keep things simple, we do not do this here.

Fixed-Point Characterizations

Let L be a complete lattice with order ⊑ and bottom and top elements ⊥,

⊤. Let f : ❑ ∞ × ❑ ∞ → L, g : L → | ≥0 ∪ {∞}, F : ❑ × ❑ × L → L such that d T = g • f , g is monotone, F (x, y, •) : L → L is monotone for all x, y ∈ ❑, and
f (σ, τ ) =      F (σ 0 , τ 0 , f (σ 1 , τ 1 )) if σ, τ = ǫ, ⊤ if σ = ǫ, τ = ǫ or σ = ǫ, τ = ǫ, ⊥ if σ = τ = ǫ (2)
for all σ, τ ∈ ❑ ∞ .

We hence assume that d T has a recursive characterization (using F ) on top of an arbitrary lattice L which we introduce between ❑ ∞ and | ≥0 ∪ {∞} to serve as a memory. Below we will work with different endofunctions I on the set of mappings (◆ + ∪ {∞}) × {1, 2} → L S×S which are parametrized by the number m of switches in ◆ + ∪ {∞} which Player 1 has left, and a value p ∈ {1, 2} which keeps track of whether Player 1 currently is building the left or the right path.

Theorem 16. The endofunction I on (◆ + ∪ {∞}) × {1, 2} → L S×S defined by

I(h m,p )(s, t) =                                      max      sup s x -→s ′ inf t y -→t ′ F (x, y, h m,1 (s ′ , t ′ )) sup t y -→t ′ inf s x -→s ′ F (x, y, h m-1,2 (s ′ , t ′ )) if m ≥ 2, p = 1 sup s x -→s ′ inf t y -→t ′ F (x, y, h m,1 (s ′ , t ′ )) if m = 1, p = 1 max      sup t y -→t ′ inf s x -→s ′ F (x, y, h m,2 (s ′ , t ′ )) sup s x -→s ′ inf t y -→t ′ F (x, y, h m-1,1 (s ′ , t ′ )) if m ≥ 2, p = 2 sup t y -→t ′ inf st x -→s ′ F (x, y, h m,2 (s ′ , t ′ )) if m = 1, p = 2
has a least fixed point h * : (◆ + ∪ {∞}) × {1, 2} → L S×S , and if the LTS (S, T ) is finitely branching, then

d k-sim = g • h * k,1 , d k-sim-eq = g • max(h * k,1 , h * k,2 ) for all k ∈ ◆ + ∪ {∞}.
Hence I iterates the function h over the branching structure of (S, T ), computing all nested branching distances at the same time. Note the specialization of this to simulation and bisimulation distance, where we have the following fixed-point equations, using h * 1,1 = h 1-sim and h * ∞,1 = h bisim :

h 1-sim (s, t) = sup s x -→s ′ inf t y -→t ′ F (x, y, h 1-sim (s ′ , t ′ )) h bisim (s, t) = max      sup s x -→s ′ inf t y -→t ′ F (x, y, h bisim (s ′ , t ′ )) sup t y -→t ′ inf s x -→s ′ F (x, y, h bisim (s ′ , t ′ ))
Proof. The lattice of mappings (◆ + ∪{∞})×{1, 2} → L S×S with the point-wise partial order is complete, and I is monotone because F is, so by Tarski's fixedpoint theorem, I has indeed a least fixed point h * . To show that

d k-sim = g • h * k,1
for all k, we pull back d k-sim along g: Define w :

(◆ + ∪ {∞}) × {1, 2} → L S×S by w k,1 (s, t) = sup θ1∈Θ k-sim 1 inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(s, t))) w k,2 (s, t) = sup θ1∈Θ k-sim 1 inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(t, s))) then d k-sim = g • f (k, 1
) for all k by monotonicity of g. We will be done once we can show that w = h * . We first show that w is a fixed point for I. Let s, t ∈ S, then (assuming k ≥ 2)

I(w k,1 )(s, t) = max      sup s x -→s ′ inf t y -→t ′ F (x, y, w k,1 (s ′ , t ′ )) sup t y -→t ′ inf s x -→s ′ F (x, y, w k-1,2 (s ′ , t ′ )) = max        sup s x -→s ′ inf t y -→t ′ F (x, y, sup θ1∈Θ k-sim 1 inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(s ′ , t ′ )))) sup t y -→t ′ inf s x -→s ′ F (x, y, sup θ1∈Θ (k-1)-sim 1 inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(t ′ , s ′ )))) = max        sup s x -→s ′ inf t y -→t ′ sup θ1∈Θ k-sim 1 inf θ2∈Θ2 F (x, y, f (tr(out(θ 1 , θ 2 )(s ′ , t ′ )))) sup t y -→t ′ inf s x -→s ′ sup θ1∈Θ (k-1)-sim 1 inf θ2∈Θ2 F (x, y, f (tr(out(θ 1 , θ 2 )(t ′ , s ′ )))) = max              sup s x -→s ′ inf t y -→t ′ sup θ1∈Θ k-sim 1 inf θ2∈Θ2 f (x • tr(out 1 (θ 1 , θ 2 )(s ′ , t ′ )), y • tr(out 2 (θ 1 , θ 2 )(s ′ , t ′ ))) sup t y -→t ′ inf s x -→s ′ sup θ1∈Θ (k-1)-sim 1 inf θ2∈Θ2 f (x • tr(out 1 (θ 1 , θ 2 )(t ′ , s ′ )), y • tr(out 2 (θ 1 , θ 2 )(t ′ , s ′ ))) ,
the next-to-last step by monotonicity of F . Now the choices of t y -→ t ′ and θ 1 ∈ Θ k-sim 1 do not depend on each other, so the corresponding inf and sup can be exchanged, whence

I(w k,1 )(s, t) = max              sup s x -→s ′ sup θ1∈Θ k-sim 1 inf t y -→t ′ inf θ2∈Θ2 f (x • tr(out 1 (θ 1 , θ 2 )(s ′ , t ′ )), y • tr(out 2 (θ 1 , θ 2 )(s ′ , t ′ ))) sup t y -→t ′ sup θ1∈Θ (k-1)-sim 1 inf s x -→s ′ inf θ2∈Θ2 f (x • tr(out 1 (θ 1 , θ 2 )(t ′ , s ′ )), y • tr(out 2 (θ 1 , θ 2 )(t ′ , s ′ ))) = max        sup θ1∈Θ k-sim 1,ns inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(s, t))) sup θ1∈Θ k-sim 1,s inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(s, t))) = w k,1 (s, t).
In the last max expression, Θ k-sim 1,ns ⊆ Θ k-sim

1
is the subset of Player-1 strategies θ 1 which do not switch from the configuration (s, t, 0), i.e. for which src(θ 1,1 (s, t, 0)) = s, and Θ k-sim

1,s = Θ k-sim 1 \ Θ k-sim
1,ns consists of the strategies which do switch from (s, t, 0). The other cases in the definition of I -I(w 1,1 ), I(w 1,2 ), and I(w k,2 ) for k ≥ 2 -can be shown similarly, and we can conclude that I(w k,p ) = w k,p for all k ∈ ◆ + ∪ {∞}, p ∈ {1, 2}.

To show that w is the least fixed point for I, let h : (◆ + ∪ {∞}) × {1, 2} → L S×S be such that I( h) = h. We prove that w ≤ h, and again we show only the case w k,1 ≤ hk,1 for k ≥ 2. Note first that as the LTS (S, T ) is finitely branching, we can use the equation for I( hk,1 )(s, t) to conclude that for all s, t ∈ S, for any s x -→ s ′ there is t y -→ t ′ such that F (x, y, hk,1 (s ′ , t ′ )) ≤ I( hk,1 )(s, t),

for any t y -→ t ′ there is s x -→ s ′ such that F (x, y, hk-1,2 (s ′ , t ′ )) ≤ I( hk,1 )(s, t).

Now let θ 1 ∈ Θ k-sim

1

; the proof will be finished once we can find θ 2 ∈ Θ 2 for which f (tr(out(θ 1 , θ 2 )(s, t))) ≤ hk,1 (s, t). Let (π • e, ρ, m) ∈ Conf 2 and write s = tgt(last(π)), t = tgt(last(ρ)). Assume first that e = (s, x, s ′ ), let t = tgt(last(ρ)) and e = (t, y, t ′ ) an edge which satisfies the inequality of Equation (3), and define θ 2 (π • e, ρ, m) = (e ′ , m). For the so-defined Player-2 strategy θ 2 we have f (tr(out(θ 1 , θ 2 )(s, t))) ≤ sup s x -→s ′ inf t y -→t ′ F (x, y, hk,1 (s ′ , t ′ )) ≤ I( hk,1 )(s, t) = hk,1 (s, t) for all s, t ∈ S. The case e = (t, y, t ′ ) is shown similarly, using Equation ( 4) instead.

The fixed-point characterization for the ready simulation distances is similar (and so is its proof, which we hence omit):

Theorem 17. The endofunction I on (◆ + ∪ {∞}) × {1, 2} → L S×S defined by

I(h m,p )(s, t) =                                                    max      sup s x -→s ′ inf t y -→t ′ F (x, y, h m,1 (s ′ , t ′ )) sup t y -→t ′ inf s x -→s ′ F (x, y, h m-1,2 (s ′ , t ′ )) if m ≥ 2, p = 1 max      sup s x -→s ′ inf t y -→t ′ F (x, y, h m,1 (s ′ , t ′ )) sup t y -→t ′ inf s x -→s ′ f (x, y) if m = 1, p = 1 max      sup t y -→t ′ inf s x -→s ′ F (x, y, h m,2 (s ′ , t ′ )) sup s x -→s ′ inf t y -→t ′ F (x, y, h m-1,1 (s ′ , t ′ )) if m ≥ 2, p = 2 max      sup t y -→t ′ inf st x -→s ′ F (x, y, h m,2 (s ′ , t ′ )) sup s x -→s ′ inf t y -→t ′ f (x, y) if m = 1, p = 2
has a least fixed point h * : (◆ + ∪ {∞}) × {1, 2} → L S×S , and if the LTS (S, T ) is finitely branching, then

d k-rsim = g • h * k,1 , d k-rsim-eq = g • max(h * k,1 , h * k,2 ) for all k ∈ ◆ + ∪ {∞}.
For the linear distances, we extend F to a function

❑ n × ❑ n × L → L, for n ∈ ◆, by F (ǫ, ǫ, α) = α, F (x • σ, y • τ, α) = F (x, y, F (σ, τ, α)).
We also extend the -→ s ′ for some s ′′ ∈ S. We write s σ -→ if there is a (finite or infinite) trace σ from s. The proofs of the below theorems are similar to the one of Theorem 16.

Theorem 18. The endofunction I on (◆ + ∪ {∞}) × {1, 2} → L S×S defined by

I(h m,p )(s, t) =                                                    max              sup s σ -→ inf t τ -→ f (σ, τ ) sup s σ -→s ′ inf t τ -→t ′ F (σ, τ, h m-1,1 (s ′ , t ′ )) sup s σ -→s ′ inf t τ -→t ′ F (σ, τ, h m-1,2 (s ′ , t ′ )) if m ≥ 2, p = 1 sup s σ -→ inf t τ -→ f (σ, τ ) if m = 1, p = 1 max              sup t τ -→ inf s σ -→ f (σ, τ ) sup t τ -→t ′ inf s σ -→s ′ F (σ, τ, h m-1,2 (s ′ , t ′ )) sup t τ -→t ′ inf s σ -→s ′ F (σ, τ, h m-1,1 (s ′ , t ′ )) if m ≥ 2, p = 2 sup t τ -→ inf s σ -→ f (σ, τ ) if m = 1, p = 2
has a least fixed point h * : (◆ + ∪ {∞}) × {1, 2} → L S×S , and if the LTS (S, T ) is finitely branching, then

d k-trace = g • h * k,1 , d k-trace-eq = g • max(h * k,1 , h * k,2 ) for all k ∈ ◆ + ∪ {∞}.
Theorem 19. The endofunction I on (◆ + ∪ {∞}) × {1, 2} → L S×S defined by

I(h m,p )(s, t) =                                                                                  max              sup s σ -→ inf t τ -→ f (σ, τ ) sup s σ -→s ′ inf t τ -→t ′ F (σ, τ, h m-1,1 (s ′ , t ′ )) sup s σ -→s ′ inf t τ -→t ′ F (σ, τ, h m-1,2 (s ′ , t ′ )) if m ≥ 2, p = 1 max              sup s σ -→ inf t τ -→ f (σ, τ ) sup s σ -→s ′ inf t τ -→t ′ sup s ′ x -→s ′′ inf t ′ y -→t ′′ f (σ • x, τ • y) sup s σ -→s ′ inf t τ -→t ′ sup t ′ y -→t ′′ inf s ′ x -→s ′′ f (σ • x, τ • y) if m = 1, p = 1 max              sup t τ -→ inf s σ -→ f (σ, τ ) sup t τ -→t ′ inf s σ -→s ′ F (σ, τ, h m-1,2 (s ′ , t ′ )) sup t τ -→t ′ inf s σ -→s ′ F (σ, τ, h m-1,1 (s ′ , t ′ )) if m ≥ 2, p = 2 max              sup t τ -→ inf s σ -→ f (σ, τ ) sup t τ -→t ′ inf s σ -→s ′ sup t ′ y -→t ′′ inf s ′ x -→s ′′ f (σ • x, τ • y) sup t τ -→t ′ inf s σ -→s ′ sup s ′ x -→s ′′ inf t ′ y -→t ′′ f (σ • x, τ • y) if m = 1, p = 2
has a least fixed point h * : (◆ + ∪ {∞}) × {1, 2} → L S×S , and if the LTS (S, T ) is finitely branching, then

d k-ready = g • h * k,1 , d k-ready-eq = g • max(h * k,1 , h * k,2 ) for all k ∈ ◆ + ∪ {∞}.
The fixed-point characterizations above have two important consequences. For the first, Proposition 3 easily follows by induction for distances with a fixed-point characterization, which means that the condition of well-behavedness is not needed to show the triangle inequality.

For the second, the fixed-point characterization immediately lead to iterative semi-algorithms for computing the respective distances: to compute e.g. simulation distance, we can initialize h 1-sim (s, t) = 0 for all states s, t ∈ S and then iteratively apply the above equality. This assumes the LTS (S, T ) to be finitely branching and uses Kleene's fixed-point theorem and continuity of F . However, this computation is only guaranteed to converge to simulation distance in finitely many steps in case the lattice L S×S is finite; otherwise, the procedure might not terminate.

Relation Families

Below we show that both simulation and bisimulation distance admit a relational characterization akin to the one of the standard Boolean notions. Using switching counters like we did in the previous section, this can easily be generalized to give relational characterizations to all distances in this paper.

Theorem 20. If the LTS (S, T ) is finitely branching, then d 1-sim (s, t) ≤ ε if, and only if, there exists a relation family R = {R α ⊆ S × S | α ∈ L} for which (s, t) ∈ R β ∈ R for some β with g(β) ≤ ε, and such that for any α ∈ L and for all (s

′ , t ′ ) ∈ R α ∈ R, • for all s ′ x -→ s ′′ , there exists t ′ y -→ t ′′ such that (s ′′ , t ′′ ) ∈ R α ′ ∈ R for some α ′ ∈ L with F (x, y, α ′ ) ⊑ α.
Similarly, d bisim (s, t) ≤ ε if, and only if, there exists a relation family R = {R α ⊆ S × S | α ∈ L} for which (s, t) ∈ R β ∈ R for some β with g(β) ≤ ε, and such that for any α ∈ L and for all (s ′ , t

′ ) ∈ R α ∈ R, • for all s ′ x -→ s ′′ , there exists t ′ y -→ t ′′ such that (s ′′ , t ′′ ) ∈ R α ′ ∈ R for some α ′ ∈ L with F (x, y, α ′ ) ⊑ α; • for all t ′ y -→ t ′′ , there exists s ′ x -→ s ′′ such that (s ′′ , t ′′ ) ∈ R α ′ ∈ R for some α ′ ∈ L with F (x, y, α ′ ) ⊑ α.
Proof. We only show the proof for simulation distance; for bisimulation distance it is analogous. Assume first that d 1-sim (s, t) ≤ ε, then we have h : S × S → L for which g(h(s, t)) ≤ ε and h(s ′ , t ′ ) = sup s x -→s ′ inf t y -→t ′ F (x, y, h(s ′′ , t ′′ )) for all s ′ , t ′ ∈ S. Let β = h(s, t), and define a relation family R

= {R α | α ∈ L} by R α = {(s ′ , t ′ ) | h(s ′ , t ′ ) ⊑ α}. Let α ∈ L and (s ′ , t ′ ) ∈ R α , then sup s x -→s ′ inf t y -→t ′ F (x, y, h(s ′′ , t ′′ )) = h(s ′ , t ′
) ⊑ α, and as (S, T ) is finitely branching, this implies that for all s ′ x -→ s ′′ there is t ′ y -→ t ′′ and α ′ = h(s ′′ , t ′′ ) such that (s ′′ , t ′′ ) ∈ R α ′ and F (x, y, α ′ ) ⊑ α.

For the other direction, assume a relation family as in the theorem and define h : S × S → L by h(s ′ , t ′ ) = inf{α | (s ′ , t ′ ∈ R α }. Then (s, t) ∈ R β implies that h(s, t) ⊑ β and hence g(h(s, t)) ≤ ε. Let s ′ , t ′ ∈ S, then (s ′ , t ′ ) ∈ R h(s ′ ,t ′ ) , hence for all s ′ x -→ s ′′ there is t ′ y -→ t ′′ and α ′ ∈ L for which F (x, y, α ′ ) ⊑ h(s ′ , t ′ ) and (s ′′ , t ′′ ) ∈ R α ′ , implying h(s ′′ , t ′′ ) ⊑ α ′ and hence F (x, y, h(s ′′ , t ′′ )) ⊑ h(s ′ , t ′ ). Collecting the pieces, we get I(h)(s ′ , t ′ ) = sup s ′ x -→s ′′ inf t ′ y -→t ′′ F (x, y, h(s ′′ , t ′′ )) ⊑ h(s ′ , t ′ ), hence h is a pre-fixed point for I. But then h * ⊑ h, hence d 1-sim (s, t) = g(h * (s, t)) ≤ g(h(s, t)) ≤ ε.

Recursive Characterizations for Example Distances

We show that the considerations in Section 7 apply to all the example distances we have introduced in Section 3. We apply Theorem 16 to derive fixed-point formulas for corresponding simulation distances, but of course all other distances in the quantitative linear-time-branching-time spectrum have similar characterizations.

Let d be a hemimetric on ❑, then for all σ, τ ∈ ❑ ∞ and 0 < λ ≤ 1, Incidentally, these are exactly the expressions introduced in [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Fahrenberg | A quantitative characterization of weighted Kripke structures in temporal logic[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF]. Also note that if S is finite with |S| = n, then undiscounted point-wise distance PW 1 (d) can only take on the finitely many values {d(x, y) | (s, x, s ′ ), (t, y, t ′ ) ∈ T }, hence the fixed-point algorithm given by Kleene's theorem converges in at most n 2 steps. This algorithm is used in [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF][START_REF] Desharnais | Approximate analysis of probabilistic processes[END_REF][START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF]. For undiscounted accumulating distance ACC 1 (d), it can be shown [START_REF] Kim | Metrics for weighted transition systems: Axiomatization and complexity[END_REF] that with D = max{d(x, y) | (s, x, s ′ ), (t, y, t ′ ) ∈ T }, distance is either infinite or bounded above by 2n 2 D, hence the ACC 1 (d) algorithm either converges in at most 2n 2 D steps or diverges.

For the limit-average distance AVG(d), we let L = (| ≥0 ∪ {∞}) ◆ , g(h) = lim inf j h(j), and f (σ, τ )(j) = 1 j+1 j i=0 d(σ i , τ i ) the j-th average. The intuition is that L is used for "remembering" how long in the traces we have progressed with the computation. With F given by F (x, y, h)(n) = 1 n+1 d(x, y)+ n n+1 h(n-1) it can be shown that (2) holds, giving the following fixed-point expression for limit-average simulation distance (which to the best of our knowledge is new):

h 1-sim n (s, t) = sup s x -→s ′ inf t y -→t ′ 1 n+1 d(x, y) + n n+1 h 1-sim n-1 (s ′ , t ′ )
For the maximum-lead distance, we let L = (| ≥0 ∪ {∞}) | , the lattice of mappings from leads to maximum leads. Using the notation from Section 3, we let g(h) = h(0) and f (σ, τ )(δ) = max(|δ|, sup j |δ + j i=0 σ w i -j i=0 τ w j |) the maximum-lead distance between σ and τ assuming that σ already has a lead of δ over τ . With F (x, y, h)(δ) = max(|δ + x -y|, h(δ + xy)) it can be shown that (2) holds, and then the fixed-point expression for maximum-lead simulation distance becomes the one given in [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF]: Again it can be shown [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF] that for S finite with |S| = n and D = max{d(x, y) | (s, x, s ′ ), (t, y, t ′ ) ∈ T }, the iterative algorithm for computing maximum-lead distance either converges in at most 2n 2 D steps or diverges.

h 1-sim (δ)(s, t) = sup
Regarding Cantor distance, a useful recursive formulation is

f (σ, τ )(n) = f (σ 1 , τ 1 )(n + 1) if σ 0 = τ 0 , n otherwise,
which iteratively counts the number of matching symbols in σ and τ . Here we use L = (| ≥0 ∪ {∞}) ◆ , and g(h) = 1 h(0) ; note that the order on L has to be reversed for g to be monotone. The fixed-point expression for Cantor simulation distance becomes

h 1-sim n (s, t) = max(n, sup s x -→s ′ inf t x -→t ′ h 1-sim n+1 (s ′ , t ′ ))
but as the order on L is reversed, the sup now means that Player 1 is trying to minimize this expression, and Player 2 tries to maximize it. Hence Player 2 tries to find maximal matching subtrees; the corresponding Cantor simulation equivalence distance between s and t hence is the inverse of the maximum depth of matching subtrees under s and t. The Cantor bisimulation distance in turn is the same as the inverse of bisimulation depth.

∞ 1 -nested ready inclusion ready inclusion 1 -nested trace equivalence trace equivalence 1 --nested simulation 1 -nested ready simulation ready simulation 1 -

 11111 -nested trace equivalence (k + 1)-nested ready inclusion (k + 1)-nested trace equivalence k-nested ready equivalence (k + 1)-nested trace inclusion k-nested ready inclusion k-nested trace equivalence 2-nested ready inclusion 2-nested trace equivalence possible-futures equivalence 1-nested ready equivalence ready equivalence 2-nested trace inclusion possible-futures inclusion nested trace inclusion trace inclusion ∞-nested simulation equivalence bisimulation (k + 1)-ready sim. equivalence (k + 1)-nested sim. equivalence k-nested ready sim. equivalence (k + 1)-nested simulation k-nested ready simulation k-nested sim. equivalence 2-nested ready simulation 2-nested sim. equivalence 1-nested ready sim. equivalence ready simulation equivalence 2nested sim. equivalence simulation equivalence 1-nested simulation simulation

Figure 1 :

 1 Figure 1: The quantitative linear-time-branching-time spectrum. The nodes are the different system distances introduced in this paper, and an edge d 1 -→ d 2 or d 1 d 2 indicates that d 1 (s, t) ≥ d 2 (s, t) for all states s, t, and that d 1 and d 2 in general are topologically inequivalent.

Figure 2 :

 2 Figure 2: Configuration update in the game used for showing the triangle inequality

1

 1

1

 1

x-→

  relation to finite traces so we can write s σ -→ s ′ below, by letting s ǫ -→ s for all s ∈ S and s x•σ -→ s ′ if, and only if, s x -→ s ′′ σ

  (σ 0 , τ 0 ), λ PW λ (d)(σ 1 , τ 1 )) if σ, τ = ǫ, ∞ if σ = ǫ, τ = ǫ or σ = ǫ, τ = ǫ, 0 if σ = τ = ǫ, ACC λ (d)(σ, τ ) = 0 , τ 0 ) + λ ACC λ (d)(σ 1 , τ 1 )) if σ, τ = ǫ, ∞ if σ = ǫ, τ = ǫ or σ = ǫ, τ = ǫ, 0 if σ = τ = ǫ,hence we can apply the iteration theorems with lattice L = | ≥0 ∪ {∞}, g = id the identity function, and the recursion function F given like the formulas above.Using Theorem 16 we can e.g. derive the following fixed-point expressions for simulation distance:PW λ (d) 1-sim (s, t) max(d(x, y), λ PW λ (d) 1-sim (s ′ , t ′ )) ACC λ (d) 1-sim (s, t) x, y) + λ ACC λ (d) 1-sim (s ′ , t ′ ))

  max(|δ + x -y|, h 1-sim (s ′ , t ′ )(δ + xy))

  and assume (Θ ′ 1 , d T ) and (Θ ′′ 1 , d T ) to be wellbehaved and d T to be separating. If there exist states s, t ∈ S for which


Uli Fahrenberg

Axel Legay

Configurable Formal Methods for Extreme Modeling Position Paper

Reliable model transformations are essential for agile modeling. We propose to employ a configurable-semantics approach to develop automatic model transformations which are correct by design and can be integrated smoothly into existing tools and work flows.

Model management is an essential activity in a model-driven development process. This is especially true in an agile context where models are continuously refined, iterated and combined.

It is a common misunderstanding that development by stepwise refinement, or use of component algebras, requires using a highly planned and waterfall-like development process. See for example the following quote: An important variant of the waterfall model is formal system development, where a mathematical model of a system specification is created. This model is then refined, using mathematical transformations that preserve its consistency, into executable code. Based on the assumption that your mathematical transformations are correct, you can therefore make a strong argument that a program generated in this way is consistent with its specification. [30, p.32] We will argue below that methods from model management and formal system development, when combined with and inspired by approaches originating in the area of formal interface and specification theories, can play an important role also in an agile context.

Within the context of model-driven engineering, automated model transformations such as merging, differencing and slicing are of great importance. This is especially true in the industrial context where models can easily get so large that the engineers only see them through viewpoints, or slices; indeed, an explicit system model may not even exist, so that the general model is only implicitly given as a collection of viewpoints.

When the system model is so complex that no single engineer has a comprehensive view, it can be very challenging to ensure correctness of an applied model transformation by inspection. (Even when the system model is less complex, ensuring correctness by inspection may be a difficult and error-prone process and require advanced tooling.) The use of model transformations which are correctby-design, or at least checkable-by-design, hence becomes increasingly important. This point of view has also been argued in [START_REF] Altmanninger | Models in conflict -towards a semantically enhanced version control system for models[END_REF][START_REF] Brunet | A manifesto for model merging[END_REF][START_REF] Maoz | A manifesto for semantic model differencing[END_REF][START_REF] Maoz | Semantically configurable consistency analysis for class and object diagrams[END_REF].

A good example is given by one of the case studies in the MERgE ITEA2 project [START_REF]MERgE ITEA2 project[END_REF]. This consists of a large system model with multiple (more than twenty) viewpoints, each detailing a different aspect of the model. The involved engineers are only working with the model through these viewpoints, as the whole model is too complex to be worked with directly. Now when a model transformation is applied to the model (e.g. a new subsystem is added through model merging), the engineers can inspect at their respective viewpoints whether, locally, the model transformation has been applied correctly. But can we be sure that this implies that the transformation is also globally correct? Can we design a procedure which allows such kind of local-to-global reasoning?

To put it succinctly, it is an important problem in model-driven engineering to ensure that model transformations are semantically correct or that, at least, their semantic correctness can be inferred by a combination of slicing and local inspection.

One basic model transformation is the one of differencing, i.e. assessing differences between models. This is an important ingredient in version control and essential in three-way merging, but can also be applied, more elementarily, to inspect related models for their common points and differences. Semantically correct differencing procedures, for class diagrams and activity diagrams respectively, have been proposed in [START_REF] Maoz | A manifesto for semantic model differencing[END_REF][START_REF] Maoz | ADDiff: Semantic differencing for activity diagrams[END_REF][START_REF] Maoz | CDDiff: Semantic differencing for class diagrams[END_REF]. However, these procedures rely on a complete, formal semantics of the modeling formalism in question, which for most cases is unrealistic: in practice, engineers use modeling tools which do not have a formal semantics, or where an existing formal semantics is too complex to be practically useful.

It is our point of view that any "bottom-up" approach to correct model transformations which uses a complete formal semantics as a starting point, such as the above-cited, is of doubtful use in practice. In practice, engineers develop models according to an intuitive understanding of how things work, and not according to a complete formal semantics (if indeed it exists at all).

Apart from being correct-by-design or checkable-by-design, we have also argued in [START_REF] Fahrenberg | Make a difference! (Semantically)[END_REF] that it is important that model transformations return an object of the same type as the inputs. Hence, the merge of two class diagrams, for instance, should again be a class diagram, the difference of two feature diagrams should again be a feature diagram, etc. This allows developers to visualize the transformation and to manipulate it using the usual tools for working with models; the transformation integrates smoothly into existing tools and work flows. Figure 1 shows an example of such a work flow which necessitates that the difference between two models is again a model of the same kind.

[ [START_REF] Maoz | A manifesto for semantic model differencing[END_REF][START_REF] Maoz | ADDiff: Semantic differencing for activity diagrams[END_REF][START_REF] Maoz | CDDiff: Semantic differencing for class diagrams[END_REF] propose semantic difference operators for class diagrams and activity diagrams, respectively, however, their approaches are enumerative in nature: their output is a (potentially infinite) list of object models which witness the difference between the input diagrams. The output language is thus different

M1 M2 M3 diff merge Fig. 1.
Example of a work flow where the changes ("diff") between models M1 and M2 are automatically applied ("merge") to M3. Note that a simplistic "diff" is not always the correct approach; it can be important to e.g., tell the difference between renaming an entity and a deletion followed by an addition. from the input language, which makes it impossible to integrate their tool into a standard work flow without additional processing steps.

Within the subject of interface and specification theories in formal methods, semantic model transformations exist for many types of low-level behavioral models [3-5, 7-9, 11-14, 20, 22, 23]. In recent work, we have developed a generalization of these approaches in which the semantics of models is configurable [START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF][START_REF] Fahrenberg | The quantitative linear-time-branching-time spectrum[END_REF]: When models and specifications contain quantities such as timing information or resource use, the precise behavior of model transformations depends on the type of quantities and on the application. Hence, the precise definitions and properties of model transformations depend on the quantitative semantics, and our generalization offers a generic way of configuring the transformations and properties according to the semantics.

Similarly in spirit, Maoz et.al. have in [START_REF] Cohen | Semantically configurable analysis of scenariobased specifications[END_REF][START_REF] Maoz | Semantically configurable consistency analysis for class and object diagrams[END_REF] introduced techniques for semantically configurable analysis of some high-level models, viz. class diagrams and scenario specifications. They use feature diagrams [START_REF] Kang | Feature-oriented domain analysis (FODA) feasibility study[END_REF][START_REF] Schobbens | Feature diagrams: A survey and a formal semantics[END_REF] for configurability, so that the analysis depends on the selection of features.

We have in [START_REF] Fahrenberg | Sound merging and differencing for class diagrams[END_REF][START_REF] Fahrenberg | Make a difference! (Semantically)[END_REF] introduced semantically correct model transformations for feature diagrams and class diagrams, see Figures 2 and3 for some examples. These operators' return types are the same as their input types, so that they can be integrated smoothly into existing tools and work flows, but they rely on a complete formal semantics. We believe that these approaches can be combined with the configurability of [START_REF] Cohen | Semantically configurable analysis of scenariobased specifications[END_REF][START_REF] Maoz | Semantically configurable consistency analysis for class and object diagrams[END_REF] to yield model transformations which are automatic and correct-by-design, yet flexible enough to be practically useful.

Conclusion

We propose to employ a configurable-semantics approach, using feature diagrams, to develop automatic model transformations which are correct by design and can be integrated smoothly into existing tools and work flows. Such model transformations are important for agile modeling methods. Fig. 2. Two class diagrams (above) and their merge (below), cf. [START_REF] Fahrenberg | Sound merging and differencing for class diagrams[END_REF].

As an example, consider the following scenario: An engineer wants to perform a three-way merge of two models which have evolved from a common ancestor. She will first use her development tools to attempt an entirely syntactic merge, which will detect some conflicts which are inessential because they only amount to syntactic differences while being semantically equivalent (given the developers' intuitive understanding of the semantics). These she can easily detect, and she can adjust her merge tool to take them into account (hence applying a partial semantics). However, due to semantic effects which propagate through the models, also the reverse may happen: there may be semantic conflicts which go undetected by the syntactic approach. These are more difficult to detect and require that even a merge which is syntactically correct be carefully checked by applying possibly several different semantics.

Fig. 3 .

 3 Fig.3. Two feature diagrams and an over-approximation of their difference, cf.[START_REF] Fahrenberg | Make a difference! (Semantically)[END_REF].


Médard Thiry

Hervé Theveniaut

Régine Simon-Coinçon

Caroline Ricordel-Prognon

Fabien Lenoir

Persistent paleosurfaces in the basement of French Massif Central: geodynamic implications

The post-orogenic evolution of crystalline massifs has always suffered from a lack of reliable geological data to constrain its history. With the advent of new techniques such as thermochronology and paleomagnetic age determinations, more robust constraints are available. However, their interpretations may still present contradictions. This is the case of the French Massif Central basement. The siderolithic paleoweathering surfaces have been dated to the Late Jurassic/Early Cretaceous, contrasting with previously accepted Tertiary age and implying that the Massif has never hosted a thick sedimentary cover. This contradicts with former thermochronological results. Herein, we expose the arguments for and against the proposed geodynamic evolution of the French Massif Central constrained by paleomagnetic age determinations. This said, thermochronological results should not be cast aside. Instead, the apparent contradiction should be addressed. Is there a, yet unknown, bias in these fission track records?

Dating of the siderolithic profiles

The red duricrusts, associated to the siderolithic formations overlying the French Massif Central basement have traditionally been assigned to the Eocene-Oligocene. Paleomagnetic results obtained on these duricrusts indicate that their ages range from 160 Ma (Late Jurassic) in the centre of the massif to 140 Ma (Early Cretaceous) in the northern parts [START_REF] Ricordel-Prognon | Lateritic paleoweathering profiles in French Massif Central: Paleomagnetic datings[END_REF] (Figure 1). A second episode of remagnetization is recorded at around 50 Ma in two red duricrust sections: Le Rouget in the centre of the massif and St-Désiré near its northern edge. In the St-Désiré area, the younger age is recorded in the lower part of the profiles. This agrees with the weathering process which progress from the top to the base, by deepening of the profile. The current geodynamic models for the Massif Central are anchored on a Tertiary age of the duricrusts. A revaluation of their ages to about 100 Myr (or more) older has major repercussions and demands that the geodynamic evolution of the Massif Central be revised, including its behaviour during the Mesozoic, its erosion, the development of the current landscapes, etc. In the past, the models were essentially constrained by a Tertiary age of the siderolithic formations. A significant portion of the continental evolution of the massif, the paleosurfaces and the current surface topography were considered as being of Tertiary age. Pushing the age of the siderolithic formations back to the Late Jurassic places back into question earlier geodynamic models. Moreover, if these evolutions are not of Tertiary age, how did the Massif evolve during the Tertiary? Lastly, the Late Jurassic ages of the siderolithic formations bring considerable constraints for interpreting the palaeogeographic evolution of the Massif Central during Mesozoic and Cenozoic.

N Mediterranean Sea

St

Role of eustatism

The paleomagnetic ages show that red duricrusts are older in the centre of the massif than to the north, near the edge of the Paris Basin (Figure 1). The spatial distributions of ages call for a progressive emergence of the massif over a 30 Myr period, coinciding with low eustacy levels at the end of the long regression period from the Triassic to the Lower Cretaceous. The second period of oxidation, leading to the paleomagnetic remagnetization ages of 50 Ma also coincides with a period of low sea level during the Eocene. Even if tectonic movements cannot be denied over this long period, the progressive emergence of the massif under the influence of falling sea level has played a decisive role for its evolution. Marine regression would have triggered the incision of the landscape and in turn lowering groundwater tables would have reactivated oxidation and weathering recorded by paleomagnetism.

Durability of the paleolandscapes

The red duricrusts are bound to contrasted paleolandscapes that are still imprinted in the current morphology of the massif. These paleolandscapes, formed of deep paleodrainages, pediments surrounding paleoreliefs, fault scarps, etc. are sealed by red duricrusts. Moreover, the red duricrusts locally seal paleovalleys filled with fluviatile sandstones and claystones.

What age are these ancient valley infill deposits? The sands beneath the red duricrust do not contain chert nodules at La Collange or St Désiré sites. We can deduce that their provenance is not the former Jurassic cover which contained chert layers. They may, however, be associated to Triassic fluviatile deposits known around the Massif Central and observed to infill paleovalleys cutting through the basement [START_REF] Lougnon | Les gisements plombo-zincifères du seuil du Poitou et de sa bordure limousine[END_REF][START_REF] Fogliérini | Le gisement stratiforme de Largentière (Ardèche). Pb (Ag, Zn, Sb). in: Les gisements français de pb, Zn, W, Sn, Au, As, barytine, fluorine, talc[END_REF][START_REF] Soulé De Lafont | Les gisements stratiformes de flurorine du Morvan (sud-est du bassin de Paris, France). n: Les gisements français de pb, Zn, W, Sn, Au, As, barytine, fluorine, talc[END_REF].

The erosional history of the massif is complicated by successive marine transgression and regression. Albeit, it is likely that Jurassic and Cretaceous sediments covered the northern margin of the Massif and may have extended to its central parts. No matter the extent and history of the sedimentary cover, the fact that basement paleomorphologies inherited from the post-Hercynian evolution are preserved is most important; an unsuspected finding prior to the attribution of the red duricrust to a Jurassic age.

Grabens outset and Pangea break up

Often red duricrusts developed on thick fan deposits abutting fault scarps (St Désiré and Cher graben, Lembron area, Naussac graben and le Rouget site).

Considering the previously accepted Tertiary age of the siderolithic formations, the red duricrusts were thought to have developed during the early stages of rifting. Field observations provide the evidence that the faults were active before development of the red duricrusts. With the new paleomagnetic ages, the sequence of events remain unchanged the timing of faulting along the Tertiary grabens began much earlier prior to 170-150 Ma (Late Jurassic). By contrast, number of ore deposits connected to fracture opening in the basement have been dated back to Middle Jurassic by way of radiochronology. This is especially the case of various mineralizations in the Massif Central, the Vosges Massif and the Schwarzwald basements [START_REF] Bonhomme | Reliability of K/Ar-dating of clays and silifications associated with vein mineralizations in western Europe[END_REF][START_REF] Brockamp | Authigenic sericite record of a fossil geothermal system: the Offenburg trough, central Black Forest, Germany[END_REF][START_REF] Edel | The Variscan tectonic inheritance of the Upper Rhine Graben: evidence of reactivations in the Lias, Late Eocene-Oligocene up to the recent[END_REF]. In addition, extensive hydrothermal alterations occurred in Permian and Triassic age deposits along fault systems related to the Paleozoic crystalline basements. Their isotopic ages are concentrated between 190-140 Ma ago, around Middle-Late Jurassic [START_REF] Bonhomme | Diagenèse généralisée du Jurassique moyen (170-160 Ma) dans le bassin du Rhône inférieur jusqu'à la bordure des Cévennes (France). Datation K-Ar d'argiles du Trias et du Lias inférieur[END_REF][START_REF] Santizo | Existence d'un hydrothermalisme tardif dans le bassin de Lodève (Hérault). Arguments paléothermométriques et géochronologiques[END_REF]Clauer et al., 2008;[START_REF] Brockamp | Mesozoic hydrothermal impact on Rotliegende and Bunter immature sandstones of the High Rhine trough and its adjacent eastern area (southern Black Forest, Germany)[END_REF]. Authors agree to relate these hydrothermal activities, which are found extensively throughout Europe, with tectonic pulses during the break up of Pangea and the long-lasting opening of the North Atlantic Ocean and/or the nearby Tethys area. The onset of a pre-rift thermal uplift in the Aalenian has also been evidenced in Central and Northern North Sea [START_REF] Rattey | Sequence stratigraphy of a failed rift system: the Middle Jurassic to Early Cretaceous basin evolution of the Central and Northern North Sea[END_REF]. In the French Massif Central the red duricrusts that abut and seal the faults are direct evidence of pre-rifting faulting of the European craton and along which Oligocene rifting was reactivated.

Mesozoic cover of the Paleozoic massif

Dating of the red duricrusts resting on crystalline basement raises the question of the Mesozoic cover of the Massif Central. Geologists considered classically that the Massif Central formed a high throughout the Mesozoic era. It was generally admitted that even if the basement was not outcropping the Jurassic series were reduced and the Upper Cretaceous transgression did not cover the massif. This paleogeographic outline was argued by the presence of proximal facies in the peripheral deposits (dinosaurian footprints in continental borderlands, exondation traces, thickness reduction, sandy deposits coming with the Cretaceous transgression and absence of residual flintstones) [START_REF] Vignaud | Les faunes de vertébrés Jurassiquesde la bordure Nord-Orientale du Bassin d'Aquitaine (France): Biochronologie et environnements[END_REF][START_REF] Loeuff (le) | Discovery of a thyreophoran trackway in the Hettangian of central France[END_REF][START_REF] Gand | Les traces de pas d'Amphibiens, de Dinosaures et autres Reptiles du Mésozoïque français: Inventaire et interprétations[END_REF]. This "accepted" outline was questioned during the 1990s by the results from apatite fission tracks analyses. These results led to propose that the Massif Central was covered by a thick Mesozoic series, up to 1500 m, and which would have been eroded quickly at the end of the Upper Cretaceous and the beginning of the Tertiary, before the development of the siderolithic duricrusts that rest on the basement. [START_REF] Barbarand | Burial and exhumation history of the south-eastern Massif Central (France) constrained by apatite fission track thermochronology[END_REF][START_REF] Peyaud | Mid-Cretaceous uplift and erosion on the northern margin of the Ligurian Tethys deduced from thermal history reconstruction[END_REF]. Both proposals corresponded to conflicting geodynamic evolutions (Figure 2). The dating of the red duricrusts calls into question the eventuality of such a thick Mesozoic cover on the Massif Central. Indeed, if the crystalline basement was uncovered during the Lower Cretaceous it is not possible to cumulate Jurassic and Cretaceous sedimentary series. Only an Upper Cretaceous cover is plausible yet it is unconceivable that it was thicker on the massif than in the peripheral sedimentary basins. It then follows that the Cretaceous (post-Sidérolithic) sedimentary cover never reached 500 m of thickness. Moreover, Mesozoic material, in particular chert, is not observed within the red duricrusts in the centre of the Massif Central. Cherts stemming from the Jurassic cover are observed in duricrusts in the northern Massif Central, along the Paris basin margin. The Jurassic chert cobles known in the centre of the massif are restricted to alluvium coming from Jurassic deposits that line the massif to the South and to the East [START_REF] Fernandes | Itinéraires et transformations du silex : une pétroarchéologie refondée, application au Paléolithique moyen[END_REF]. It is thus likely that the centre of the Massif never hosted a Mesozoic cover and that the sands underneath the red duricrust in La Collange section are fluviatile sands related to the major Triassic discharge. In addition, there are no known residual Cretaceous flints in the centre of the Massif or in the alluvium connected to the large valleys cut in the basement. Therefore, one cannot exclude that a portion of the Massif Central remained emerged also during the Upper Cretaceous. The arguments of the classic geological hypotheses based on facies of the peripheral deposits are therefore sound. However, why do fission track analyses support a scenario with a thick sedimentary cover?

Persistence of the paleosurfaces

In addition to the Jurassic paleosurfaces marked by the red duricrust and dated by paleomagnetism, other paleosurfaces related to the continental evolution of the Massif Central are known and help constrain its geodynamic evolution. These are namely Triassic paleosurfaces characterized by specific weathering of the basement and Tertiary paleosurfaces underlying Oligocene deposits in grabens.

Basement rocks (granites, gneiss, rhyolites and even Permo-Carboniferous sedimentary rocks) show often pinkish/reddened facies throughout the Massif Central. It has been shown that these reddened facies are albitised (mainly pseudomorphic replacement of the primary plagioclases into albite and alteration of the biotite into chlorite) and hematized [START_REF] Schmitt | Triassic albitization in southern France : an unusual mineralogical record from a major continental paleosurface[END_REF][START_REF] Parcerisa | Albitisation related to the Triassic unconformity in igneous rocks of the Morvan Massif (France)[END_REF]. These reddened and albitised facies, up to 200 m thick, are arranged in a clear succession against the Triassic unconformity that gives significant constraints to their connection with the Triassic palaeosurface. Moreover, altered facies have been dated back to the Triassic by using radiochronological methods [START_REF] Bonhomme | Datation K-Ar de fractions fines associées aux minéralisations. Le cas du basin uranifère permo-houiller de Brousse-Broquiès (Aveyron)[END_REF][START_REF] Schmitt | Pétrographie et datations K-Ar des transformations minérales affectant le gÎte uranifére de Bertholéne (Aveyron-France)[END_REF] and more recently by paleomagnetic methods [START_REF] Ricordel | Triassic magnetic overprints related to albitization in granites from the Morvan massif (France)[END_REF]. Given that the alterations are of the same age as the unconformity, it follows that the albitized facies are The remarkable persistence of the Triassic paleosurface has been highlighted by geomorphologists. The consistency and in particular the resistance to erosion emerges as a major feature of this paleosurface and seems to be mainly related to the albitization. The albitized granites are entirely free of anorthitic plagioclases that are much more sensitive to chemo-mechanical weathering. The development of albite and additional chloritization of the primary biotite crystals render the rocks much more resistant to weathering and erosion.

Conclusion

The results presented herein show the importance of determining the age of paleoweathering profiles and focus interests on the history of continental areas and in particular the geodynamics of Paleozoic crystalline basements. The results obtained over more than 30 years of investigation of the paleosurfaces of the French Massif Central and its bordering geological formations highlight how interpretations "ripen" and evolve through time and the necessity and benefit of nurturing a research program over several decades. This said, an unresolved question remains in explaining the inconsistency between the scenarios constrained by paleoweathering profiles ages versus fission track analyses. A possible research path to be explored is the crystallization of apatite during Triassic albitization of granites.

  Figure 1 -Geological sketch of the French Massif Central showing the occurrences of the siderolithic red duricrusts setting on the basement and their paleomagnetic ages.

Figure 2 -

 2 Figure 2 -Sketch of the conflicting hypotheses for the geodynamic evolution of the French Massif Central during the Mesozoic. In the "Classical" hypothesis (A) the massif remained bare or hosted a reduced sedimentary cover. The tectonic constraints are more or less continuous with a relatively stable zone of flexure. In the fission track hypothesis (B) the massif supported a thick cover. Here, differential movements and important erosion intervenes after the Upper Cretaceous.

  related to the Triassic paleosurface and can be used to trace the Triassic paleosurface through wide crystalline areas, even areas far removed from the Mesozoic coverrelated unconformities provide key arguments to unravel the geodynamic evolution of the Massif Central. Triassic, Late Jurassic and Tertiary unconformities are superimposed on large areas of the Massif Central. This implies very little erosion of the crystalline basement since Triassic time, as shown by the widespread preservation of the Triassic albitized facies. These paleosurface ages provide important constraints to Mesozoic/Cenozoic crustal dynamics modelling. Identification and dating of the successive continental unconformities are evidence for long lasting continental evolution and landscape stability of large areas of the Massif Central during the Mesozoic.