Uli Fahrenberg

Axel Legay

Claus Thrane

The Quantitative Linear-Time-Branching-Time Spectrum

Keywords: 1998 ACM Subject Classification F, 1, 1 Models of Computation 1

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 provide fixed-point characterizations of all system distances, and we 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 should be treated orthogonally in any theory of quantitative verification (of course they can hardly be separated in practice, but that is not of our concern here). The formalism we propose in this paper addresses this orthogonality 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 real-valued outcomes, as opposed to discrete games, effectively allows us obtain a continuous verdict on the relationship between systems, and hence to detect the difference between minor and major discrepancies between systems.

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 The nodes are the different system distances introduced in this paper, and an edge d1 -→ d2 indicates that d1(s, t) ≥ d2(s, t) for all states s, t, and that d1 and d2 are topologically inequivalent.

quantitative measures like the ones in [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] 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 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.

The authors wish to thank Luca Aceto for some insightful comments on a previous version of this paper. Note that due to space constraints, some proofs had to be omitted.

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 , . . . ) and a i the k-shift, and ith element respectively, of a (finite or infinite) sequence, and by ǫ the empty sequence.

A function d :

X × X → | ≥0 ∪ {∞} on a set X is called a hemimetric if d(x, x) = 0 and d(x, y) + d(y, z) ≥ d(x, z) for all x, y, z ∈ X. If d is such that d(x, y) = 0 implies x = y for all x, y ∈ X, it is called a quasimetric.
B i (x; r) = {y ∈ X | d i (x, y) < r}, for i = 1, 2,
x ∈ X, and r > 0, 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 metric 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 metrics which imply that any other reasonable metric 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 (σ, τ ) = ∞.
(Note that we hence apply the asymmetric view on distances as e.g. in [START_REF] Luca De Alfaro | Linear and branching system metrics[END_REF].) 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. For a (finite or infinite) path π in a LTS we denote by tr(π) ∈ ❑ ∞ the trace induced by π. 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 distance on labels in ❑ and a method to combine these distances on individual symbols to a distance on traces. Three general methods are used for this combination: 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 ).
Here λ is a discounting factor with 0 < λ ≤ 1, and we assume that the involved traces have equal length; otherwise any trace distance has value ∞. Note that all trace distances are parametrized by the label distance d. 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 label distance d 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 σ j = τ j for all j, 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 -PW 1 (d)(σ, τ ) = 1 if and only if d T disc (σ, τ ) = ∞. Point-wise and accumulating distances (for concrete instances of label distances d and concrete instantiations of ❑) 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 [START_REF] Henzinger | Quantifying similarities between timed systems[END_REF][START_REF] Thrane | Quantitative analysis of weighted transition systems[END_REF] defined for

❑ ⊆ Σ × |. 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 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) 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 5.2 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.

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 we only allow Player 1 to switch paths if he also increases 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 ′ ).
A pair of states (s, t) ∈ S × S and a pair of strategies

(θ 1 , θ 2 ) ∈ Θ 1 × Θ 2 induc- tively determine a sequence (π j , ρ j , m j ) of configurations given by (π 0 , ρ 0 , m 0 ) = (s, t, 0), (π 2j+1 , ρ 2j+1 , m 2j+1 ) = upd θ1 (π 2j , ρ 2j , m 2j ) and (π 2j , ρ 2j , m 2j ) = upd θ2 (π 2j-1 , ρ 2j-1 , m 2j-1 )
; the sequence is understood to finish as soon as one of the updates is undefined.

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 potentially 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 out(θ 1 , θ 2 )(s, t) = (π, ρ), and its utility is util(θ 1 , θ 2 )(s, t) = d T (tr(out(θ 1 , θ 2 )(s, t))) = d T (tr(π), tr(ρ))
, where d T is given as a parameter to the game. 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).
In the following we will need 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 2 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 trace distance d T 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, and ultimately to determinacy of Gale-Steward games [START_REF] Martin | Borel determinacy[END_REF]. Note that if it holds, then so does the same equation with Θ 1 replaced by any subset Θ ′ 1 ⊆ Θ 1 . We finish this section by showing that under certain conditions, the game value is 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. The following proposition shows that for any uniform strategy subset which contains all non-switching strategies and any well-behaved trace distance, the value of our quantitative game is a hemimetric.

◮ Proposition 2. If Θ ′ 1 ⊆ Θ 1 is uniform and Θ 0 1 ⊆ Θ ′ 1 , and if d T is well-behaved, then v(Θ ′ 1 ) is a hemimetric on S.
Next we show a powerful 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.

◮ Theorem 3 (Transfer principle). Assume the LTS (S, T ) to be finitely branching and d T to be a well-behaved quasimetric, and let

Θ ′ 1 , Θ ′′ 1 ⊆ Θ 1 . If there exist s, t ∈ S for which 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, and as (S, T ) is finitely branching, 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 a quasimetric, 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. ◭ 4
The Distance Spectrum

In this section we introduce the distances depicted in Figure 1 and show their mutual 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 lineartime-branching-time spectrum at every point of the quantitative dimension. In order to capture the remaining equivalences in the original spectrum [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF], 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.

Let (S, T ⊆ S × ❑ × S) be a LTS and

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

Branching Distances

If the switching counter in the game introduced in Section 3 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 4. The bisimulation distance between s and t is d bisim (s, t) = v(s, t).

Note again that bisimulation distance, and indeed all distances defined in this section, are parametrized by the trace distance d T .

◮ Theorem 5. For d T = d T disc the discrete trace distance, d bisim disc (s, t) = 0 iff 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 pre-defined 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 non-switching strategies.

◮ Definition 6. 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 between s and t is d k-sim-eq (s, t) = max(v(Θ k-sim 1 )(s, t), v(Θ k-sim 1 )(t, s)). ◮ Theorem 7. For d T = d T disc the discrete trace distance, d k-sim
disc (s, t) = 0 iff there is a k-nested simulation from s to t, d k-sim-eq disc (s, t) = 0 iff 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. The proof is similar to the one of Theorem 5.

◮ Theorem 8. 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 a well-behaved quasimetric and the LTS (S, T ) is finitely branching, 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 Theorem 3 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 after 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} ◮ Definition 9. 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 1 (Θ k-rsim 1 )(s, t), v 1 (Θ k-rsim 1 )(t, s)).
For the discrete case, only k = 1 seems to have been considered; the proof is again similar to the one of Theorem 5.

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

The next theorem finishes our work on the right half of Figure 1; its proof is similar to the one of Theorem 8.

◮ Theorem 11. 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 a well-behaved quasimetric and the LTS (S, T ) is finitely branching, then all distances above are topologically inequivalent.

Linear Distances

Above we have introduced the distances in the right half of the quantitative linear-timebranching-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. Now we can define, for s, t ∈ S and

k ∈ ◆ + , the ∞-nested trace equivalence distance: d ∞-trace-eq (s, t) = v 1 ( Θ1 )(s, t), the k-nested trace distance: d k-trace (s, t) = v 1 ( Θk-sim 1
)(s, t), the k-nested trace equivalence distance: )(s, t), and the k-nested ready equivalence distance:

d k-trace-eq (s, t) = max(v 1 ( Θk-sim 1 )(s, t), v 1 ( Θk-sim 1 )(t, s)), the k-nested ready distance: d k-ready (s, t) = v 1 ( Θk-rsim
d k-ready-eq (s, t) = max(v 1 ( Θk-rsim 1 )(s, t), v 1 ( Θk-rsim 1 )(t, s)).
Using the discrete trace distance, we recover the following standard relations [START_REF] Van Glabbeek | The linear time -branching time spectrum I[END_REF].

◮ Theorem 12. For d T = d T disc the discrete trace distance and s, t ∈ S we have d 1-trace disc (s, t) = 0 iff there is a trace inclusion from s to t, d 1-trace-eq disc (s, t) = 0 iff s and t are trace equivalent, d 2-trace disc (s, t) = 0 iff there is a possible-futures inclusion from s to t, d 2-trace-eq disc (s, t) = 0 iff s and t are possible-futures equivalent, d 1-ready disc (s, t) = 0 iff there is a readiness inclusion from s to t, d 1-ready-eq disc (s, t) = 0 iff 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 8 and 11, the theorem follows by strategy set inclusion, Theorem 3, and corresponding results for the discrete relations.

◮ Theorem 13. 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 a well-behaved quasimetric and the LTS (S, T ) is finitely branching, then all distances above are topologically inequivalent.

Recursive Characterizations

Now we 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 5.2 that this can be applied to all examples of trace distances mentioned in Section 2.1. 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] and is also necessary in our case.

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 σ = τ = ǫ (1)
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.

◮ Theorem 14. 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 distance, where we have the following fixed-point equation, using h * 1,1 = h 1-sim :

h 1-sim (s, t) = sup s x -→s ′ inf t y -→t ′ F (x, y, h 1-sim (s ′ , t ′ ))
An equally compact expression may be derived for bisimulation distance, and similar theorems for all the other distances in the quantitative linear-time-branching-time spectrum can also be derived. The fixed-point characterizations above immediately lead to iterative 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 . Note however that this computation is only guaranteed to converge to simulation distance in finitely many steps in case the lattice L S×S is finite.

Recursive Characterizations for Example Distances

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

Let d be a hemimetric on ❑, then for all σ, τ ∈ ❑ ∞ and 0 < λ ≤ 1,

ACC λ (d)(σ, τ ) =        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 14 we can e.g. derive the following fixed-point expression for simulation distance:

ACC λ (d) 1-sim (s, t) = sup s x -→s ′ inf t y -→t ′ (d(x, y) + λ ACC λ (d) 1-sim (s ′ , t ′ ))
Similar considerations apply to the point-wise distances, with "+" replaced by "max". Incidentally, these are exactly the expressions introduced, in an ad-hoc manner, 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 fixedpoint 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 also here the 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 (1) holds, giving the following fixed-point expression for limit-average simulation distance:

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 2.1, 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 (1) 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]:

h 1-sim (δ)(s, t) = sup s x -→s ′ inf t y -→t ′ max(|δ + x -y|, h 1-sim (s ′ , t ′ )(δ + x -y))
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.

Regarding Cantor distance, a useful recursive formulation is f (σ, τ )(n) = f (σ 1 , τ 1 )(n + 1) if σ 0 = τ 0 and 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. 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 Proof of Theorem 14. The lattice (L S×S ) (◆+∪{∞})×{1,2} with the point-wise partial order is complete, and I is monotone because F is, so by Tarski's fixed-point theorem, I has indeed a least fixed point h * . To show that ≁ kd = g • h * k,1 for all k, we pull back ≁ kd along g:

s t u π π π π χ χ χ χ π ′ π ′ π ′ π ′ ρ ′ 1 ρ ′ 1 ρ ′ 1 ρ ′ 1 ρ ′ 2 ρ ′ 2 ρ ′ 2 ρ ′ 2 χ ′ χ ′ χ ′ χ ′ Figure 2
(e ′ , m) = θ t,u 2 (ρ ′ 2 • e, χ ′ , m) in the (s, t)-game to compute θ s,t 2 (π ′ • e ′ , ρ ′ 1 , m). Figure
1 ∈ Θ ′ 1 , let (π, χ) = out(θ s,u 1 , θ s,u 2 )(s, u),
Define w : (◆ + ∪ {∞}) × {1, 2} → L S×S by w k,1 (s, t) = sup θ1∈≁kΘ1 inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(s, t))) w k,2 (s, t) = sup θ1∈≁kΘ1 inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(t, s))) then ≁ kd = 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) = w k,1 (s, t).

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 ′
In the last max expression, ≁ kΘ 1,ns ⊆≁ kΘ 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Θ 1,s =≁ kΘ 1 \ ≁ kΘ 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), [START_REF] Chen | Game characterizations of process equivalences[END_REF] 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).

(4)

Now let θ 1 ∈≁ kΘ 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.

◭

Figure 1

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

1

 1

FFfFFffff

  (x, y, w k-1,2 (s ′ , t ′ )) (x, y, supθ1∈≁kΘ1 inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(s ′ , t ′ )))) (tr(out(θ 1 , θ 2 )(t ′ , s ′ )))) (x, y, f (tr(out(θ 1 , θ 2 )(s ′ , t ′ ))(x, y, f (tr(out(θ 1 , θ 2 )(t ′ , s ′ )))) (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)Θ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Θ 1 do not depend on each other, so the corresponding inf and sup can be exchanged, whenceI(w k,1 )(s, t) = max (x • tr(out 1 (θ 1 , θ 2 )(s ′ , t ′ )), y • tr(out 2 (θ 1 , θ 2 )(s ′ , t ′ ))) sup (x • tr(out 1 (θ 1 , θ 2 )(t ′ , s ′ )), y • tr(out 2 (θ 1 , θ 2 )(t ′ , s ′ ))), (tr(out(θ 1 , θ 2 )(s, t))) sup θ1∈≁kΘ1,s inf θ2∈Θ2 f (tr(out(θ 1 , θ 2 )(s, t)))

  Two hemimetrics d 1 and d 2 on a set X are said to be topologically equivalent if the topologies on X generated by the open balls

  Configuration update in the game used for showing the triangle inequality 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

  and let ρ′ be the corresponding memory path. By Lemma 15 there exist θ s,t

	1 , θ t,u 1 2 )(s, t) and d T (tr(ρ ′ ), tr( χ)) = util(θ t,u 1 , θ s,t util(θ s,t 1 , θ t,u ∈ Θ ′ 1 for which d T (tr(π), tr(ρ ′ )) = 2 )(t, u). Using Equation (2) we have 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). ◭

Appendix: Proofs

◮ Lemma 15. 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 (σ, τ ). ◭ Proof of Proposition 2. 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

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:

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