Patricia Bouyer
email: bouyer@lsv.ens-cachan.fr

Nicolas Markey
email: markey@lsv.ens-cachan.fr

Ocan Sankur
email: ocan.sankur@normalesup.org

Robust Reachability in Timed Automata and Games: A Game-based Approach ✩

Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.

Introduction

Timed automata [START_REF] Alur | A theory of timed automata[END_REF] are a timed extension of finite-state automata. They come with an automatatheoretic framework to design, model, verify and synthesize systems with timing constraints. One of the most basic problems in timed automata is the reachability problem: given a timed automaton and a target location, is there a path that leads to that location? This can be rephrased in the context of control as follows: is there a strategy that dictates how to choose time delays and edges to be taken so that a target location is reached? This problem has been solved long ago [START_REF] Alur | A theory of timed automata[END_REF], generalized to timed games [START_REF] Asarin | Controller synthesis for timed automata[END_REF], and efficient algorithms have then been developed and implemented [START_REF] Kim | UPPAAL in a nutshell[END_REF][START_REF] Yovine | Kronos: A verification tool for real-time systems[END_REF].

However, the abstract model of timed automata is an idealization of real timed systems. For instance, we assume in timed automata that strategies can choose the delays with arbitrary precision. In particular, the delays can be arbitrarily close to zero (the system is arbitrarily fast), and clock constraints can enforce exact delays (time can be measured exactly). Although these assumptions are natural in abstract models, they need to be justified after the design phase. Indeed the situation is different in real-world systems: digital systems have response times that may not be negligible, and control software cannot ensure timing constraints exactly, but only up to some error, caused by clock imprecisions, measurement errors, and communication delays. A good control software must be robust, i.e., it must ensure good behavior in spite of small imprecisions [START_REF] Henzinger | The embedded systems design challenge[END_REF][START_REF] Kopetz | Real-Time Systems: Design Principles for Distributed Embedded Applications[END_REF].

Consequently, there has been a recent effort to consider imprecisions inherent to real systems in the theory of timed systems. In particular, there has been several attempts to define convenient notions of robustness for timed automata. The approach initiated in [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF][START_REF] De Wulf | Robust safety of timed automata[END_REF] is the closest to our framework. It consists in modeling imprecisions by enlarging all clock constraints of the automaton by some parameter δ, that is transforming each constraint of the form x ∈ [a, b] into x ∈ [aδ, b + δ], and in synthesizing δ > 0 such that all runs of the enlarged automaton satisfy a given property. Several model-checking algorithms for timed automata were then re-visited and extended to this setting in [START_REF] Bouyer | Robust model-checking of timed automata[END_REF][START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF][START_REF] Bouyer | Robust model-checking of timed automata via pumping in channel machines[END_REF][START_REF] Sankur | Untimed language preservation in timed systems[END_REF] and symbolic algorithms were studied in [START_REF] Jaubert | Quantitative robustness analysis of flat timed automata[END_REF][START_REF] Daws | Symbolic robustness analysis of timed automata[END_REF]. This notion of robustness also corresponds to a concrete implementation semantics; in fact robustness implies implementability in a simplied model of a micro-processor, see [START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF].

In all these works, the robustness condition is satisfied if there exists an enlargement parameter for which all runs of the enlarged automaton satisfy a given property. In other terms, for any choice of the delays and edges, and any possible perturbation, the given property must hold. Although this is a convenient notion for e.g. safety properties, this does not capture the system's ability to adapt to perturbations that were observed earlier in a given run. In fact, if perturbations have accumulated and deviated the system from its course, a smart control software should be able to adapt its action to correct this. Thus, we believe a good notion of robustness can be defined by a game played between two players: Controller with a reachability objective, and Perturbator with the complementary objective.

Following this idea, we are interested in the synthesis of robust strategies in timed automata and games for reachability objectives, taking into account response times and imprecisions. In our semantics, which is parameterized by δ P and δ R with 0 < δ P ≤ δ R , Controller chooses to delay an amount d ≥ δ R after which the guard of a chosen edge is satisfied, and the system delays d ′ and takes the edge, where d ′ is chosen by Perturbator satisfying |dd ′ | ≤ δ P . Observe that the guard may not be satisfied after the delay d ′ , but the chosen edge is taken whatever the perturbations. We say that a given location is robustly reachable if there exist parameters 0 < δ P ≤ δ R such that Controller has a winning strategy ensuring that the location is reached against any strategy of Perturbator. To simplify the presentation, but w.l.o.g., we assume in this paper that δ = δ P = δ R ; our algorithm can easily be adapted to the general case (see Section 4).

The main result of this paper is the following: We show that deciding the existence of δ > 0, and of a strategy for the controller so as to ensure reachability of a given location in a turn-based timed game (whatever the imprecision, up to δ), is EXPTIME-complete. Moreover, if there is a strategy, we can compute a uniform one, which is parameterized by δ, using shrunk difference bound matrices (shrunk DBMs) that we introduced in [START_REF] Sankur | Shrinking timed automata[END_REF]. In this case, our algorithm provides a bound δ 0 > 0 such that the strategy is correct for all δ ∈ [0, δ 0 ]. Our strategies also give quantitative information on how perturbations accumulate or can compensate. Technically, our work extends shrunk DBMs by constraints, and establishes non-trivial algebraic properties of this data structure (Section 3). The main result is then obtained by transforming the infinite-state game into a finite abstraction, which we prove can be used to symbolically compute a winning strategy, if any (Section 4).

A variant of our semantics was studied in [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] for timed games with fixed parameters. In this variant, Controller can only suggest delays and edges whose guards are satisfied after any perturbation; thus, this is a conservative variant of our semantics. When δ is fixed, the semantics can be encoded by a usual timed game, and standard algorithms can be applied. Whether one can synthesize δ > 0 for which the controller has a winning strategy was left as a challenging open problem. We solve this problem for reachability objectives in turn-based timed games. Parameterized reachability and safety in the conservative semantics of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] are studied in [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF]. See also Section 2.3 for notes on related work.

Robust Reachability in Timed Automata

Timed Automata and Games, and Robust Reachability

Given a finite set of clocks C, we call valuations the elements of R C ≥0 , which are nonnegative real vectors of dimension |C|. For a subset R ⊆ C and a valuation v, v[R ← 0] is the valuation defined by v[R ← 0](x) = v(x) for x ∈ C \ R and v[R ← 0](x) = 0 for x ∈ R. Given d ∈ R ≥0 and a valuation v, the valuation v + d is defined by (v + d)(x) = v(x) + d for all x ∈ C. We extend these operations to sets of valuations in the obvious way. We write 0 for the valuation that assigns 0 to every clock.

An atomic clock constraint is a formula of the form k x ′ l or k xy ′ l where x, y ∈ C, k, l ∈ Z ∪ {-∞, ∞} and , ′ ∈ {<, ≤}. A guard is a conjunction of atomic clock constraints. A valuation v satisfies a guard g, denoted v |= g, if all constraints are satisfied when each x ∈ C is replaced with v(x). We write Φ C for the set of guards built on C. Definition 2.1. A (two-player) turn-based timed game A is a tuple (L C ∪ L P , C, ℓ 0 , E), where L = L C ∪ L P is a finite set of locations satisfying L C ∩ L P = ∅, C is a finite set of clocks, E ⊆ L × Φ C × 2 C × L is a set of edges, and ℓ 0 ∈ L C is the initial location. An edge e = (ℓ, g, R, ℓ ′ ) is also written as ℓ g,R --→ ℓ ′ . A timed automaton is a turn-based timed game with L P = ∅.

Standard semantics of timed automata is usually given as a timed transition system [START_REF] Alur | A theory of timed automata[END_REF]. To capture robustness, we define the semantics as a game where perturbations in delays are uncontrollable. The semantics extends naturally to turn-based timed games, where our game semantics simply gives control over perturbations to one of the players.

Given a turn-based timed game A = (L C ∪ L P , C, ℓ 0 , E) and δ > 0, we define the perturbation game of A w.r.t. δ as a two-player turn-based game G δ (A) between players Controller and Perturbator. Intuitively the semantics is the following: At locations L C , Controller first suggests a delay and an edge at Perturbator perturbs the delay by some amount in the range [-δ, δ], and the designated edge is taken with the perturbed delay; at locations L P , the edge and the delay are entirely determined by Perturbator. Observe that the semantics is not symmetric; Perturbator has the role of the environment. Formally, the state space of G δ (A) is partitioned into V C ∪ V P where V C = L C × R C ≥0 belong to Controller, and

V P = L P × R C ≥0 ∪ L C × R C ≥0 × R ≥0 × E belong to Perturbator.
The initial state is (ℓ 0 , 0) and belongs to Controller. The transitions are defined as follows: from any state (ℓ, v) ∈ V C , there is a transition to (ℓ, v, d, e) ∈ V P whenever d ≥ δ, e = (ℓ, g, R, ℓ ′ ) is an edge such that v + d |= g. Then, from any such state (ℓ, v, d, e) ∈ V P , there is a transition to (ℓ ′ , (v + d + ǫ)[R ← 0]) ∈ V C , for any ǫ ∈ [-δ, δ]. Further, for any (ℓ, ν) ∈ V P , there is an edge from (ℓ, ν) to (ℓ ′ , (ν + d)[R ← 0]) for any d ≥ 0 and edge e = (ℓ, g, R, ℓ ′ ) such that ν + d |= g.

We assume familiarity with basic notions in game theory, and quickly survey the main definitions. A run in G δ (A) is a finite or infinite sequence of consecutive states starting at (ℓ 0 , 0). It is said maximal if it is infinite or cannot be extended. A strategy for Controller is a function that assigns to every non-maximal run ending in some (ℓ, v) ∈ V C , a pair (d, e) where d ≥ δ and e is an edge enabled at v + d, i.e., there is a transition from (ℓ, v) to (ℓ, v, d, e) ∈ V P . A strategy for Perturbator assigns to all states (ℓ, v, d, e) ∈ V P a perturbation ǫ ∈ [-δ, δ], and to all states (ℓ, v) ∈ V P , a delay and an edge whose guard is satisfied at v. A run ρ is compatible with a strategy f if for every prefix ρ ′ of ρ ending in V C , the next transition along ρ after ρ ′ is given by f . Given a target location ℓ, a strategy f is winning for the reachability objective defined by ℓ whenever all maximal runs that are compatible with f visit ℓ.

Observe that we require at any state (ℓ, v), that Controller should choose a delay d ≥ δ and an edge e that is enabled after the chosen delay d. The edge chosen by Controller is always taken but there is no guarantee that the guard will be satisfied exactly when the transition takes place. In fact, Perturbator can perturb the delay d chosen by Controller by any amount ǫ ∈ [-δ, δ], including those that do not satisfy the guard. Notice that G 0 (A) corresponds to the standard (non-robust) semantics of A. We are interested in the following problem.

Problem 2.2 (Parameterized Robust Reachability). Given a turn-based timed game A and a target location ℓ, decide whether there exists δ > 0 such that Controller has a winning strategy in G δ (A) for the reachability objective ℓ.

Our main result is the decidability of this problem. Moreover, if there is a solution, we compute a strategy represented by parameterized difference-bound matrices where δ is the parameter; the strategy is thus uniform with respect to δ. In fact, we provide a bound δ 0 > 0 such that the strategy is winning for Controller for any δ ∈ [0, δ 0 ]. These strategies also provide a quantitative information on how much the perturbation accumulates (See Fig. 3). The main result of this paper is the following: Theorem 2.3. Parameterized robust reachability is EXPTIME-complete both for timed automata and turn-based timed games.

Notice that we are interested in the parameterized problem: δ is not fixed in advance. When δ is fixed, the problem can be formulated and solved as a usual timed game (see [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] for such an encoding). The parameterized version is important since one does not necessarily have a precise estimation for perturbations at the design phase. It is also interesting to directly synthesize δ and a uniform strategy, as described above, rather than finding one by trial-and-error.

Checking parameterized robust reachability is different from usual reachability checking mainly for two reasons. First, in order to reach a given location, Controller has to choose the delays along a run, in such a way that these perturbations do not accumulate and block the run. In particular, it shouldn't play too close to the borders of the guards (see Fig. 3). Second, due to these uncontrollable perturbations, some regions that are not reachable in the absence of perturbation can become reachable (see Fig. 5). So, Controller must also be able to win from these newly reachable regions. The regions that become reachable in our semantics are those neighboring reachable regions. The characterization of these neighboring regions is one of the main difficulties in this paper (see Section 3.5).

The paper is organized as follows. In Section 3, we study shrunk DBMs, a data structure used to represent the parameterized state space of timed automata under perturbations [START_REF] Sankur | Shrinking timed automata[END_REF]. We extend this data structure to include shrinking constraints, and study neighborhoods of shrunk DBMs. For the sake of readability, we first present and prove the algorithm for timed automata, in Section 4, then explain how to extend the algorithm to turn-based timed games in Section 5. The EXPTIME-hardness result is given in Section 6.

Motivating example: robust real-time scheduling

An application of timed automata is the synthesis of schedulers in various contexts [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF]. We show that robust reachability can help providing a better schedulability analysis: we show that schedulers synthesized by standard reachability analysis may not be robust: even the slightest decrease in task execution times can result in a large increase in the total time. This is a phenomenon known as timing anomalies, first identified in [START_REF] Graham | Bounds on multiprocessing timing anomalies[END_REF].

Consider the scheduling problem described in Fig. 1, inspired by [START_REF] Reineke | A definition and classification of timing anomalies[END_REF]. Assume that we look for a greedy (i.e., work-conserving) scheduler, that will immediately start executing a task if a machine is free for execution on an available task. What execution time can a greedy scheduling policy guarantee on this instance? One can model this problem as a timed automaton, and prove, by classical reachability analysis, that these tasks can be scheduled using a greedy policy within six time units. However the scheduler obtained this way may not be robust, as illustrated in Fig. 1(b). If the duration of task A unexpectedly drops by a small amount δ > 0, then any greedy scheduler will schedule task B before task C, since the latter is not ready for execution at time 2δ. This yields a scheduling of tasks in 8δ time units.

Our robust reachability algorithm is able to capture such phenomena, and can provide correct and robust schedulers. In fact, it would answer that the tasks are not schedulable in six time units (with a greedy policy), but only in eight time units. See Appendix A for a detailed model and discussion of this example.

Related work: robustness in timed automata and games

Robustness in timed automata and hybrid automata models have been studied in the last two decades. The objective is mainly twofold: First, robustness is a desired property of real-time systems, so developing a formal framework for robustness analysis and robust synthesis is a natural goal. Second, taking into consideration perturbations can yield a more realistic semantics, which does not have the excessive expressive power of abstract timed automata. In fact, giving up on infinite precision may render some undecidable problems decidable, such as checking safety in linear hybrid automata under some conditions [START_REF] Fränzle | Analysis of hybrid systems: An ounce of realism can save an infinity of states[END_REF].

Several works focused particularly on defining a good notion of robustness in timed automata. [START_REF] Markey | Robustness in real-time systems[END_REF] surveys some of these. A first such attempt is [START_REF] Gupta | Robust timed automata[END_REF], where a topological notion is introduced, with the hope that the language inclusion problem could become decidable under this semantics, but the undecidability was later shown to hold even in the robust setting [START_REF] Henzinger | Robust undecidability of timed and hybrid systems[END_REF]. This approach differs from our work since we rather focus on a more concrete perturbation model with modelling and synthesis purposes. Also, topological robustness consists in discarding isolated behaviours, whereas our semantics adds behaviours. 0 1 2 3 4 5 6 7 8

M 2 M 1 A C B D E (a) A has duration 2.
0 1 2 3 4 5 6 7 8

M 2 M 1 A B C D E (b) A has duration 2 -δ.
Figure 1: Consider tasks A, B, C of duration 2 and D, E of duration 1, to be scheduled on two machines. As usual, we assume that a machine can execute a single task at a time. Dependences between tasks are as follows: A → B and C → D, E, meaning e.g. that A must be completed before B can start. Task A must be executed on machine M 1 and tasks B, C on machine M 2 . Moreover, the release time of task C means that it cannot be scheduled before 2 time units. Fig. 1(a) shows the optimal greedy schedule for these tasks under these constraints, while Fig. 1(b) shows the outcome of any greedy scheduler when the duration of task A is less than 2.

The semantics under an unknown regular sampling of time was considered in [START_REF] Cassez | A comparison of control problems for timed and hybrid systems[END_REF][START_REF] Parosh | Sampled universality of timed automata[END_REF][START_REF] Parosh | Sampled semantics of timed automata[END_REF]. Here, the goal is to synthesize a sampling parameter under which a reachability or safety objective holds, or the untimed language is preserved. [START_REF] Bouyer | Timed automata can always be made implementable[END_REF] shows that one can "compile" any timed automaton to an "approximate" one whose semantics is preserved under sampling. These approaches are orthogonal to ours since they privilege discrete semantics rather than considering continous delays and perturbations, and study loss of behaviour. We believe continous semantics provide more precision in timed automaton models since perturbations and environment's delays cannot always be assumed to be discrete.

Let us state more precisely the relation of our semantics with that of [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] De Wulf | Almost ASAP semantics: From timed models to timed implementations[END_REF][START_REF] De Wulf | Robust safety of timed automata[END_REF]. Robust model-checking, studied in these works, can be reformulated as follows: does there exists some δ > 0 such that whatever Controller and Perturbator do in G δ (A), a given property is satisfied. This is therefore the universal counterpart of our formulation of the parameterized robustness problem. It has been shown that this universal parameterized robust model-checking is no more difficult (in terms of complexity) than standard model-checking. This has to be compared with our result, where complexity goes up from PSPACE to EXPTIME.

In [START_REF] Sankur | Shrinking timed automata[END_REF], we studied robustness of timed automata to guard shrinkings, which is the dual notion of the robustness against guard enlargement. We introduced shrunk DBMs, which we also use and extend in this paper, in order to study the state space of timed automata with shrunk guards. We also give in [START_REF] Sankur | Shrinking timed automata[END_REF] a methodology to implement timed automata, while systematically avoiding the effect of imprecisions, modelled by guard enlargement. As in robust model-checking, this approach studies worst-case behaviour under a fixed (though parameterized) imprecision bound, and does not take into account systems' ability to react to actual perturbations.

As mentioned in the introduction, a similar but unparameterized notion of robustness for timed games was studied in [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF]. This unparameterized setting was also considered in the context of timed interface theories in [START_REF] Kim | Robust specification of real time components[END_REF] but the parameter synthesis problem was not addressed. The semantics of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF] is different since it requires Controller to suggest delays and edges whose guards are satisfied after the perturbed delay, for any perturbation. It turns out that parameterized reachability and safety are easier in this semantics; both are PSPACE-complete [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF].

A related line of work is that of parameter synthesis in timed automata and games. The parametric reachability problem is undecidable in general for timed automata [START_REF] Alur | Parametric real-time reasoning[END_REF]. Subclasses with decidable reachability problems include the case of timed automata with a single parametric clock [START_REF] Alur | Parametric real-time reasoning[END_REF], and the L/U timed automata [START_REF] Hune | Linear parametric model-checking of timed automata[END_REF]. The extension of this latter class to timed games were considered recently in [START_REF] Jovanovic | Real-time control with parametric timed reachability games[END_REF] where it is shown that the problem is decidable on L/U timed games. This latter algorithm could be applied to a restriction of our problem with only nonnegative perturbations. In fact, each edge could be redirected to a fresh state controlled by the second player, who is required to choose a perturbation upto δ. However, the general case, or the case of negative perturbations cannot be modelled this way.

The present paper is an extended version of [START_REF] Bouyer | Robust reachability in timed automata: A game-based approach[END_REF] with full proofs, and the extension to turn-based timed games.

Shrinking DBMs

Regions, zones and DBMs

In all timed automata and games we consider, we assume that all clocks are bounded above by a constant. We do not lose generality with this hypothesis since reachability objectives are preserved by choosing a constant large enough, and requiring that all clocks stay below it at any transition. We assume familiarity with the notions of regions and zones, and refer to [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF] for more background. For two regions r and r ′ , we write r ⋖ r ′ if r ′ is the immediate (strict) time-successor of r. A zone is a set of clock valuations satisfying a guard.

We write C 0 for the set

C ∪ {0}. A difference-bound matrix (DBM) is a |C 0 | × |C 0 |-matrix over (R × {<, ≤}) ∪ {(∞, <)}.
We adopt the following notation: for any DBM M , we write M = (M, ≺ M ), where M is the matrix made of the first components, with elements in R ∪ {∞}, while ≺ M is the matrix of the second components, with elements in {<, ≤}. A DBM M naturally represents a zone (which we abusively write M as well), defined as the set of valuations v such that, for all x, y ∈ C 0 , it holds v(x)v(y) ≺ M

x,y M x,y (where v(0) = 0). Conversely, any zone can be represented by a DBM. We will write M ⊆ M ′ to mean that the inclusion holds between the zones defined by the respective DBMs.

We define a total order on (R × {<, ≤}) ∪ {(∞, <)} as follows. We let

(a, ≺) ≤ (b, ≺ ′ ) ⇔    a < b or a = b and either ≺ = ≺ ′ or ≺ ′ = ≤.
The addition is defined by (a, ≺) + (b, ≺ ′ ) = (a + b, ≺ ′′ ), where ≺ ′′ = ≤ if ≺ = ≺ ′ = ≤, and < otherwise. We also let (a, ≺) + b = (a + b, ≺).

For any DBM M , let G(M ) denote the graph over nodes C 0 , where there is an edge (x, y) ∈ C 2 0 of weight M x,y if M x,y < (∞, <). The normalization of M corresponds to assigning to each edge (x, y) the weight of the shortest path in G(M ) from x to y. We say that M is normalized when it is stable under normalization [START_REF] Bengtsson | Timed automata: Semantics, algorithms and tools[END_REF].

Shrinking

Consider the automaton A of Fig. 2, where the goal is to reach ℓ 3 . If there is no perturbation or lower bound on the delays between transitions (i.e., δ = 0), then the states from which Controller can reach location ℓ 3 can be computed backwards. One can reach ℓ 3 from location ℓ 2 and any state in the zone X = (x ≤ 2) ∧ (y ≤ 1) ∧ (1 ≤ xy), shown by (the union of the light and dark) gray areas on Fig. 3 (left); this is the set of time-predecessors of the corresponding guard. The set of winning states from location ℓ 1 is the zone Y = (x ≤ 2), shown in Fig. 3 (right), which is simply the set of predecessors of X at ℓ 2 . When δ > 0 however, the set of winning states at ℓ 2 is a "shrinking" of X, shown by the dark gray area. If the value of the clock x is too close to 2 upon arrival in ℓ 2 , Controller will fail to satisfy the guard x = 2 due to the lower bound δ on the delays. Thus, the winning states from ℓ 2 are described by X ∧ (x ≤ 2δ). Then, this shrinking is backward propagated to ℓ 1 : the winning states are Y ∧ (x ≤ 2 -2δ), where we "shrink" Y by 2δ in order to compensate for a possible perturbation.

An important observation here is that the sets X ∧ (x ≤ 2δ) and (x ≤ 2 -2δ) precisely describe the winning states at respective locations for any δ ≥ 0. Thus, we have a uniform description of the winning states parameterized by δ. In general, we will be able to uniformly describe such sets of winning states "for small enough δ > 0". For instance, if the winning states are described by x ≤ 2 -2δ ∧ x ≤ 1 then the set is non-empty for all δ ∈ [0, 1]. However, we will simplify this set as x ≤ 1, which is equivalent to the above formula for all δ ∈ [0, 1 2 ]. Thus, we give up on computing the winning states for all values of δ, and concentrate on an infinitesimal analysis. These simplifications allow us to compute the state space by a simpler representation, and still provide safe bounds on δ.

We now define shrunk DBMs, a data structure we introduced in [START_REF] Sankur | Shrinking timed automata[END_REF], in order to manipulate "shrinkings" of zones.

Shrunk DBMs

For any interval [a, b], we define the shrinking operator as shrink

-δ • 1 C×{0} and shrink [-δ,δ] (Z) is the DBM Z -δ • 1 C×{0}∪{0}×C , for any δ > 0.
Our aim is to handle these DBMs symbolically. For this, we define shrinking matrices (SM), which are nonnegative integer square matrices with zeroes on their diagonals. A shrunk DBM is then a pair (M, P ) where M is a DBM, P is a shrinking matrix [START_REF] Sankur | Shrinking timed automata[END_REF]. The meaning of this pair is that we consider DBMs M -δP where δ ∈ [0, δ 0 ] for some δ 0 > 0. In the rest of this paper, we abusively say "for all small enough δ > 0" meaning "there exists δ 0 > 0 such that for all δ ∈ [0, δ 0 ]". We also adopt the following notation: when we write a statement involving shrunk DBMs (M, P ), we mean that the statement holds for (M -δP ) for all small enough δ > 0. For instance, (M, P ) = Pre time ((N, Q)) means that M -δP = Pre time (N -δQ) for all small enough δ > 0. In the same vein, shrunk DBMs can be re-shrunk, and we write shrink((M, P )) (resp. shrink + ((M, P )) for the shrunk DBM

(N, Q) such that N -δQ = shrink [-δ,δ] (M -δP ) (resp. N -δQ = shrink [0,δ] (M -δP )) for all small enough δ > 0.
As usual DBMs, shrunk DBMs also have normal forms. Similarly, the normalization of shrunk DBMs can be defined using finite shortest paths in the graph G(M ) of a given DBM M , computed by the Floyd-Warshall algorithm. In order to adapt this algorithm to our data structure, we need to define the basic operations of summation and minimization on shrunk DBMs. We define, ((α, ≺), k) + ((β, ≺ ′ ), l) = ((α + β, ≺ ′′ ), k + l), where ≺ ′′ = ≤ if ≺ = ≺ ′ = ≤ and < otherwise. The comparison of elements is defined as follows.

((α, ≺), k) ((β, ≺ ′ ), l) ⇔    α < β or α = β and k > l, or α = β and k = l and ≺ ′ = < ⇒ ≺ = <. (1)
Intuitively, the smaller constraint is the most restrictive. Note that if ((α, ≺), k) ((β, ≺ ′ ), l), then one can compute δ 0 such that αkδ ≤ βlδ for all δ ∈ [0, δ 0 ]. The minimum is then defined as follows.

min (((α, ≺), k), ((β, ≺ ′ ), l)) = ((α, ≺), k) if ((α, ≺), k) ((β, ≺ ′ ), l), ((β, ≺ ′ ), l) otherwise. (2)
Now, a shrunk DBM (M, P ) is normalized if for all x, y, z ∈ C 0 , (M x,y , P x,y ) ≤ (M x,z , P x,z ) + (M z,y , P z,y ). As one might expect, a shrunk DBM means that the DBMs M -δP are normalized for small enough δ > 0 as shown in the next lemma. Lemma 3.1. For any shrunk DBM (M, P ) that is normalized, there exists δ 0 > 0 such that M -δP is a normalized DBM for all δ ∈ [0, δ 0 ].

Proof. This follows from the fact that there is a finite number of inequalities to satisfy for the normalization of (M, P ), so one can choose δ small enough to satisfy all of them. It follows that for such δ > 0, for all x, y, z ∈ C 0 , M x,y -δP x,y ≺ M

x,y M x,z -δP x,z + M z,y -δP z,y , which means that the DBM M -δP is normalized.

Any shrunk DBM can be made normalized by the Floyd-Warshall shortest paths algorithm applied with the operations defined on shrunk DBMs. Algorithm 1 recalls this procedure, and the next lemma shows it correctness. Let us define norm((M, P )) the normalized shrunk DBM obtained by this procedure.

Data: Shrunk DBM (M, P ) for x ∈ C 0 do for y ∈ C 0 do for z ∈ C 0 do (M, P ) x,y := min((M, P ) x,y , (M, P ) x,z + (M, P ) z,y ); end end end Algorithm 1: Normalization algorithm for shrunk DBMs.

Lemma 3.2. For any shrunk DBM (M, P ), let (M ′ , P ′ ) denote the result of the computation of Algorithm 1. Then, (M ′ , P ′ ) is normalized, and there exists δ 0 > 0 such that for all δ ∈ [0, δ 0 ], M -δP describes the same set as M ′ -δP ′ .

Proof. The fact that (M ′ , P ′ ) is normalized as a shrunk DBM follows by the correctness of the shortest paths algorithm. Furthermore, since the algorithm performs a finite number of operations, all minima computed during the procedure hold for all small enough δ > 0. Therefore, for all δ ∈ [0, δ 0 ], where δ 0 can be computed by updating it at each iteration, M ′ -δP ′ and M -δP are equivalent.

We will now consider shrunk DBMs (M, P ) where M is already normalized as a DBM. In this case, the normalization of the shrunk DBM can be described considering the shortest paths in the constraint graph. We consider paths π = π 1 . . . π n of G(M ) weighted by a given DBM or any matrix, as follows. For a matrix P , the P -weight of π, written P (π), (or the weight of π in P ) is the sum of the weights P πj ,πj+1 for 1 ≤ j ≤ n -1. Recall that M denotes the matrix of the constants of a DBM M (without the inequalities). Definition 3.3. Let M be a normalized DBM. For any x, y ∈ C 0 , we define Π x,y (G(M )) as the set of paths with least and finite M-weight from x to y in G(M ).

Notice that the shortest paths are defined with respect to weights in M and not M . The M -sign of a path π, written sign M (π) is < if ≺ M πi,πi+1 = < for some i, and ≤ otherwise. Finite-weighted shortest paths can be used to characterize the non-emptiness and the normalization of shrunk DBMs. Lemma 3.4. Let M be a normalized non-empty DBM and P be a shrinking matrix. Then, (M, P ) is non-empty if, and only if, for all x ∈ C 0 , there is no path in Π x,x (G(M )) with positive P -weight. Moreover, if (M, P ) is not empty, then, define (M ′ , P ′ ) by letting P ′

x,y be the largest P -weight of the paths in Π x,y (G(M )), and define M ′

x,y = (M x,y , ≺ M ′ x,y ) where ≺ M ′ x,y = < if some path of Π x,y (G(M )) of P -weight P ′

x,y has M -sign <, and ≤ otherwise. Then (M ′ , P ′ ) = norm((M, P )).

Proof. Observe that (M ′ , P ′ ) satisfies the following, for all x, y, z ∈ C 0 ,

M ′ x,y = M ′ x,z + M ′ z,y ⇒ (M ′ x,y , P ′ x,y ) ≺ M ′ x,y (M ′ x,z , P ′ x,z ) + (M ′ z,y , P ′ z,y ). (3)
In fact, the left hand side condition means that (x, z, y) ∈ Π x,y (G(M )), so, by definition of P ′ , P ′ x,y ≥ P ′ x,z + P ′ z,y , where in case of equality, sign M ′ (x, z, y) =< implies ≺ M ′ x,y =< by construction. It follows that (M ′ , P ′ ) is normalized. Now, a normalized DBM is non-empty if, and only if all its diagonal entries are (0, ≤). Therefore, (M, P ) is empty whenever Π x,x (G(M )) has a path with positive P -weight, for some x ∈ C 0 . If any such path has P -weight equal to 0, then ≺ M

x,y =≤ since M is non-empty. The first statement follows.

Remark 3.5. Consider a normalized DBM M and any SM P . If (M ′ , P ′ ) = norm((M, P )), then M ′ = M, M ⊆ M ′ and P ≤ P ′ . This follows from the definition of normalization. In fact, normalization does not change the values M, and if ≺ M ′

x,y = <, then Π x,y (G(M )) has a path with sign <, so ≺ M

x,y = <. That P ≤ P ′ follows from the fact that for all x, y, P ′ x,y is the greatest P -weight of the shortest paths from x to y, so it is at least P x,y .

Here is an example where the signs of the inequalities change due to normalization: Consider x ≤ 1 ∧ 1 ≤ y ∧ xy < 1, which is normalized (seen as a DBM over two clocks). However the

shrinking x ≤ 1 -δ ∧ 1 ≤ y ∧ x -y < 1, yields, after normalization x ≤ 1 -δ ∧ 1 ≤ y ∧ x -y ≤ 1 -δ,
where the last inequality becomes non-strict.

It was shown in [START_REF] Sankur | Shrinking timed automata[END_REF] that when usual operations are applied on shrunk DBMs, one always obtains shrunk DBMs, whose shrinking matrices can be computed. The proof was only given for shrunk DBMs with non-strict inequalities. We recall the constructions, and extend it to shrunk DBMs with both strict and non-strict inequalities. Lemma 3.6 ([36]). Let M, M ′ , N be normalized non-empty DBMs.

1. If N = Pre time (M ), then for all SMs P , there exists a shrunk DBM (N ′ , Q) such that N = N ′ , N ⊆ N ′ and (N ′ , Q) = Pre time ((M, P )). Moreover, Q is obtained from P , by setting Q 0,x = 0 for all x ∈ C and applying normalization.

2. If N = M ∩ O, then for all SMs P and P ′ , there exists a shrunk DBM (N ′ , Q) such that N ′ = N, N ⊆ N ′ and (N ′ , Q) = (M, P ) ∩ (O, P ′ ). Moreover, (N ′ , Q) is given by setting (N ′ x,y , Q x,y ) = min((M x,y , P x,y ), (O x,y , P ′ x,y )) and applying normalization.

3. If N = Unreset R (M ) for some R ⊆ C, then for all SMs P , there exists a shrunk DBM (N ′ , Q)

such that N ′ = N, N ⊆ N ′ and (N ′ , Q) = Unreset R ((M, P )). To obtain (N ′ , Q), first compute (N ′′ , Q ′ ) such that (N ′′ , Q ′ ) = (M, P ) ∩ (R = 0) by previous case, then set all components (x, y) with x ∈ R or y ∈ R, to (N ′′ , Q ′ )
x,y = ((∞, <), 0) and apply normalization.

4. If N = Post time (M ), then for all SMs P , there exists a shrunk DBM (N, Q) such that (N, Q) = Post time ((M, P )). Q can be obtained from P by setting Q x,0 = 0 for all x ∈ C.

5. If (N, Q) = shrink((M, P )), then N = M and Q is obtained from P by incrementing all P x,0 and P 0,x for x ∈ C. For shrink + , one only increments P x,0 , for all x ∈ C.

Proof. The proofs for shrunk DBMs with only non-strict inequalities were given in [START_REF] Sankur | Shrinking timed automata[END_REF], except for the Post time operator which we prove below. Let us recall here the idea and explain the extension to strict inequalities. Assume (M, P ) is normalized. All operations are defined following corresponding ones for usual DBMs. For instance, to compute Pre time ((M, P )), one sets the first row to ((0, ≤), 0), then applies normalization. In fact, for small enough δ > 0, this is precisely the computation of Pre time (M -δP ), seen as a classical DBM. Note that the bound on δ and the types of the inequalities can (only) change during normalization. The rest of the statement follows from Remark 3.5.

However (M, P ) cannot always be assumed to be normalized since P is chosen arbitrarily. If N = f (M ) denotes one of the equations in this lemma, because all operations are non-decreasing, if (M ′ , P ′ ) = norm((M, P )), then N ′′ = f (M ′ ) satisfies N ⊆ N ′′ , and moreover N = N ′′ . The latter equality follows from N ⊆ N ′′ and the fact that any shortest path of N is also a shortest path of N ′′ , though possibly with a different sign. Thus, by Remark 3.5, the lemma yields a shrunk DBM

(N ′ , Q) = f ((M ′ , P )) = f ((M, P )) with N ⊆ N ′ and N = N ′ , as desired.
We now prove the case of Post time . The Post time operation on DBMs simply sets the first column to (∞, <). The resulting DBM is already normalized. Accordingly, we define Q ′

x,y = P x,y for all (x, y) ∈ C 0 × C and Q ′

x,0 = 0 for x ∈ C 0 , and let (N

′ , Q) = norm((N, Q ′ )).
In fact, for small enough δ > 0, this corresponds to setting the first column of N -δQ to ((∞, <), 0) and applying normalization.

Corollary 3.7. Let M = f (N 1 , . . . , N k ) be an equation between normalized DBMs M, N 1 , . . . , N k , using the operators Pre time , Post time , Unreset R , ∩, shrink and shrink + and let P 1 , . . . , P k be SMs. Then, there exists a shrunk DBM

(M ′ , Q) with M ′ = M, M ⊆ M ′ and (M ′ , Q) = f (N 1 , P 1 ), . . . , (N k , P k ) . The shrunk DBM (M ′ , Q
) and a corresponding upper bound on δ can be computed in polynomial time.

Corollary 3.7 shows that shrinking matrices are propagated when usual operations are applied on DBMs. Using this, one can also compute an upper bound on δ, under which a given equation between shrunk DBMs hold. Figure 4 illustrates some of these operations. Notice also that the lemma always gives normalized shrunk DBMs (M ′ , Q).

= Pre time         (a) (M, Q) = Pre time ((N 1 , P )) = ∩ (b) (M, Q) = (N 1 , P 1 ) ∩ (N 2 , P 2 ) = shrink +         (c) (M, Q) = shrink + ((M, P )) = shrink         (d) (M, Q) = shrink((M, P ))
Figure 4: On the right of Fig. 4(a), the gray area represents a zone N 1 , while the dark gray area is some shrinking (N 1 , Q). On the left, the dark area is the shrunk zone (M, P ) where M = Pre time (N 1 ). Similarly, Fig. It is easily observed that shrink [0,δ] (Pre time (M )) is the set of states that can reach M after a delay of length at least δ:

shrink [0,δ] (Pre time (M )) = {v | ∃d ≥ δ, v + d ∈ M }.
This observation is used in the construction of the abstract game in Section 4.

Let us extend the computation of upper bounds on δ in Lemma 3.6 for an inclusion relation, which will be useful later in the proofs (proof of Lemma 3.17). Lemma 3.8. Assume the equation (M, P ) ∩ N ⊆ (N, Q) between normalized shrunk DBMs (M, P ) and (N, Q). One can compute δ 0 > 0, in polynomial time, such that (M -δP

) ∩ N ⊆ N -δQ for all δ ∈ [0, δ 0 ]. Proof. Let N ′ = M ∩ N . Let Q ′ be the SM given by Lemma 3.6 such that (N ′ , Q ′ ) = (M, P ) ∩ N and δ ′ 0 > 0 the corresponding bound on δ. Then, the inclusion is equivalent to (N ′ , Q ′ ) ⊆ (N, Q). Since both shrunk DBMs are normalized, holds if for all x, y ∈ C 0 , either N ′ x,y = N x,y and Q ′ x,y ≥ Q x,y , or N ′
x,y < N x,y . In the former case, N ′ x,y -δQ ′ x,y ≤ N x,y -δQ x,y holds for all δ > 0. In the latter case, it holds for all δ <

Nx,y-N ′ x,y Qx,y-Q ′ x,y
. Thus, we choose

δ 0 = min δ ′ 0 , min N x,y -N ′ x,y Q x,y -Q ′ x,y
, where the inner min is over all pairs x, y ∈ C 0 for which N ′ x,y < N x,y and Q x,y = Q ′ x,y .

Shrinking constraints

We now apply the previous developments to our controller synthesis problem. We will explain the different steps of the computations on the example of Fig. 5. Here, a timed automaton with a single transition is given. From state x = y = 0, Controller has no choice but to suggest a delay of 1. Thus, from region r 0 , the game can reach regions r 1 , r 2 , r 3 , depending on the move of Perturbator. Assuming ℓ and ℓ ′ are not the target state, in order to win, Controller needs a winning strategy at ℓ ′ from all three regions. The idea of our algorithm is to run a forward exploration in order to identify these successor regions r 1 , r 2 , r 3 from which winning strategies need to be found. We will prove that given winning strategies from these successors, one can construct a winning strategy for ℓ as well. However, winning strategies generally require shrinking, as demonstrated in Fig. 3. It is easy to see that not all shrinkings of these regions provide a winning strategy from r 0 ; in fact, r 1 (resp. r 3 ) should not shrink from the right (resp. left) side: their union should include the shaded area, thus points that are arbitrarily close to r 2 . The goal of this section is to study shrinking constraints in order to express this kind of requirements on the shape of the shrinkings of regions. In the next section, we will show how these constraints can be computed by a forward exploration of the regions of a timed automaton, and in Section 3.6, we will show how a winning strategy can be derived once we have these required constraints.

ℓ ℓ ′ x=y=1 y:=0 r 1 r 3 r 0 r ′ 0 r 2
A shrinking constraint is a matrix that specifies which facet of a given zone can be shrunk by a positive parameter, and which ones cannot be shrunk at all. We now give the formal definition. Definition 3.9. Let M be a DBM. A shrinking constraint for M is a |C 0 | × |C 0 | matrix over {0, ∞}. A shrinking matrix P is said to respect a shrinking constraint S if P ≤ S, where the comparison is component-wise. A pair M, S of a DBM and a shrinking constraint is called a constrained DBM.

Shrinking constraints specify which facets of a given zone one is (or is not) allowed to shrink (see Fig. 6). More precisely, these specify if a component of considered shrinking matrices must be 0 or it can also be positive.

  0 x y 0 (0, ≤), 0 (0, <), ∞ (0, <), 0 x (3, <), ∞ (0, ≤), 0 (2, <), 0 y (3, <), ∞ (0, <), ∞ (0, ≤), 0   (a) A constrained DBM M, S and its representation (b) A shrinking of M, S
Figure 6: Consider a zone defined by 0 < x < 3, 0 < y < 3, and 0 < xy < 2. Let the shrinking constraint S be defined by S 0,y = 0, Sx,y = 0, and S z,z ′ = ∞ for other components. The resulting M, S is depicted on the left, as a matrix (where, for convenience, we merged both matrices into a single one) and as a constrained zone (where a thick segment is drawn for any boundary that is not "shrinkable", i.e., with S z,z ′ = 0). On the right, the dark gray area represents a shrinking of M that satisfies S.

We will focus our attention to well shrinking constraints defined below, show that shrinking constraints have a normal form (Subsection 3.4.1), and then show how shrinking constraints can be propagated in order to deduce new shrinking constraints as in the example of Fig. 5 (Subsection 3.4.2).

Normalization and Well-Shrinking Constraints.

A shrinking constraint S for a DBM M is said to be well if for any SM P ≤ S, (M, P ) is non-empty. A well constrained DBM is a constrained DBM given with a well shrinking constraint. We say that a shrinking constraint S for a DBM M is normalized if it is the minimum among all equivalent shrinking constraints: for any shrinking constraint S ′ if for all SMs P , P ≤ S ⇔ P ≤ S ′ , then S ≤ S ′ . Similarly to the normalization of DBMs or SMs, normalized shrinking constraints contain the tightest constraints implied by the original shrinking constraint. They can be normalized by a procedure that is slightly different from the one used for the normalization of DBMs. This is defined formally in the following lemma. Lemma 3.10. Let M be a normalized DBM. For any shrinking constraint S for M , there exists a minimum shrinking constraint S ′ for M such that S ′ ≤ S, and for any normalized non-empty shrunk zone (M, P ), P ≤ S if, and only if, P ≤ S ′ .

Moreover, S ′ can be obtained as follows. Start with S ′ = S. For every pair x, y ∈ C 0 , if S x,y = 0, then set S ′ z,z ′ to 0 for all edges (z, z ′ ) of all paths in Π x,y (G(M )). Also assign S ′ x,y = 0 whenever M x,y = ∞. If S = S ′ , then S is said to be normalized.

Proof. Consider S ′ obtained from S by the above procedure. Obviously, S ′ ≤ S, so that for any SM P ≤ S ′ , we have also P ≤ S. Conversely, consider any normalized non-empty shrunk DBM (M, P ) with P ≤ S ′ , for instance P x,y ≥ 1 for some x, y where S ′

x,y = 0. If S x,y = 0, then clearly, P x,y ≤ S x,y . Otherwise, S x,y = ∞ and S ′

x,y = 0 indicate that there exists z 1 , z 2 ∈ C 0 such that S z1,z2 = 0 and there is a path in Π z1,z2 (G(M )) that goes through edge (x, y). Let us denote this path with π. Then since P is normalized, P z1,z2 ≥ w(π), and since π contains the edge (x, y), we have P z1,z2 ≥ P x,y ≥ 1, therefore P ≤ S.

For any pair x, y ∈ C 0 with S ′ x,y = ∞ let P be the matrix with 0's on all components except for P x,y = 1. Let P ′ be the SM such that (M, P ′ ) = norm((M, P )). The normalization procedure can only increase the components so P ′

x,y ≥ 1. We have P ′ ≤ S ′ , since for any z 1 , z 2 such that S ′ z1,z2 = 0, (x, y) is not on a path of Π z1,z2 (G(M )). So, for any shrinking constraint S ′′ such that S ′′ x,y < S x,y for some x, y, there exists a SM P with P ≤ S ′ and P ≤ S ′′ . Therefore, S ′ is minimal.

Clearly, the normalization of a shrinking constraint depends on the DBM M , since Π x,y (G(M )) depends on G(M ); this is also the case for SMs (Lemma 3.4). In the sequel, unless otherwise stated, all shrinking constraints are assumed to be normalized.

The following property of normalized shrinking constraints is easy to prove, using the previous lemma. Given a shrinking constraint S and a SM P , it will allow us to consider that S is normalized, instead of requiring that P is. Lemma 3.11. Let M be a normalized DBM and S a normalized shrinking constraint. Let P be any SM such that (M, P ) is non-empty, and let (M ′ , P ′ ) = norm((M, P )). Then, P ≤ S if, and only if, P ′ ≤ S.

Proof. Since the normalization procedure for computing P ′ increases the components, the reverse implication holds. Conversely, assume that P ≤ S, and pick x, y ∈ C 0 such that S x,y = 0 (for the other entries, there is nothing to be checked on P ′ ). Then P x,y = 0. From Lemma 3.10, S z,z ′ = 0 for all edges of all paths in Π x,y (G(M )), so that also P z,z ′ = 0 for these edges. Applying the definition of P ′

x,y from Lemma 3.4, we get P ′ x,y = 0.

Propagating Shrinking Constraints.

Let us come back to Fig. 5. Here, starting from the region r 0 given with its well-shrinking constraint, we deduced the shrinking constraints to be satisfied at r 1 , r 2 , r 3 by manually inspecting the figure. Similarly, in order to find a winning strategy, say, from location ℓ ′ , and region r 1 satisfying the corresponding shrinking constraint, one would need to inspect the edges from ℓ ′ , and derive shrinking constraints for those successor regions.

In this subsection, we show a systematic way of deriving the shrinking constraints along elementary operations on DBMs. Lemma 3.12 studies each elementary operation on DBM; each item is illustrated in Fig. 7. Lemma 3.12. Let M, N, O be normalized non-empty DBMs.

1. Assume that M = Pre time (N ). For any normalized well shrinking constraint S for M , there exists a normalized well shrinking constraint S ′ for N such that for any shrunk DBM (N ′ , Q) with N ′ = N, the following holds: Q ≤ S ′ if, and only if, the SM P s.t.

(M ′ , P ) = Pre time ((N ′ , Q)) satisfies P ≤ S. 2. Assume that M = N ∩ O = ∅.
(a) For any normalized well shrinking constraint S for M , there exists a normalized well shrinking constraint S ′ for N such that for any shrunk DBM (N ′ , Q) with N ′ = N and N ′ ∩O = ∅, the following holds: Q ≤ S ′ if, and only if the SM P s.t. (M ′ , P ) = (N ′ , Q)∩O satisfies P ≤ S.

(b) For any normalized well shrinking constraint S for N , there exists a normalized well shrinking constraint S ′ for M such that for any shrunk DBM (M ′ , Q) with M = M ′ and M ⊆ M ′ , the following holds: Q ≤ S ′ if, and only if there exists an SM P ≤ S such that (N, P ) ∩ O ⊆ (M ′ , Q). Moreover, if (N, P ) ∩ O = ∅ for all SMs P ≤ S, then S ′ is a well shrinking constraint.

3. Assume that M = Unreset R (N ). For any normalized well shrinking constraint S for M , there exists a normalized well shrinking constraint S ′ for N such that for any SM Q, the following holds: Q ≤ S ′ if, and only if the SM P s.t.

(M ′ , P ) = Unreset R ((N, Q)) satisfies P ≤ S.
All shrinking constraints S ′ can be computed in polynomial time.

Proof. ◮ Pretime. Observe that M is obtained from N by first setting the first row of N to (0, ≤) (write N ′ for this intermediary DBM) and then applying normalization. Since N is normalized, and we only consider valuations with non-negative values, we have N 0,y ≤ 0 for all y ∈ C. Consider (x, y) ∈ C × C 0 , and a path in Π x,y (N ). If that path does not visit the state 0, then it has the same weight in N ′ as in N . Otherwise, its weight in N ′ is larger than in N , thus it is larger than N ′ x,y . In both cases, N ′ x,y will not change during the normalization phase. So the normalization of N can only change the first row.

Let S ′ x,y = S x,y for (x, y) ∈ C × C 0 , S ′ 0,y = ∞ for y ∈ C, and S ′ 0,0 = 0. We show that S ′ satisfies the desired property. Consider a shrunk DBM (N ′ , Q) with Q ≤ S ′ and N = N ′ , and let P be the shrinking matrix such that (M ′ , P ) = Pre time ((N ′ , Q)). Let us write M ′′ = Pre time (N ′ ). The shrunk DBM (M ′ , P ) is obtained by normalizing the shrunk DBM (M ′′ , Q ′ ) where Q ′ is derived from Q by setting the first row to 0 (Lemma 3.6).

We show that P ≤ S. Observe that M = M ′ = M ′′ so the graphs these DBMs define are the same. First suppose that S x,y = 0 for some x, y ∈ C × C 0 . For such x, y, we have N x,y = M x,y , and since N ′ ⊆ M ′′ , we have Π x,y (G(M )) ⊆ Π x,y (G(N )). Now, we have P x,y > 0 if, and only if there is a path in the former set with positive weight in Q ′ (Lemma 3.4). But this would imply that the same path has positive weight in Q since Q ′ ≤ Q, and moreover this path belongs to Π x,y (G(N )). This would in turn imply that Q x,y > 0, but we have S x,y = S ′

x,y = 0, which contradicts Q ≤ S ′ . It follows that P x,y ≤ S x,y . Now suppose that S 0,y = 0 for some y ∈ C. Since S is assumed to be normalized, along all paths of Π 0,y (G(M )), all edges (z, z ′ ) satisfy S z,z ′ = 0 (Lemma 3.10). Since Q ′ 0,z = 0 for all z, and that Q ′ z,z ′ = Q z,z ′ = 0 for all z, z ′ = 0, we get P 0,y = 0 (Lemma 3.4). Hence P ≤ S. We now show that for any SMs P and Q s

.t. Q ≤ S ′ and (M ′ , P ) = Pre time ((N ′ , Q)), it holds P ≤ S. Consider any SM Q ≤ S ′ such that (w.l.o.g.) (N ′ , Q) is normalized. Then S ′
x,y = 0 and Q x,y ≥ 1 for some x, y. By construction of S ′ , we have x = 0, and S x,y = 0. Moreover, since x = 0, we have M x,y = N x,y , and N x,y < ∞ since Q x,y ≥ 1 and (N ′ , Q) is normalized. Let P denote the normalized SM such that (M ′ , P ) = Pre time ((N ′′ , Q)). P is obtained by letting the first row of Q to zero and applying normalization. We get P x,y ≥ Q x,y ≥ 1, therefore P ≤ S.

To show that S ′ is a well shrinking constraint, assume that for some Q ≤ S ′ , (N ′ , Q) is empty. By definition of S ′ , there exists P ≤ S such that (M ′ , P ) = Pre time ((N ′ , Q)), so (M ′ , P ) is also empty, which contradicts the fact that S is a well shrinking constraint for M . ◮ Intersection (a). For any SMs P, Q, we have (M,

P ) = (N, Q) ∩ O if, and only if (M ′ , P ) = (N, Q) ∩ M for some M ′ = M. So it suffices to consider the equation M = N ∩ M with M ⊆ N . Moreover, notice that ∅ = M = M ∩ N ′ for any N ⊆ N ′ .
We let S ′

x,y = S x,y for any x, y ∈ C 0 such that M x,y = N x,y and S ′ x,y = ∞ otherwise, and make S ′ normalized. Observe that the weight of any path is smaller or equal in G(M ) than in G(N ), since M ⊆ N and both DBMs are normalized. Consider any shrunk DBM

(N ′ , Q) with N = N ′ , N ⊆ N ′ and Q ≤ S ′ and let P such that (M ′ , P ) = (N ′ , Q) ∩ M . Let us write M ′′ = N ′ ∩ M . Again, G(M ) = G(M ′ ) = G(M ′′ ). Here, P is obtained from Q by first defining Q ′ as Q ′ x,y = 0 if M x,y < N x,y and Q ′
x,y = Q x,y otherwise. Then P is the normalization of Q ′ . We show, by induction on n ≥ 2, that for any pair x, y ∈ C 0 with S x,y = 0, any path of Π x,y (G(M )) visiting at most n states have weight 0 in Q ′ . This entails that P x,y = 0 whenever S x,y = 0.

• When n = 2, if M x,y = N x,y , then S ′
x,y = 0 by definition of S ′ , so Q x,y = 0, and Assume now Q ≤ S ′ , i.e., Q x,y ≥ 1 and S ′

Q ′ x,y = 0. If M x,y < N x,y , we have Q ′ x,y = 0 by the definition of Q ′ . • Consider n ≥ 3. Let π = x 1 x 2 . . . x n be a path in Π x,y (G(M )). Since S x
x,y = 0 for some x, y ∈ C 0 . Then we must have M x,y = N x,y and S x,y = 0. Let (M ′ , P ) = (N ′ , Q) ∩ M . We know that P is the normalization of Q ′ , and that Q ′

x,y = Q x,y ≥ 1. So P x,y ≥ Q ′ x,y ≥ 1. Hence P x,y ≤ S x,y . We have that S ′ is a well shrinking constraint for N , since otherwise this would imply that S is not a well shrinking constraint for M , as in the previous case. ◮ Intersection (b). Using the same argument as in the previous case, we can assume that O = M ⊆ N . Since M and N are normalized and non-empty, we have M x,y ≤ N x,y for all x, y ∈ C 0 . We define S ′ 1 by S ′ 1x,y = S x,y if M x,y = N x,y and S ′ 1x,y = 0 otherwise. Let S ′ be defined as

S ′ x,y = max π∈Πx,y(G(M )) S ′ 1 (π). Consider any shrunk DBM (M ′ , Q) with M ′ = M, (M ′ , Q) ⊆ M ,
and Q ≤ S ′ . Let us show that there is (N, P ) with P ≤ S with the desired property. Let us first define Q ′ as follows:

Q ′ x,y =    0 if M x,y < N x,y or S x,y = 0 max z,z ′ :(x,y)∈Π z,z ′ (G(M )) Q z,z ′ if M x,y = N x,y and S x,y = ∞.
Let us write (N ′ , P ) = norm((N, Q ′ )). If S x,y = 0 for some x, y ∈ C 0 , then along all edges (z, z ′ ) ∈ Π x,y (G(N )), we have S z,z ′ = 0, therefore Q ′ z,z ′ = 0. Thus, P x,y = 0 (from Lemma 3.4) and we get P ≤ S.

Let (M ′′ , Q ′′ ) denote the shrunk DBM defined by

(M ′′ , Q ′′ ) = (N ′ , P ) ∩ M with M ′′ = M (Lemma 3.6). Let us show that Q ≤ Q ′′ , which implies, together with M ′′ ⊆ M ⊆ M ′ that (M ′′ , Q ′′ ) ⊆ (M ′ , Q) as desired. Q ′′ is
the normalization of the SM P ′ defined as follows: P ′

x,y = P x,y if M x,y = N x,y and P ′

x,y = 0 otherwise. Let x, y ∈ C 0 .

• Assume that M x,y = N x,y . If S ′ x,y = 0, then Q x,y = 0 so clearly Q ′′ x,y ≥ Q x,y . Otherwise, there exists a path π ∈ Π x,y (G(M )) such that for some edge (z, z ′ ) ∈ π, M z,z ′ = N z,z ′ and S z,z ′ = ∞. By definition of Q ′ , we have Q ′ z,z ′ ≥ Q x,y . Moreover P ′ z,z ′ = P z,z ′ ≥ Q z,z ′ . The normalization of P ′ then yields Q ′′ x,y ≥ P ′ z,z ′ = P z,z ′ ≥ Q z,z ′ ≥ Q x,y . • Otherwise, M x,y < N x,y . If S ′
x,y = 0, the result is clear. If S ′ x,y = ∞, then there must be a path in Π x,y (G(M )) with an edge (z,

z ′ ) with M z,z ′ = N z,z ′ and S z,z ′ = ∞. Then, Q ′ z,z ′ ≥ Q x,y . So the normalization of P ′ yields Q ′′ x,y ≥ P ′ z,z ′ = P z,z ′ ≥ Q ′ z,z ′ ≥ Q x,y .
We now show the converse direction. Consider any x, y ∈ C 0 such that S ′ x,y = 0. Let us show that for any (N, P ) with P ≤ S, if (M ′ , Q ′′ ) denotes the shrunk DBM such that (M ′ , Q ′′ ) = M ∩ (N, P ), then Q ′′

x,y = 0. This proves that if Q x,y ≥ 1 for some SM Q, then there is no matching P ≤ S that satisfies the property.

We show, by induction on n ≥ 2, that if S ′ x,y = 0, then all paths of Π x,y (G(M )) of length at most n have weight zero in P ′ .

• Let n = 2. If M x,y = N x,y , then P ′

x,y = P x,y . But we have S x,y = 0, so P x,y = 0. If M x,y < N x,y , then P ′

x,y = 0 by definition. We now show that S ′ is a well shrinking constraint for M , given the hypothesis that (N, P )∩M = ∅ for all SMs P ≤ S. But this immediately implies that S ′ is a well shrinking constraint, since for any

• If n ≥ 3, consider any path π = x 1 x 2 . . . x n in Π x,y (G(M )). Suppose that M xj ,xj+1 = N xj ,xj+1 for all 1 ≤ j ≤ n -1. Then π is also a shortest path in G(N ), hence M x,y = N x,
Q ≤ S ′ there exists P ≤ S with ∅ (N, P ) ∩ M ⊆ (M, Q). ◮ Unreset. Let N R denote the DBM that defines the (largest) zone satisfying ∧ x∈R x = 0. Since we have M = Unreset R (N ∩ N R )
, by the previous case, we may assume that N ⊆ N R . The DBM M is obtained from N by replacing each component (x, y) with x ∈ R by ∞. For any y ∈ C 0 , we define S ′′

x,y = S x,y if x ∈ C \ R, and S ′′ 0,y = 0, and

S ′′ x,y = ∞ if x ∈ R. Then S ′ is obtained by normalizing S ′′ .
Let Q be any normalized SM with Q ≤ S ′ , and P be the (normalized) SM such that (M ′ , P ) = Unreset R ((N, Q)). Let Q ′ denote the SM obtained from Q by setting each component (x, y), with x ∈ R, to zero. Then, P is the normalization of Q ′ . Let us show that P ≤ S. Consider any x, y ∈ C 0 with S x,y = 0.

• If x ∈ C \ R then S ′
x,y = S x,y = 0 and Q x,y = 0. So, along all paths Π x,y (G(N )), S ′ is zero, and so are the weights in Q, and also the weights in Q ′ . Now, clearly, Π x,y (G(M )) ⊆ Π x,y (G(N )). So after normalization of Q ′ , we have P x,y = 0.

• If x = 0, then S ′

x,y = 0 and Q x,y = 0. The argument is then similar.

• If x ∈ R, then M x,y = ∞. Thus Π x,y (G(M )) = ∅, so the normalization of Q ′ yields P x,y = 0.
Consider a normalized SM Q with Q ≤ S ′ . We must have Q x,y ≥ 1 and S ′′ x,y = 0 for some x, y ∈ C 0 , by Lemma 3.10. The latter condition entails that x / ∈ R. Let Q ′ denote the DBM obtained from Q by replacing all components (x, y) where x ∈ R with 0. Then the normalization of Q ′ yields the SM P such that (M

′ , P ) = Unreset R ((N, Q)). Since x ∈ C 0 \ R, then S x,y = S ′
x,y = 0 and Q ′

x,y = Q x,y ≥ 1. The normalization of Q ′ can only increase its components, so P x,y ≥ 1, hence P ≤ S.

We show that S ′ is a well shrinking constraint for N as in the previous cases.

= Pre time         (a) (M ′ , P ) = Pre time ((N, Q)) = ∩ (b) (M ′ , P ) = (N, Q) ∩ N ′ ∩ ⊆ (c) (N, P ) ∩ N ′ ⊆ (M, Q) = Unreset R         (d) (M ′ , P ) = Unreset R ((N, Q))
Figure 7: Each of the figures illustrates one item in Lemma 3.12. In each case, DBMs M , N and N ′ are fixed and satisfy the "unshrunk" equation (that is, when P = Q = 0). The thick plain segments represent the fixed shrinking constraint S. The thick dashed segments represent the shrinking constraint S ′ that is constructed. In each case, if a SM Q is chosen, it holds that Q ≤ S ′ iff there is an SM P ≤ S that satisfies the equation. For instance, if Q x,0 ≥ 1 in (a), then the DBM describing the time predecessors of (N, Q) shrinks the diagonal component (x, y), which violates S.

We now extend the previous lemma to the operator shrink + . In this case, the existence of a shrinking constraint depends on the given constrained DBM. The lemma is illustrated in Fig. 8. Lemma 3.13. Let M be a normalized non-empty DBM and S be a normalized shrinking constraint.

• If M x,0 < ∞ and S x,0 = 0 for some x ∈ C, then for all SMs Q, the shrunk DBM (M ′ , P ) = shrink + ((M, Q)) does not satisfy P ≤ S.

• Otherwise, for all SMs Q, the following holds: Q ≤ S if, and only if, the shrunk DBM (M ′ , P ) = shrink + ((M, Q)) satisfies P ≤ S.

Proof. If S x,0 = 0 and M x,0 < ∞ for some x ∈ C, since shrink + increases each (but one) component of the first column of the SM by one, and since the normalization can only increase components for which M x,0 < ∞, there is no P ≤ S such that (M ′ , P ) = shrink + ((M, Q)).

Assume that S x,0 = ∞ for all x ∈ C with M x,0 < ∞. Consider any Q ≤ S. The operator shrink + increments all components (x, 0) of the SM by one, and applies normalization. So if Q x,y > S x,y = 0 for some x, y ∈ C, we know that if P denotes the SM such that (M ′ , P ) = shrink + ((M, Q)), then P x,y ≥ Q x,y > 0, since shrink + only increases the components of the SM. Thus, for SMs Q ≤ S, there is no corresponding P ≤ S with the desired property. Consider now any Q ≤ S, and P such that (M ′ , P ) = shrink + ((M, Q)). Assume that P x,y ≥ 1 for some S x,y = 0. We have M x,y < ∞ since (M ′ , P ) is normalized. Since Q x,y = 0, there exists a path in Π x,y (G(M )) that contains an edge (z, 0) such that Q z,0 = 0, and P z,0 ≥ 1. But then S z,0 = 0, which contradicts our assumption.

Let us comment on Fig. 7, the figure about Pre time , and how it can be used for our purpose. Assume there is an edge guarded by N (the whole gray area in the right) without resets. In the non-robust setting, this guard can be reached from any point of M (the whole gray area in the left). If we have a shrinking constraint S on M , and we want to synthesize a winning strategy from a shrinking of M satisfying S, then Lemma 3.12 gives the shrinking constraint S ′ for N , with the following property: given any shrinking (N, Q), we can find P ≤ S with (M, P ) = Pre time ((N, Q)) (hence, we can delay into (N, Q)), if, and only if Q satisfies Q ≤ S ′ . The problem is now "reduced" to finding a winning strategy from N, S ′ . However, forward-propagating these shrinking constraints is not always that easy. We also need to deal with resets, with the fact that Controller has to choose a delay greater than δ > 0, and also with the case where there are several edges leaving a location. This is the aim of the following developments.

= shrink +         (a) (M ′ , P ) = shrink + ((M, Q)) but P ≤ S = shrink +         (b) (M ′ , P ) = shrink + ((M, Q)) with P ≤ S.

Neighborhoods

We studied in the previous section the propagation of shrinking constraints along DBM operations. The last step before we can fully treat the propagation of these constraints along a transition is to take into account the perturbations. For instance, in Fig. 5, given Controller's move to the point x = y = 1, we need a systematic way of deriving the neighboring regions spanned by the perturbations. This will allow us to compute the set of all successor regions reachable under a transition.

We consider constrained regions, which are constrained DBMs in which the DBM represents a region. We define the set of neighboring regions of a constrained region r, S as, N r,S = s s ⋖ * r or r ⋖ + s, and ∀Q ≤ S. s ∩ enlarge((r, Q)) = ∅ where enlarge((r, Q)) is the shrunk DBM (M, P ) such that v + [-δ, δ] ⊆ M -δP for every v ∈ r -δQ. This is the set of regions that have "distance" at most δ to any shrinking of the constrained region (r, S). We write neighbor r, S = s∈N r,S s. Lemma 3.14 (Neighborhood). Let r, S be a well constrained region. Then neighbor r, S is a zone. If N is the corresponding normalized DBM, there exists a well shrinking constraint S ′ such that for every SM Q, Q ≤ S ′ iff the SM P defined by (r ′ , P ) = r ∩ shrink((N, Q)), satisfies P ≤ S. The pair N, S ′ is the constrained neighborhood of r, S , and it can be computed in polynomial time. Moreover, the constraint S ′ is such that S ′

x,y = S x,y for every x, y ∈ C, and S ′ x,0 = S ′ 0,x = ∞ for every x ∈ C.

Constrained neighborhoods are illustrated in Fig. 9. To prove Lemma 3.14 which states the properties of the neighborhoods of constrained regions, we first need to introduce some notations and simple facts about constrained regions.

neighbor         = neighbor         =
Let r, S be a constrained region. There exists a unique partition X 1 , . . . , X n of the clocks such that for all valuations ν ∈ r, frac(ν(x)) = frac(ν(y)) for all x, y ∈ X i , for any 1 ≤ i ≤ n, and frac(ν(x)) < frac(ν(y)) if x ∈ X i and y ∈ X j for any 1 ≤ i < j ≤ n. We assume that frac(ν(x)) = 0 for all x ∈ X 1 . So X 1 may be empty, but other X i 's are non-empty. In the sequel, when we consider a region, the above partition is called partition of clocks according to their fractional values. Lemma 3.15. Let r, S be a constrained region and consider the partition X 1 , . . . , X n of clocks according to their fractional values. Then, for all x, y ∈ X i for any 1 ≤ i ≤ n, we have S x,y = 0, and for all x ∈ X 1 , we have S x,0 = S 0,x = 0. Moreover,

• There exists 2 ≤ i 0 ≤ n + 1 such that for any x ∈ X i with i 0 ≤ i ≤ n, S x,0 = 0, for any y ∈ X i ′ with i ≤ i ′ ≤ n, S x,y = 0, and for any x ∈ X i with 1 ≤ i < i 0 , S x,0 = ∞.

• There exists 1 ≤ j 0 ≤ n such that for any x ∈ X j with 1 ≤ j ≤ j 0 , S 0,x = 0, for any y ∈ X j ′ with 1 ≤ j ′ < j, S y,x = 0, and for any x ∈ X j with j 0 + 1 ≤ j ≤ n, S 0,x = ∞.

Proof. This follows from the normalization of S. In fact, suppose S x,0 = 0 for some x ∈ X i with i ≥ 2, and consider y ∈ X j for any i < j ≤ n. Then (x, y, 0) is a shortest path in G(r). Therefore, we must have S x,y = S y,0 = 0. One can then choose i 0 as minimal to satisfy this statement, and j 0 maximal.

Let us make some remarks about the graphs of regions and their shrinking constraints. Consider a region r. For any x ∈ X i , y ∈ X j and z ∈ X k with i < j < k, (x, y, z) and (z, x, y) are shortest paths in G(r). In fact, r x,z = r x,y + r y,z since r x,y = r x,0r y,0 , r y,z = r y,0r z,0 , and r x,z = r x,0r z,0 . Similarly, r z,x = r z,0r x,0 + 1 and r z,y = r z,0r y,0 + 1 yield r z,y = r z,x + r x,y . A shrinking constraint S with S x,y = 0 means that a shrinking of r satisfying S, contains valuations ν with frac(ν(y))frac(ν(x)) ≤ ǫ for any ǫ > 0. If S y,x = 0, this means that some valuations ν satisfy frac(ν(y))frac(ν(x)) ≥ 1ǫ.

Proof of Lemma 3.14. Let us prove that the neighborhood is a zone, and show how to compute it. We characterize the successor regions of r that belong to the neighborhood of r, S . The predecessor regions can be charaterized similarly. Consider the partition of clocks in r ordered according to their fractional parts:

0 = frac(X 1 ) < frac(X 2 ) < . . . < frac(X m ) < 1,
where X i 's are subsets of clocks having the same fractional part, and X 1 is possibly empty.

• First, assume that S x,0 = ∞ for x ∈ X m . Consider the case

X 1 = ∅. Consider any SM Q ≤ S such that Q x,0 ≥ 2 for all clocks x ∈ X 2 ∪ . . . X m .
Then for all ν ∈ (r -δQ), we have frac(ν(x)) ≤ 1 -2δ for all clocks x. We have, for any t ∈ [0, δ], frac(ν(x) + t) < 1. So no region s with r ⋖ s is included in the neighborhood. If S x,0 = ∞ for x ∈ X m but X 1 = ∅, then necessarily S x,0 = S 0,x = 0 for x ∈ X 1 since S is a well shrinking constraint. Then, the neighborhood contains the region s with r ⋖ s but no successor of s, which is shown as above.

• Assume that S x,0 = 0 for x ∈ X m . Let i ∈ {1, . . . , m} be minimum such that X i is nonempty and S x,0 = 0 for all x ∈ X j and i ≤ j ≤ m. 1 Then, for any 1 ≤ j ≤ i -1 and x ∈ X j S x,0 = ∞ by Lemma 3.15. Let s be the unique region that satisfies r ⋖ + s, s x,0 = r x,0 + 1 and ≺ s x,0 =< for all x ∈ X i , and s x,0 = r x,0 for all x ∈ X i-1 . We show that the neighborhood of r, S contains all regions t such that r ⋖ * t ⋖ * s, but no region t such that s ⋖ + t. Let (r, Q, δ 0 ) be a well-shrinking and consider any δ ∈ [0, δ 0 ]. For any x ∈ X j for max(2, i) ≤ j ≤ m, we have r x,0 -δQ x,0 = r x,0 , and -r 0,x + δQ 0,x < r x,0 (in fact ≺ r x,0 =< for these clocks). Let ǫ < min(δ/2, r x,0 -(-r 0,x + δQ 0,x )) for all x ∈ X j and max(2, i) ≤ j ≤ m, so that -r 0,x + δQ 0,x < r x,0ǫ < r x,0 . By a folklore result [24, Lemma 4], there exists a valuation ν ∈ (r -δQ) such that r x,0ǫ < ν(x) < r x,0 for x ∈ X max(2,i) . Define d j = 1frac(ν(x)) for x ∈ X j for all i ≤ j ≤ m. We know by the fractional ordering that 0

< d m < d m-1 < . . . < d i < δ/2. Define also d ′ j = dj +dj-1 2
for all i + 1 ≤ j ≤ m, and

d m+1 = dm 2 . If i = 1, then we have reg(ν) ⋖ reg(ν + d m+1 ) ⋖ reg(ν + d m ) ⋖ reg(ν + d ′ m ) ⋖ reg(ν + d m-1 ) ⋖ . . . ⋖ reg(ν + d i ),
and for ǫ ′ > 0 small enough, reg(ν

+ d i ) ⋖ reg(ν + d i + ǫ ′ ) = s. If i > 1, we remove reg(ν + d m+1 )
since this is equal to reg(ν). Let us show now that the time-successor of s is not included in the neighborhood. In fact, if i = 1, then, the immediate time successor of s is the unique region r ⋖ + t such that -t 0,x = t x,0 = r x,0 + 1 and ≺ t x,0 =≤ for x ∈ X 1 . But for all ν ∈ (r -δQ), we have ν(x) = r x,0 , so ν(x) + δ < t x,0 . If i = 2 and X 1 = ∅, then the immediate time successor t of s satisfies -t 0,x = t x,0 = r x,0 + 1 for x ∈ X m . But since for any ν ∈ r, ν(x) + δ < t x,0 , t is not in the neighborhood. If i ≥ 2 and X i-1 = ∅, then the proof is similar since the immediate time successor of s is the region where clocks in X i-1 become integer. The case of the time-predecessors of r is treated similarly.

From the proof above we can directly define the DBM N that represents the neighborhood of r, as follows. N has the same diagonal constraints as r, so N x,y = r x,y for all x, y ∈ C. For all x ∈ X 1 , we let N x,0 = r x,0 + 1 and ≺ N x,0 =<, and if r 0,x < 0, we let N 0,x = r 0,x + 1 and ≺ N 0,x =<, otherwise N 0,x = r 0,x = 0 and ≺ N 0,x =≤. If S x,0 = ∞ for all x ∈ X 2 ∪ . . . ∪ X m , then r x,0 = N x,0 for all x. Otherwise, let i ∈ {2, . . . , m} minimum such that S x,0 = 0 for all x ∈ X j for all i ≤ j ≤ m. We let N x,0 = r x,0 + 1 and ≺ N x,0 =< for all x ∈ X i ∪ X i+1 ∪ . . . ∪ X m , and N x,0 = r x,0 , ≺ N x,0 =≺ r x,0 for all x ∈ X 2 ∪ . . . ∪ X i-1 . Symmetrically, if S 0,x = ∞ for all x ∈ X 2 ∪ . . . ∪ X m , we let N 0,x = r 0,x and ≺ r 0,x =≺ N 0,x . Otherwise, let i ′ ∈ {2 . . . , m} be maximum such that S 0,x = 0 for all x ∈ X j for all 2 ≤ j ≤ i ′ . For all x ∈ X j and 1 ≤ j ≤ i ′ , if r 0,x < 0, we let N 0,x = r 0,x + 1 and ≺ N 0,x =<, and otherwise N 0,x = 0 and ≺ N 0,x =≤. We let N 0,x = r 0,x , ≺ N 0,x =≺ r 0,x for all x ∈ X i ′ +1 ∪ . . . ∪ X m . Let S ′ be the shrinking constraint given by Lemma 3.12, for which for all SMs Q, Q ≤ S ′ if, and only if there exists P ≤ S with (r ′ , P ) = r ∩ (N, Q) with r ′ = r. From the proof of this lemma, S ′ is the normalization of the following shrinking constraint: we let S ′

x,y = S x,y for all x, y ∈ C, since r x,y = N x,y . For all x ∈ C, S ′

x,0 = S x,0 if r x,0 = N x,0 and S ′ x,0 = ∞ otherwise. But by construction of N , r x,0 = N x,0 only if S ′

x,0 = ∞ so we get S ′ x,0 = ∞ for all clocks. Similarly, we get S ′ 0,x = ∞ for all x ∈ C. We are going to show that S ′ is already normalized. Consider any x ∈ C. To get a contradiction, suppose that there exists z, z ′ ∈ C with S ′ z,z ′ = S z,z ′ = 0 and a path x 1 . . . x n in Π z,z ′ (G(N )) that contains the edge (x, 0) -which would imply that S ′

x,0 becomes 0. Since r z,z ′ = N z,z ′ , we have Π z,z ′ (G(N )) ⊆ Π z,z ′ (G(r)). Then, S x,0 = 0 since S is normalized. But this means N x,0 = r x,0 + 1 by definition of N , and this path cannot be a shortest path in

G(N ) (in fact, N z,z ′ = r z,z ′ = n-1 k=1 r xi,xi+1
). Consider now x, y ∈ C such that S x,y = ∞ and let us show that S ′

x,y = ∞ after normalization. Suppose there exists a path π ∈ Π z,z ′ (G(N )) where z, z ′ = 0, S z,z ′ = S ′ z,z ′ = 0 and the edge (x, y) belongs to π. If 0 does not appear in π, then this path also belongs to Π z,z ′ (G(r)), since r z,z ′ = N z,z ′ and all edges have the same weight in both graphs, so we would have S x,y = 0. So, assume that some edges (w, 0) and (0, w ′ ) belong to π. If S w,0 = S 0,w = ∞, then r w,0 = N w,0 and r 0,w = N 0,w by definition of N , so π is a shortest path in G(r), which contradicts S x,y = ∞. But, if S w,0 = 0 or S 0,w = 0 then N w,0 = r w,0 + 1 or N 0,w = r 0,w + 1, and in this case π is not a shortest path in G(N ) since N z,z ′ = r z,z ′ . Hence, there is no such path π, and we get S ′

x,y = ∞ after normalization. Now, let Q ′ be such that (N ′ , Q ′ ) = shrink((N, Q)). If Q ′′ denotes the SM obtained from Q ′ by incrementing by one each component of the first row and the first column (except cell (0, 0)), then

(N ′ , Q ′ ) = norm((N, Q ′′ )). Moreover, because S ′ x,0 = S ′ 0,x = ∞ for all x ∈ C, we have Q ′ , Q ′′ ≤ S ′′ .
Then, by definition of S ′ , there exists P ≤ S such that (r

′ , P ) = r ∩ (N, Q ′ ). Conversely, if Q ≤ S ′ , then Q ′ ≤ S ′ . So, if there exists P such that (r ′ , P ) = r ∩ (N, Q ′ ), then P ≤ S, by definition of S ′ .
The fact that S ′ is a well shrinking constraint for N follows from the fact that S is a well shrinking constraint for r. In fact, for any Q ≤ S ′ , there exists P ≤ S such that (r ′ , P ) = r ∩ shrink((N, Q)) and (r ′ , P ) is non-empty by hypothesis, so (N, Q) cannot be empty.

Controllable Predecessors

Now that we have the notions required to reason with shrinking constraints and neighborhoods, we will show how one can compute controllable predecessors given one transition. For instance, in Fig. 5, given winning states at location ℓ ′ inside regions r 1 , r 2 , r 3 given as shrunk DBMs satisfying the corresponding shrinking constraints, we will show how to combine these to derive a winning state inside r 0 at location ℓ.

The following lemma characterizes, given a constrained region r, S , the set of constrained regions s, S s such that any shrunk region satisying s, S s can be reached by delaying from some shrunk region satisfying r, S . These are the sets whose reachability can be ensured by Controller by a delay. Lemma 3.16. Let r, S be a well constrained region, and s be a region such that r ⋖ * s. Then the following properties are equivalent:

1. there exists a well shrinking constraint S ′ (which can be computed in polynomial time) such that for every SM Q, Q ≤ S ′ iff the SM P such that (r ′ , P ) = r ∩ shrink + (Pre time ((s, Q))) for some r ′ = r satisfies P ≤ S;

2. neighbor r, S ⊆ Pre time (s);

3. define N = Pre time (s), and S N such that for all SM Q, Q ≤ S N iff the SM P defined by (r ′ , P ) = r ∩ (N, Q) with r ′ = r satisfies P ≤ S. Then (S N ) x,0 = ∞ for all x ∈ C.

Proof. ◮ 3 ⇒ 1. Let S ′ be such that for all SMs Q, Q ≤ S ′ if, and only if there is

Q ′ ≤ S N with (N ′ , Q ′ ) = Pre time ((s, Q))
and N ′ = N. We will show that S ′ satisfies the required condition. We first assume that Q ≤ S ′ . By Lemma 3.13, there exists

Q ′′ ≤ S N such that (N ′′ , Q ′′ ) = shrink + ((N ′ , Q ′ )) = shrink + (Pre time ((s, Q))) for N ′′ = N.
And by definition of S N , there exists P ≤ S such that (r

′ , P ) = r ∩ (N ′′ , Q ′′ ) for some r ′ = r. Conversely, if Q ≤ S ′ , then if Q ′ denotes the SM such that (N ′ , Q ′ ) = Pre time ((s, Q)), then Q ′ ≤ S N . By Lemma 3.13, if Q ′′ denotes the SM such that (N ′′ , Q ′′ ) = shrink + ((N ′ , Q ′ )), then Q ′′ ≤ S N .
Therefore, there is no SM P such that (r ′ , P ) = r ∩ shrink + (Pre time ((s, Q))).

◮ not 2 ⇒ not 1. Let V, S ′ = neighbor r, S . We assume that V ⊆ N = Pre time (s). Then, if t denotes the region s ⋖ t, we have s, t ⊆ V . By definition of the neighborhood, for any SM P ≤ S r , when δ is small enough, there exists a valuation v ∈ r -δP such that v + d ′ ∈ t for some 0 ≤ d ′ ≤ δ. But since s ⋖ t, v + d ′ ∈ s for some d ′ ≥ 0 implies that 0 ≤ d ′ < δ (and there exists 0 ≤ d ′ < δ with v + d ′ ∈ r ′ ). Therefore, for any SM Q, if P denotes the SM such that (r ′ , P ) = r ∩ shrink + (Pre time ((s, Q))) with r ′ = r, then P ≤ S: indeed, if P ≤ S, then for small enough δ > 0, v + [0, δ] ⊆ Pre time (s -δQ) and in particular v + δ ∈ Pre time (s -δQ), which implies that there is d ′′ ≥ 0 such that v + δ + d ′′ ∈ s -δQ ⊆ s, contradicting the above remark. ◮ 2 ⇒ 3. Let (V, S ′ ) = neighbor r, S . We have r ⊆ V ⊆ N . Let (N ′ , Q) be a normalized shrunk DBM with N = N ′ , obtained by setting Q x,0 = 1 for all x ∈ C and 0 all other components. Let

Q ′ be the SM such that (V ′ , Q ′ ) = V ∩ (N ′ , Q), for some V ′ = V. • We show that Q ′ ≤ S ′ . Define (Q 1 ) x,y = Q x,y if V x,y = N x,y and (Q 1 ) x,y = 0 otherwise. Q ′ is the normalization of Q 1 . We have S ′ x,0 = S ′ 0,x = ∞ by Lemma 3.14, so Q ′ x,0 ≤ S ′
x,0 and Q ′ 0,x ≤ S ′ 0,x . For any x, y ∈ C, we assume S ′ x,y = 0. It implies S x,y = 0. To get a contradiction, assume that there is a path in Π x,y (G(V )) with an edge (z, z ′ ) such that V z,z ′ = N z,z ′ and Q z,z ′ ≥ 1. Since Q z,z ′ ≥ 1, there must be a path in Π z,z ′ (G(N )) that contains an edge (α, 0). But since Π z,z ′ (G(N )) ⊆ Π z,z ′ (G(V )), there is a path in Π x,y (G(V )) that contains the edge (α, 0). This contradicts S ′

x,y = 0 since we know, by Lemma 3.14 that S ′ α,0 = ∞.

• We now show that Q ≤ S N , which implies the desired result. By Lemma 3.14, there exists P ≤ S such that (r ′ , P ) = r ∩ shrink((V ′ , Q ′ )), for some r ′ = r. But, if P ′ denotes the SM such that (r ′′ , P ′ ) = r ∩ (V ′ , Q ′ ), then P ′ ≤ P ≤ S because shrink can only increase the components of the SM. Therefore, (r

′′ , P ′ ) = r ∩ V ∩ (N, Q) = r ∩ (N, Q).
Thus, by Lemma 3.12, we must have Q ≤ S N , which implies (S N ) x,0 = ∞ for all x ∈ C.

We now assume that the above conditions hold, and prove that S ′ (of item 1) has the same diagonal constraints as S. By Lemma 3.12, S N is computed as the normalization of S ′ , which is defined for every x, y ∈ C 0 as S ′

x,y = S x,y if N x,y = r x,y and ∞ otherwise. Since N and r have the same diagonal constraints, S x,y = 0 for x, y ∈ C implies (S N ) x,y = 0. If S x,y = ∞, suppose that (S N ) x,y = 0. There exist z, z ′ such that (x, y) belongs to a path in Π z,z ′ (G(N )), and S ′ z,z ′ = 0. But this implies that r z,z ′ = N z,z ′ and S z,z ′ = 0. We have then Π z,z ′ (G(N )) ⊆ Π z,z ′ (G(r)) since r ⊆ N , and this contradicts that S x,y = ∞. We now show that S ′ has the same diagonal components as S N . In fact, S ′ is the normalization of S ′ N defined by (S ′ N ) 0,x = ∞ for all x ∈ C and (S ′ N ) x,y = (S N ) x,y for other x, y ∈ C 0 . Clearly, (S N ) x,y = 0 for any x, y ∈ C implies S ′

x,y = 0. Assume that S ′ x,y = 0 with x, y ∈ C. Then (x, y) belongs to a path π ∈ Π z,z ′ (G(s)) with (S ′ N ) z,z ′ = 0, so necessarily z = 0 and s z,z ′ = N z,z ′ . If π does not contain the node 0, then π ∈ Π z,z ′ (G(N )) since all other weights are the same in G(s) and G(N ). If it contains node 0, then π still must be in Π z,z ′ (G(N )). In fact, (S ′ N ) z,z ′ = 0 means that N z,z ′ < ∞ and since all weights are the same in G(s) and G(N ) except for the edges (0, z) which can only decrease in s, π is a shortest path in both graphs. In both cases, we get (S N ) x,y = 0.

That S ′ is a well shrinking constraint for s follows from the hypothesis that S is a well shrinking constraint for r. In fact, if for some Q ≤ S ′ , (s, Q) is empty, then the corresponding (r, P ) (defined in item 1) is empty, which is a contradiction.

Note that this lemma may not hold for all s with r ⋖ s. Consider the constrained region r, S on the right of Fig. 9, and let s be the first triangle region above r: any valuation arbitrarily close to the thick segments will be in r -δP for any P ≤ S, but it can only reach s by delaying less than δ time units.

The following lemma describes sets of states from where Controller can ensure reaching a given set, through an action. Intuitively, given a constrained region and its constrained neighborhood, we show how to compute the shrinking constraints on the successor regions (through a given edge), such that Controller can make sure that given shrunk DBMs of the successor regions are reached. Lemma 3.17. Let r, S be a well constrained region, and let R ⊆ C. Let N = {s 1 , . . . , s m } be the set of neighboring regions of r, S , and define t i = s[R ← 0] for each 1 ≤ i ≤ m. Then, there exist well shrinking constraints S ti for all t i such that for any set of shrunk DBMs

(t ′ i , Q t ′ i ) 1≤i≤m with t i = t ′ i , we have that Q t ′ i ≤ S ti for all 1 ≤ i ≤ m if,
and only if there exists P ≤ S such that

(r ′ , P ) ⊆ r ∩ shrink( 1≤i≤m (s ∩ Unreset R ((t ′ i , Q t ′ i )))).
for some r ′ = r. Moreover, all the t i , S ti can be computed in polynomial time.

Proof. It is useful to remember in this proof that t i = t ′ i implies t i ⊆ t ′ i since t i is a region. Let N, S ′ be the (well) constrained neighborhood of r, S , given by Lemma 3.14. For any region s ∈ N , let S s be the well shrinking constraint given by Lemma 3.12, such that for all shrunk DBMs (s ′ , Q) with s ′ = s and s ⊆ s ′ , Q ≤ S s if, and only if there exists P ≤ S ′ with s ∩ (N, P ) ⊆ (s ′ , Q). Here, S s is in fact a well shrinking constraint since s ∩ (N, P ) = ∅ for all P ≤ S ′ , by the construction of the neighborhood. Then, let us write t = s[R ← 0], and let S ′ s be the well shrinking constraint given by Lemma 3.12, such that for any shrunk DBM (t ′ , Q t ) with t = t ′ and t ⊆ t ′ , Q t ≤ S ′ s if, and only if there exists P s ≤ S s with (s ′ , P s ) = s ∩ Unreset R ((t ′ , Q t )) for some s ′ = s with s ⊆ s ′ . We let S t = min s∈N :t=s[R←0] S ′ s , where the minimum is taken componentwise. Then S t is still a well shrinking constraint. Now, S t satisfies the following property: for any shrunk DBM (t ′ , Q t ) with t ′ = t and t ⊆ t ′ , Q t ≤ S t if, and only if for all regions s ∈ N with t = s[R ← 0], there exists P s ≤ S s such that (s ′ , P s ) = s ∩ Unreset R ((t ′ , Q t )) for some s ′ with s ′ = s and s ⊆ s ′ . Combining this and S ′ defined above, we get that S t has the property that for any shrunk DBMs (t ′ , Q t ) with t ′ = t and t ⊆ t ′ , Q t ≤ S t if, and only if for all s ∈ N with t = s[R ← 0], there exists

P s ≤ S ′ such that s ∩ (N, P s ) ⊆ s ∩ Unreset R ((t ′ , Q t )).
For any family of shrunk DBMs

{(t ′ i , Q t ′ i )} 1≤i≤m with t i ⊆ t ′ i , t i = t ′ i and Q t ′ i ≤ S ti
, consider the set {P s } s∈N as defined above. Let P ′ = max s∈N (P s ), where the max is componentwise. We have P ′ ≤ S ′ since P s ≤ S ′ for all s ∈ N . We have s ∩ (N,

P ′ ) ⊆ s ∩ Unreset R ((t ′ i , Q t ′ i )) for all s ∈ N , since P s ≤ P ′ . So, (N, P ′ ) = s∈N s ∩ (N, P ′ ) ⊆ s∈N s ∩ Unreset R ((t ′ i , Q t ′ i )).
By Lemma 3.14, there exists P ≤ S such that (r

′ , P ) = r ∩ shrink((N, P ′ )) ⊆ s∈N s ∩ Unreset R ((t ′ i , Q t ′ i )).
This proves the first direction of the lemma. Consider any SMs {Q ti } 1≤i≤m such that (Q ti ) x,y ≥ 1 and (S t ) x,y = 0 for some i and x, y ∈ C 0 . Then there exists r 0 ∈ N with r 0

[R ← 0] = t, such that if Q r0 denotes the SM that satisfies (r ′ 0 , Q r0 ) = r 0 ∩ Unreset R ((t ′ i , Q ti )
) with r ′ 0 = r 0 and r 0 ⊆ r ′ 0 , we have Q r0 ≤ S r0 . So, there is no SM P r0 such that r 0 ∩ (N, P r0 ) ⊆ (r ′ 0 , Q r0 ) and P r0 ≤ S ′ . It follows that there is no

P ′ ≤ S ′ satisfying (N, P ′ ) ⊆ s∈N (s ′ , Q s ) where (s ′ , Q s ) = s ∩ Unreset R ((t, Q t )).
In fact, if this would imply that (N, P ′ ) ∩ r 0 ⊆ (r ′ 0 , Q r0 ), since the regions in N are pairwise disjoint. Therefore, if (N, P ′ ) satisfies the above inclusion, then P ′ ≤ S ′ , so there is no P ≤ S such that (r ′ , P ) satisfies the statement of the lemma for some r ′ = r. This lemma gives for instance the shrinking constraints that should be satisfied in r 1 , r 2 and r 3 , in Fig. 5, once shrinking constraint in r ′ 0 is known. In this case, the constraint in r ′ 0 is 0 everywhere since it is a punctual region. The neighborhood N of r ′ 0 is composed of r ′ 0 and two extra regions (defined by (0 < x < 1) ∧ (x = y) and (1 < x < 2) ∧ (x = y)). If there are shrinkings of regions r 1 , r 2 , r 3 satisfying the corresponding shrinking constraints (given in the lemma), and from which Controller wins, then one can derive a shrinking of r ′ 0 , satisfying its constraint, and from which Controller wins. In the next section, we define the game RG(A) following this idea, and explain how it captures the game semantics for robustness.

A finite game abstraction

Let A = (L, C, ℓ 0 , E) be a timed automaton. We define a finite turn-based game RG(A) on a graph whose nodes are of two sorts: square nodes labelled by (ℓ, r, S r ), where ℓ is a location, r a region, S r is a well shrinking constraint for r; diamond nodes labelled similarly by (ℓ, r, S r , e) where moreover e is an edge leaving ℓ. Square nodes belong to Controller, while diamond nodes belong to Perturbator. Transitions are defined as follows:

(a) From each square node (ℓ, r, S r ), for any edge e = (ℓ, g, R, ℓ ′ ) of A, there is a transition to the diamond node (ℓ, s, S s , e) if the following conditions hold:

(i) r ⋖ * s and s ⊆ g;

(ii) S s is such that for all SMs Q, Q ≤ S s iff there exists P ≤ S r with (r ′ , P ) = r ∩ shrink + (Pre time ((s, Q))),

for some r ′ = r.

(b) From each diamond node (ℓ, r, S r , e), where e = (ℓ, g, R, ℓ ′ ) is an edge of A, writing N for the set of regions in the neighborhood of (r, S r ) and

N ′ = {s[R ← 0] | s ∈ N },
(s ∩ Unreset R ((t ′ , Q t ))), where t = s[R ← 0],
for some r ′ = r.

Intuitively, the transitions from the square nodes are the decisions of Controller. In fact, it has to select a delay and a transition whose guard is satisfied. Then Perturbator can choose any region in the neighborhood of the current region, and, after reset, this determines the next state. Note that RG(A) can be computed, thanks to Lemmas 3.16 and 3.17, and has exponential-size. Observe also that RG(A) is constructed in a forward manner: we start by the initial constrained region (i.e. the region of valuation 0 with the zero matrix as shrinking constraint), and compute its successors in RG(A). Then, if Controller has a winning strategy in RG(A), we construct a winning strategy for G δ (A) by a backward traversal of RG(A), using Lemmas 3.16 and 3.17. Thus, we construct RG(A) by propagating shrinking constraints forward, but later do a backward traversal in it. The correctness of the construction is stated as follows.

Proposition 4.1. For any timed automaton A, Controller has a winning strategy in RG(A) if, and only if there exists δ 0 > 0 such that Controller wins G δ (A) for all δ ∈ [0, δ 0 ].

Note that as we compute a winning strategy for Controller (if any) by Proposition 4.1, we can also compute a corresponding δ 0 . The upper bound of Theorem 2.3 is a consequence of the above proposition, since RG(A) has exponential size and finite reachability games can be solved in time polynomial in the size of the game.

Changing the perturbation parameters.. Consider the semantics where Controller's delays are bounded below by kδ, and the perturbations belong to [lδ, mδ] with lδ + kδ ≥ 0, for some rational number δ > 0 and integers k ≥ 0, l, m (Observe that any choice of these rational parameters can be written in this manner). The abstract game construction can then be adapted to this case. In fact, it suffices to replace the operator shrink + by shrink [0,kδ] , and the operator shrink by shrink [lδ,mδ] in the construction. Assume we are given a reachability objective defined by ℓ ⌣ ∈ L, and let σ be a memoryless winning strategy for Controller in RG(A) for reaching ℓ ⌣. Consider the execution tree T σ of RG(A), where Controller plays with σ. T σ is finite by Koenig's Lemma since all branches are winning, thus finite, and all branches end in the target state.

To any square node n of T σ labelled by (ℓ, r, S r ), we will assign a shrunk DBM r ′ , P n and δ n > 0 with P n ≤ S r and r = r ′ , such that Controller wins the game G δ (A) from any state of {ℓ} × (r ′ -δP n ) for all δ ∈ [0, δ n ]. Remember that r ′ = r implies r ⊆ r ′ since r is a region. We will define these by a bottom-up traversal of T σ . We start by assigning P n = 0 and δ n = ∞ to all nodes with loc(n) = ℓ ⌣ (which are leaves of T σ ). These are trivially winning for Controller.

Consider now a square node n of T σ labelled by (ℓ, r, S r ) whose all square successors have been treated. Then, n has only one successor which is given by σ, we assume it is the diamond node n ′ labelled by (ℓ, s, S s , e). We write e = (ℓ, g, R, ℓ ′ ). Let N be the set of neighboring regions of s, S s given by Lemma 3.14. Let s 1 , . . . , s m be the regions composing N , and let n ′ 1 , . . . , n ′ m denote the successors of n ′ in T σ , where n ′ i is labelled by (ℓ ′ , t i , S ti ), and such that t i = s i [R ← 0]. By construction, shrinking constraints S ti are given by Lemma 3.17 applied to s, S s . By induction, for each 1 ≤ i ≤ m there is a shrunk DBM (t ′ i , P n ′ i ) and

δ n ′ i > 0 with t ′ i = t i and P n ′ i ≤ S ti , such that Controller wins the game G δ (A) from {ℓ ′ } × (t ′ i -δP n ′ i ) for all δ ≤ δ n ′ i
. Now, by Lemma 3.17, there exists a shrunk DBM (s ′ , Q) with s ′ = s and Q ≤ S s such that

s ′ -δQ ⊆ s ∩ shrink( 1≤i≤m s i ∩ Unreset R (t ′ i -δP n ′ i )),
for all 0 ≤ δ ≤ δ n ′ , where δ n ′ ≤ min i (δ ti ) is computed by Lemma 3.8. Then, by construction of the game, there exists P n ≤ S r and 0 < δ n ≤ δ n ′ such that r ′ -δP n = r ∩ shrink + (Pre time (s ′ -δQ)) for all 0 ≤ δ ≤ δ n , for some r ′ = r (Remember that Lemma 3.16 applies here on s ′ since s = s ′ and s ⊆ s ′ ). Here, δ n can be computed using Lemma 3.6. Controller wins from these states: in fact, it can delay into s ′ -δQ, where, after any Perturbator's move, and the clock resets, the next state belongs to one of the states t ′ i -δP n ′ i , which are all winning by induction. Notice that at each step of the computation, we get non-empty shrunk DBMs satisfying the corresponding shrinking constraints. By construction of RG(A), we have only well shrinking constraints in all nodes, so the computed shrunk DBMs (r ′ , P n ) are always non-empty. The procedure ends in the initial state (ℓ 0 , 0, 0), so Controller wins G δ (A) by projecting the play to RG(A) and always staying inside set r ′ -δP n at any node n, which is possible by construction.

Upper bound on δ 0 .

We now assume that Controller has a winning strategy and give an upper bound on δ 0 computed by the algorithm. Consider the set M of all shrunk DBMs that appear when we construct the winning strategy in the proof above, including the shrunk DBMs corresponding to intermediary results. For instance, in the computation above, given the edge (ℓ i , r i , S ri ) → (ℓ i , r ′ i , S r ′ i , e) and P r ′ i , we compute P ri such that (r i , P ri ) = r ∩ shrink + (Pre time (r ′ i , P r ′ i ) ). Then, M contains the shrunk DBMs (r i , P ri ) and (r ′ i , P

r ′ i ), but also (M 1 , Q 1 ) such that (M 1 , Q 1 ) = Pre time ((r i , P ri )), and (M 2 , Q 2 ) such that (M 2 , Q 2 ) = shrink + ((M 1 , Q 1 )
). Now, δ 0 is chosen by the algorithm small enough so that all shrunk DBMs of M are non-empty and normalized, and all such equations that appear in the construction of a winning strategy above hold, for all δ ∈ [0, δ 0 ). Note that since RG(A) has exponential size, M may contain exponentially many shrunk DBMs. We show that δ 0 can be chosen, roughly, as the inverse of the maximal component of all shrinking matrices that appear in all computations. Proposition 4.2. Let m = max (M,P )∈M max i,j∈C0 P i,j . Then, one can choose δ 0 = 1 3m . Proof. To prove this, we need to show for all δ ∈ [0, δ 0 ) that all shrunk DBMs of M are normalized, non-empty and satisfy the equations they are involved in. Let us first note that being normalized implies non-emptiness for the shrunk DBMs of M since all shrinking constraints are well. In fact, a normalized DBM is non-empty if, and only if all its diagonals are 0. Here, for any (M, P ) ∈ M, the diagonal components of M and P must be 0 since M is non-empty and normalized, and M -δP is non-empty and normalized for small enough δ > 0, by hypothesis. Hence, if M -δP is normalized, it must be non-empty too. Let (M, P ) ∈ M. Normalization condition requires

∀i, j, k ∈ C 3 0 , M i,j -δP i,j ≤ M i,k -δP i,k + M k,j -δP k,j , for all δ ∈ [0, δ 0 ). If M i,j = M i,k + M k,j
, then we must have P i,j ≥ P i,k + P k,j since the above condition holds for small enough δ > 0. But then, for these components, the condition holds for all

δ > 0. If M i,j < M i,k + M k,j , then the condition holds if δ 0 ≤ | M i,k +M k,j -Mi,j P i,k +P k,j -Pi,j
|, but this is already the case since δ 0 < 1 3m . It remains to show that all equations that appear in the computations hold. Equations of the form (M, P ) = Pre time ((N, Q)) and (M, P ) = Unreset R ((N, Q)) already hold for δ ∈ [0, δ 0 ) since all involved shrunk DBMs are normalized (see Lemma 3.6 and [36] for details). For an equation of the form (M, P ) = (N 1 , Q 1 ) ∩ (N 2 , Q 2 ), we have either (N 1 ) i,j = (N 2 ) i,j and P i,j = max((Q 1 ) i,j , (Q 2 ) i,j ), or for example (N 1 ) i,j < (N 2 ) i,j and (M i,j , P i,j ) = ((N 1 ) i,j , (Q 1 ) i,j ). In the former case, the equation holds for all δ > 0. In the latter case, it holds for all δ < | (N2)i,j -(N1)i,j (P2)i,j -(P1)i,j |. This is already the case since δ < 1 3m .

The following lemma shows that ǫ-tightness is preserved by resets.

Lemma 4.5. Let r, r ′ be regions such that r ′ = r[R ← 0] for some R ⊆ C. Consider shrinking constraints S r and S r ′ given by Lemma 3.12, such that for any SM Q, Q ≤ S r ′ iff there the SM P such that (r, P ) = r ∩ Unreset R ((r ′ , Q)) satisfies P ≤ S r . Let δ > 0 small enough so that these equations hold for given P and Q. For any ǫ > 0, and any ν that is ǫ-tight in r -δP w.r.t. S r , we have that

ν ′ = ν[R ← 0] is ǫ-tight in r ′ -δQ w.r.t. S r ′ .
Proof. Let N = Unreset R (r ′ ) and S N be the shrinking constraints such that for any SM Q, Q ≤ S N if and only if the SM P such that r -δP = r ∩ (N -δQ) satisfies P ≤ S r . Then S r ′ is such that for any SM Q, Q ≤ S r ′ if and only if there the SM P such that N -δP = Unreset R (r ′ -δQ) satisfies P ≤ S N . By definition of the reset operation, we have r ′ x,y = r x,y for all x, y ∈ R, and r ′ x,y = 0 for all x, y ∈ R (we assume 0 ∈ R). For any x ∈ R and y ∈ R, r ′

x,y = r 0,y and r ′ y,x = r y,0 . It suffices to assume that ν is ǫ-tight in r, S r and show that ν ′ = ν[R ← 0] is ǫ-tight in r ′ , S r ′ . For all x, y ∈ R or x, y ∈ R, it is clear that ν ′ satisfies the ǫ-tightness for these components. Consider x ∈ R and y ∈ R such that (S r ′ ) x,y = 0. Then (S r ′ ) 0,y = 0, and it suffices to show that -ν ′ (y) ≥ r ′ 0,yǫ since ν ′ (x) = 0 and r 0,y = r ′ 0,y . We are going to show that (S r ) 0,y = 0. If S ′ N denotes the shrinking constraint defined by (S ′ N ) x,0 = (S ′ N ) 0,x = 0 for all x ∈ R, (S ′ N ) x,y = ∞ whenever x ∈ R and y ∈ C or inversely, and (S ′ N ) x,y = (S N ) x,y for x, y ∈ C 0 \ R. Then S r ′ is the normalization of S ′ N . Then, (S r ′ ) 0,y = 0, for y ∈ R, means that there is z, z ′ ∈ C 0 such that for some path π ∈ Π z,z ′ (G(r ′ )), (0, y) belongs to π and (S ′ N ) z,z ′ = 0. Then either z, z ′ ∈ R and (S N ) z,z ′ = 0, or z = 0 and z ′ ∈ R.

• Consider the first case. We have r ′ z,z ′ = N z,z ′ (by definition of unreset). We show that there is a path π ′ ∈ Π z,z ′ (G(N )) that contains (0, y) and whose all nodes are outside R. In fact, r ′ z,0 = N z,0 and r ′ y,z ′ = N y,z ′ since z, z ′ , y ∈ R, and these have finite weights (since π is a shortest path). But N is obtained from r ′ by setting to ∞ edges with an endpoint in R, and applying normalization. So there must be shortest paths from z to 0, and from y to z ′ in G(N ). Now, since (S N ) z,z ′ = 0, (z, z ′ ) belongs to some path π ′′ ∈ Π α,β (G(N )) where r αβ = N α,β and (S r ) α,β = 0. Moreover, from r ⊆ N , r α,β = N α,β and r z,z ′ = N z,z ′ , it follows that π ′ , π ′′ ∈ Π z,z ′ (G(N )) ⊆ Π z,z ′ (G(r)). Then, replacing the edge (z, z ′ ) in π ′′ by the path π ′ , we still get a shortest path in G(r), that contains (0, y). Therefore, we must have (S r ) 0,y = 0.

• Assume now that z = 0 and z ′ ∈ R. Assume that π does not contain nodes in R other than z ′ (if it does, we can shorten π and change z ′ ). Let us write π = z 1 z 2 . . . z m where z 1 = z and z m = z ′ . Since r ′ 0,zm = r ′ zm,0 = 0, π ′ = z 1 . . . z m-1 is a cycle with weight 0. But since all nodes in π ′ are outside R, this is also a path in G(r). Therefore (S r ) zi,zi+1 = 0 along all edges, and in particular (S r ) 0,y = 0.

By hypothesis, we have -ν(y) ≥ r 0,yǫ, and since r ′ 0,y = r 0,y , we get -ν ′ (y) ≥ r ′ 0,yǫ. The proof of the symmetric case x ∈ R and y ∈ R is similar.

The next lemma is the main lemma of the proof of the second direction of the theorem. It shows that, starting from an ǫ-tight valuation of r, S , and given a Controller's move, Perturbator can, not only choose any successor available in RG(A) but also make sure that the resulting valuation is (ǫ + ǫ ′ )-tight, for arbitrary ǫ ′ > 0.

Lemma 4.6. Consider a valuation ν that is ǫ-tight in r w.r.t. S. Let ν ′ = (ν + d) for some d ≥ δ, let e = (ℓ, g, R, ℓ ′ ) an edge of A with ν ′ |= g. Consider the edge of RG(A) from (ℓ, r, S r ) to (ℓ, r ′ , S r ′ , e) for r ′ = reg(ν ′ ) and for some S r ′ , from Lemma 4.4. Then, for any region s in the N, S N = neighbor r ′ , S r ′ , and any ǫ ′ > 0, there exists

d ′ ∈ [d -δ, d + δ] such that ν + d ′ is (ǫ + ǫ ′ )-tight in s w.r.t. S s
where S s is such that for all SMs Q, Q ≤ S s if, and only if there is P ≤ S N with (N, P ) ∩ s ⊆ (s, Q).

Before proving Lemma 4.6, let us first prove the second direction of Proposition 4.1.

Proof of Proposition 4.1 (Second direction). We fix δ > 0, and consider an arbitrary strategy σ for Controller in G δ (A). We are going to define an infinite play π, where Controller follows strategy σ, and the target location is not reached. This proves that Perturbator wins G δ (A) against any strategy of Controller since σ is chosen arbitrarily.

By hypothesis, Perturbator has a winning strategy γ in RG(A). We fix ǫ ∈ [0, δ/2], and we define the sequence ǫ i = 1≤j≤i ǫ 2 j for i ≥ 1, which is positive and bounded above by ǫ. We construct in parallel a play (ℓ i , r i , S ri ), (ℓ i , r ′ i , S r ′ i , e i ) i≥1 of RG(A) where Perturbator plays with strategy γ. The play π = (ℓ i , ν i ) i≥1 will satisfy the following invariant: For each state (ℓ i , ν i ), we have ν i ∈ r i and ν i is ǫ i -tight in r i w.r.t. S ri .

Initially, we have (ℓ 1 , ν 1 ) with ν 1 = 0, and the initial state (ℓ 1 , 0, 0) of RG(A) satisfies the invariant. For i ≥ 2, let us assume that state (ℓ i , ν i ) of the play satisfies the invariant for the state (ℓ i , r i , S ri ) of RG(A). Let d ≥ δ be the delay and e i = (ℓ i , g i , R i , ℓ i+1 ) the edge prescribed by σ from state (ℓ i , ν i ) given the current history. Let ν ′ i = ν i + d and r ′ i be the region of ν ′ i . Lemma 4.4 shows that RG(A) has the corresponding edge. Let (ℓ i+1 , r i+1 , S ri+1 ) be the successor of (ℓ i , r ′ i , S r ′ i , e i ) in RG(A), given by γ. Let s be a region in N = neighbor r ′ i , S ′ such that s[R ← 0] = r i+1 . From Lemmas 4.6 and 4.5, it follows that first s, then r i+1 are reachable from ν ′ i by Perturbator's move, and that the resulting valuation is ǫ i+1 -tight in r i+1 w.r.t. S ri+1 by choosing ǫ ′ = ǫ/2 i+1 Proof of Prop. 4.6. Consider such valuations ν ∈ r and ν ′ ∈ r ′ . For any x, y ∈ C, (S r ′ ) x,y = 0 implies that r ′

x,yǫ ≤ ν ′ (x)ν ′ (y) ≤ r ′ x,y , since S r and S r ′ have the same diagonal components and time delays do not change the quantities ν(x)ν(y). Hence, ν ′ is ǫ-tight in r ′ w.r.t. S r ′ for all diagonal components. Assume that r ′ ⋖ * s. The other case is similar. Let S s be the shrinking constraint such that for all SMs Q, Q ≤ S s if and only if there is P ≤ S N with (N, P ) ∩ s ⊆ (s, Q). Let us write the clocks ordered according to their fractional values in r ′ :

0 = frac(X 1 ) < frac(X 2 ) < . . . < frac(X m ) < 1,
where each X i is a set of clocks having the same fractional value, and X 1 can be empty.

1. Assume that (S r ′ ) x,0 = ∞ for all x ∈ X 2 ∪ . . . ∪ X m .
Then, by definition of the neighborhood, either r ′ = s or r ′ ⋖ s, where the latter case is possible if X 1 = ∅.

• If r ′ = s, then Perturbator perturbs by 0. Since (S s ) x,0 = ∞ and (S s ) x,y = (S r ′ ) x,y for all x, y ∈ C, by Lemma 4.7 (below), the valuation ν ′ is ǫ-tight (s, S s ) for these components. If (S s ) 0,x = 0 for some x ∈ C, then N 0,x < r ′ 0,x by Lemma 4.7 since s 0,x = r 0,x , so we must have (S r ′ ) 0,x = 0, and ν ′ is also ǫ-tight for components (0, x). Note that the ǫ-tightness of diagonal components follow from the ǫ-tightness of ν in r ′ w.r.t. S r ′ .

• If r ′ ⋖ s, we let Perturbator perturb by a positive amount 0 < d ′ < ǫ ′ , so that the valuation is in s. Since (S s ) x,0 = ∞ and (S s ) x,y = (S r ′ ) x,y for all x, y ∈ C, by Lemma 4.7, for these components, ν ′ + d ′ is ǫ-tight in (s, S s ). If (S s ) 0,x = 0 for some x ∈ C, then N 0,x < r ′ 0,x by Lemma 4.7, so we must have (S r ′ ) 0,x = 0. We have, by hypothesis,

-ν ′ (x) ≥ r ′ 0,x = s 0,x -ǫ, so -(ν ′ (x) + d ′ ) ≥ s 0,x -ǫ -ǫ ′ . ν ′ + d ′ is also ǫ-tight for diagonal components since ν ′ is.
2. Otherwise, consider the minimum k ∈ {2, . . . , m} such that (S r ′ ) x,0 = 0 for all x ∈ X k ∪. . .∪X m .

Since s is a successor region of r ′ , there exists k ′ ∈ {k, . . . , m} such that either clocks in X k ′ are integers, or all clocks X k ′ +1 ∪ . . . ∪ X m have changed their integer parts and only these. We treat each case separately:

(a) Assume s x,0 = r ′ x,0 , ≺ s x,0 =≤ for x ∈ X k ′ ; s x,0 = r ′ x,0 + 1 and ≺ s x,0 =< for all x ∈ X k ′ +1 ∪ . . . ∪ X m ; s x,0 = r ′ x,0 for all x ∈ X 1 ∪ . . . ∪ X k ′ -1 .
We define Perturbator's move as

d ′ = 1 -frac(ν ′ i (x)) for x ∈ X k ′ . It is clear that ν ′ + d ′ ∈ s, and that d ′ ≤ ǫ since ν ′ is ǫ-tight.
Let us show that the ν ′ + d ′ is ǫ-tight in s w.r.t. S s . By Lemma 4.7, all diagonal constraints in S s are the same as in S r ′ so the property is satisfied for these components.

-Let us show ǫ-tightness for components (x, 0) (upper bounds). For all x ∈ X k ′ +1 ∪ . . . X m , we have (S s ) x,0 = ∞ by Lemma 4.7, since s x,0 = r ′

x,0 + 1 = N x,0 . We have

(ν ′ + d ′ )(x) = s x,0 = -s 0,x for x ∈ X k ′ , so ν ′ + d ′ is ǫ-tight for component (x, 0). For all x ∈ X k ∪ . . . ∪ X k ′ -1 , we have s x,0 = r ′
x,0 , and ν ′ (x) ≥ r ′ x,0ǫ, which implies ν ′ (x) + d ′ ≥ s x,0ǫ as required. For all x ∈ X 1 ∪ . . . ∪ X k-1 , we have (S s ) x,0 = ∞. In fact, (S s ) x,0 = 0 means, by Lemma 4.7 that s x,0 < N x,0 . But since r ′ ⋖ * s, we would have r ′ ≤ s x,0 < N x,0 , and this implies that (S r ′ ) x,0 = 0 by definition of N and Lemma 4.7. But by the choice of k, and by Proposition 3.15, this is a contradiction.

-We now show ǫ-tightness for components (0, x) (lower bounds). For all x ∈ X k ′ +1 ∪ . . . ∪ X m , we have, -(ν ′ (x) + d) ≥ s 0,xǫ since d ′ ≤ ǫ. The property is again clearly satisfied by ν ′ (x) + d ′ for x ∈ X k ′ since ν ′ (x) + d ′ = s x,0 . Consider now x ∈ X 1 ∪ . . . ∪ X k ′ -1 such that (S s ) 0,x = 0. We have (S s ) 0,y = 0 for y ∈ X k ′ , and (S s ) 0,x = 0, which implies that (S s ) y,x = 0 since paths 0, y, x and 0, x belong to G(s), and S s is normalized. Then, we also have (S r ′ ) y,x = 0, so ν ′ (y)ν ′ (x) ≥ s y,xǫ. means that frac(ν ′ (x)) + d ′ ≤ ǫ. The following figure illustrates this, assuming x ∈ X i .

0 < X 1 < . . . < X i frac(ν ′ (x)) < X i+1 < . . . < X k ′ ≥1-ǫ < . . . < 1 =d ′ Therefore ν ′ + d ′ satisfies ν ′ (x) + d ′ ≤ -s 0,x + ǫ, for all x ∈ C such that (S s ) 0,x = 0. (b) s x,0 = r ′ x,0 + 1 and ≺ s x,0 =< for all x ∈ X k ′ ∪ . . . ∪ X m ; s x,0 = r ′ x,0 and ≺ s x,0 =< for all x ∈ X 1 ∪ . . . ∪ X k ′ -1 .
In this case, we first delay to the immediate time predecessor of s as in the previous case, then add a positive delay d ′ of at most ǫ ′ . Then,

ν ′ + d ′ is (ǫ + ǫ ′ )-tight in s w.r.t. S s .
The following technical lemma is used in the proof of Lemma 4.6 above. Lemma 4.7. Let N, S N denote the constrained neighborhood of some constrained region. Let r be any region included in N . Let S r denote the shrinking constraint such that for all SMs Q, Q ≤ S r if, and only if there is P ≤ S N with (N, P ) ∩ r ⊆ (r, Q) for all small δ > 0. Then, for all x, y ∈ C, (S r ) x,y = 0 implies that (S N ) x,y = 0; for all x ∈ C, (S r ) x,0 = 0 implies r x,0 < N x,0 and (S r ) 0,x = 0 implies r 0,x < N 0,x . Proof. By Lemma 3.12, S r is defined as follows. Let S 1 obtained by (S 1 ) x,y = S x,y if r x,y = N x,y and 0 otherwise. Then, S r is the normalization (in the sense of SMs) of S 1 , so S 1 ≤ S r . But all diagonal constraints are the same in r and N , and r x,0 = N x,0 implies (S 1 ) 0,x = S x,0 = ∞, and similarly r 0,x = N 0,x implies (S 1 ) 0,x = S 0,x = ∞. The result follows.

We also note the following corollary of Lemma 4.6 and Lemma 4.5, which will be used in Section 5.

Corollary 4.8. Let (ℓ, r, S r ) be a square node of RG(A). Then r, S r admits tight valuations.

Proof. We prove this for each node n = (ℓ, r, S r ) by induction on the shortest path from the initial node of RG(A) to n. It is true for the initial node (ℓ 0 , 0, 0). Assume it is the case for n = (ℓ, r, S r ), and pick any square node n ′′ = (ℓ ′ , t, S t ) reached via a diamond node n ′ = (ℓ, s, S s , e). For all successor (ℓ ′ , t ′ , S t ′ ) of n ′ , pick any SM Q t ′ ≤ S t ′ , and consider P ′ ≤ S s given by Lemma 3.17 such that (s, P ′ ) ⊆ s ∩ shrink(

s ′ ∈N (s ′ ∩ Unreset R ((t ′ , Q t ′ )))),
where N is the neighborhood of s, S s , and we write t ′ = s ′ [R ← 0] for any s ′ ∈ N . Further, let P r ≤ S r such that (r ′ , P r ) = r ∩ shrink + (Pre time ((s, P ′ ))).

Choose δ > 0 small enough so that all equations hold. Let ν be any ǫ-tight valuation in r ′ -δP . By the above equations, by a joint move of Controller and Perturbator, the game can proceed to any of the set t ′ -δQ t ′ . In particular, by Lemmas 4.6 and 4.5, the resulting valuation can be chosen by Perturbator to be inside t -δQ t as (ǫ + ǫ ′ )-tight for any ǫ ′ > 0. Since Q t was chosen arbitrarily, t, S t admits tight valuations.

Extension to Turn-based Timed Games

In this section, we extend the reachability algorithm to turn-based timed games. The correctness of the abstract game for timed automata (Proposition 4.1) was based on 1) the ability of the controller to always delay inside shrinkings of regions it visits, 2) while not being able to avoid visiting tight valuations. While the former ensured Controller to win G δ (A) if a winning strategy of the abstract game is given, the latter ensured the symmetric property for Perturbator.

The situation is different in a game setting since from locations L P , Perturbator has no reason to delay into particular shrinkings. In fact, consider Figure 10 which shows the states that can be reached by a delay inside region r ′ , at a location L P , starting from a shrinking of r, with r ⋖ + r ′ . Perturbator can thus delay to valuations close to borders. In fact, if the play arrives to L P inside r -δP , then r ′ ∩ Post time (r -δP ) is the set of valuations that that can be reached inside r ′ after a delay. While this can still be expressed as a shrunk region (by Lemma 3.6), this set does not admit tight valuations, so the previous proof cannot be carried out directly. We will show however that this set is always included in the union of at most two shrunk regions that admit tight valuations (See Fig. 10(b)). This property will allow us to adapt the abstract game construction and prove its correctness following the same proof as for timed automata.

⊆ (b)

The shrinking of r ′ on the left can be decomposed as two shrinkings that admit tight valuations. Any actual delay of Perturbator will belong to one of these two shrinkings.

Figure 10: At Perturbator's locations, the delays cannot be expected to end in shrinkings of a particular form. In this example, if Perturbator delays in region r ′ from r, the valuation can be closed to the borders of the region, and the shrinking expressing the reachable valuations do not admit tight valuations (on the left). We will rather decompose this shrunk region into two shrunk regions that do admit tight valuations (on the right).

For the proofs, we first need the following characterization of constrained regions that admit tight valuations. Intuitively, a constrained region does not admit tight valuations 1) if we have S x,y = S y,x = 0 for some pair x, y ∈ C 0 with r x,y = -r y,x since this would require a valuation v to be close to two distant lines, and 2) if the zeros of S are "transitive". The characterization is formally proved in the next lemma.

Lemma 5.1. Let r, S r be a constrained region. Then, r, S r admits tight valuations if, and only if the two following conditions hold:

1. For any x, y ∈ C 0 , if r x,y = -r y,x and (S r ) x,y = 0, then (S r ) y,x = ∞, 2. For any x, y ∈ C 0 , if there is x 1 x 2 . . . x n ∈ Π x,y (G(r)) with (S r ) xi,xi+1 = 0 for 1 ≤ i ≤ n -1, then (S r ) x,y = 0.

Proof. Assume that the first condition is not satisfied. If r x,y = -r x,y and (S r ) x,y = (S r ) y,x = 0, then for any ν ∈ r, ν(x)ν(y) > r x,yǫ implies ν(x)ν(y) > -r x,y + ǫ, for small enough ǫ > 0. So no valuation ν is tight in r. Assume now that the second condition is not satisfied. Consider the fractional ordering of the clocks in r: X 1 , . . . , X n and let 2 ≤ i 0 ≤ n + 1 and 1 ≤ j 0 ≤ n be the indices given by Lemma 3.15. By hypothesis, we must have j 0 < i 0 , since otherwise j 0 ≥ 2, and r x,0 = -r 0,x for x ∈ X j0 , but (S r ) x,0 = (S r ) 0,x = 0, contradicting the hypothesis.

Observe that if x ∈ X k and y ∈ X l with j 0 < k < l < i 0 , then (S r ) y,x = ∞, since (y, 0, x) ∈ Π y,x (G(r)) and (S r ) y,0 = ∞. Furthermore, unless i 0 = j 0 + 1, there exists

j 0 + 1 = α 1 ≤ α ′ 1 < α 2 ≤ α ′ 2 < . . . < α m ≤ α ′ m = i 0 -1, such that for all x ∈ X k and y ∈ X l with α i ≤ k < l ≤ α ′
i , we have (S r ) x,y = 0, and if α i ≤ k ≤ α ′ i and l > α ′ i then (S r ) x,y = ∞. In fact, for any pair x ∈ X k and y ∈ X l with j 0 < k < l < i 0 , (S r ) y,x = ∞ because (S r ) y,0 = ∞. We have -r y,x + δP y,x < ν(x)ν(y) < r x,y -δP x,y by 1 |C|+2 + ǫ > δ max x,y P x,y .

We need to extend Lemma 3.12 to the Post time () operation. Proof. Recall that N is obtained from M by setting all components (x, 0) to (∞, <) and that the resulting DBM is already normalized. Define (S 1 ) x,0 = ∞ for all x ∈ C and (S 1 ) x,y = S x,y for all (x, y) ∈ C 0 × C. We define S ′ as the normalization of S 1 .

For any P ≤ S, let (N, Q) denote the shrunk DBM such that (N, Q) = Post time ((M, P )). Let us show that Q ≤ S ′ . Here, Q is the normalization of Q ′ defined by Q ′

x,y = P x,y if y = 0 and Q ′ x,y = 0 if y = 0. Since N x,0 = ∞ for all x ∈ C, we only need to verify that Q ′

x,y ≤ S ′ x,y when y = 0. For these components, we have N x,y = M x,y and M ⊆ N , therefore Π x,y (G(N )) ⊆ Π x,y (G(M )). So Q ′ is already normalized because P is, and Q = Q ′ . By definition of S 1 above, we have Q ≤ S 1 , which implies Q ≤ S ′ (since Q is normalized). This also shows that if Q ≤ S ′ , then for all P ≤ S, we have Post time (M -δP ) ⊆ N -δQ. In fact, for any such P , as we just showed, there exists

Q ′ ≤ S ′ such that Post time (M -δP ) = N -δQ ′ . But N -δQ ′ ⊆ N -δQ if, and only if Q ≤ Q ′ , and Q ′ ≤ S ′ implies Q ≤ S.
For any Q ≤ S ′ , let us define P such that (M,

P ) = M ∩ (N, Q). We have Post time ((M, P )) = (N, Q), since Post time (M ∩ (N, Q)) = (N, Q).
Let us show that P ≤ S. P is the normalization of P ′ defined by P ′

x,y = Q x,y if y = 0 and P ′ x,y = 0 otherwise. Consider (x, y) such that S x,y = 0. -If y = 0, then S ′

x,y = 0, by definition of S ′ . Consider any path x 1 . . . x n in Π x,y (G(M )). We have S xj ,xj+1 = 0 for all 1 ≤ j ≤ n -1. But, if x j+1 = 0, then P ′ xj ,xj+1 = 0 by definition, and otherwise P ′ xj ,xj+1 = 0 because S ′ xj ,xj+1 ≤ S xj ,xj+1 = 0. Therefore, P x,y ≤ S x,y . -For the case y = 0, one can notice that since N x,0 = ∞ for all x ∈ C, for all normalized SMs P , we have P x,0 = 0 by definition.

The following lemma gives the construction illustrated in Fig. 10. The idea is the following. We know that a time successor region of a constrained region admitting tight valuations does not admit tight valuations in general (see Fig. 10). Nevertheless, we show, in the following lemma, that such a time successor can be over-approximated by the union of at most two constrained regions admitting tight valuations (see the two regions on the right, in Fig. 10). This property will allow us to carry out the same proof as in the previous section, based on tight valuations. The idea of the proof consists in showing that, given r, S r and a successor region r ′ , the time successor valuations of r that are in r ′ are either close to the first facet of r ′ they cross when entering r ′ , or to the last facet they cross before leaving r ′ . These facets can be defined looking at the order in which the fractional values of the clocks evolve during a delay, as in the figures below. Lemma 5.3. Let r, S r be any constrained region that admits tight valuations, and r ′ such that r ⋖ * r ′ . There exist, and one can compute, S 1 , S m with m ∈ {1, 2}, such that each r ′ , S i admits tight valuations and for any SMs (Q i ) 1≤i≤m , we have Q i ≤ S i for all 1 ≤ i ≤ m, if, and only if (a) Assume that for all x ∈ X 1 ∪. . . X n , -r ′ 0,x +δQ 1 0,x ≺ r ′ 0,x ν ′ (x). For all x ∈ X i0 ∪. . .∪X n and x ∈ X 1 ∪. . .∪X j0 , we have Q 1

x,0 = 0 so ν(x) ≺ r ′ x,0 r ′ x,0 -δQ 1 x,0 . For any x ∈ X α1 ∪. . . X i0-1 , we have P x,0 ≥ Q 1

x,0 , so ν ′ (x) ≺ r ′ x,0 r ′ x,0 -δQ 1 x,0 . (b) Assume that for some 1 ≤ i ≤ n, for clocks x ∈ X i , -r ′ 0,x + δQ 1 0,x ≺ r ′ 0,x ν ′ (x). We show that ν ′ ∈ r ′ -δQ 2 . Let us first show that we have i ∈ {α 1 , . . . , α ′ 1 }. This follows from the fact that P x,α1 ≥ Q 1 0,x for all clocks x ∈ C \ (X α1 ∪ . . . ∪ X α ′ 1 ). In fact, this ensures that the constraint -r ′ 0,x + δQ 1 0,x ≺ r ′ 0,x ν ′ (x) is always satisfied for these clocks, hence i ∈ {α 1 , . . . , α ′ 1 }. We first show that the upper bounds hold. Let y ∈ X α1 and y ′ ∈ X i . We have ν ′ (y) ≤ -r ′ 0,y +δQ 1 0,y ′ since ν ′ (y ′ ) ≤ -r ′ 0,y ′ +δQ 1 0,y ′ by definition of i, and frac(ν(y)) ≤ frac(ν(y ′ )). For any

x ∈ X i0 ∪ . . . ∪ X n ∪ X 1 ∪ . . . ∪ X j0 , we also have ν ′ (x) -ν ′ (y) ≺ r ′
x,y r ′ x,y -δP x,y , which together yields ν ′ (x) ≺ r ′

x,0 r ′ x,0δ(P x,y -Q 1 0,y ′ ). This implies the desired bound since P

x,y ≥ Q 2 x,0 + Q 1 0,y ′ . For any clock x ∈ X α1 ∪ . . . ∪ X i0-1 , we have P x,0 ≥ Q 2 x,0 , which yields ν ′ (x) ≺ r ′
x,0 -δQ 2 x,0 . It remains to show the lower bounds. We have

Q 2 0,x = 0 for all x ∈ X α1 ∪ . . . ∪ X α ′ 1 so -r ′ 0,x + δQ 2 0,x ≺ r ′ 0,x ν ′ (x). For all x ∈ C \ (X α1 ∪ . . . ∪ X α ′ 1 )
, we have by definition

P α1,x ≥ Q 2 0,x . Then, -r ′ α1,x + δP α1,x ≺ r ′ α1,x ν ′ (x) -ν ′ (α 1 )
. Combining with the fact that ν ′ (α 1 ) ≥ -r ′ 0,α1 we get -r ′ 0,x + δQ 2 0,x ≺ r ′ 0,x ν ′ (x). It is now easy to see that from ǫ-tight valuations in (r, S r ), one can reach (ǫ + ǫ ′ )-tight valuations in both (r ′ , S 1 r ′ ) and (r, S 2 r ′ ). In fact, for any ǫ ′ > 0, the delay d ≥ 0 can be chosen such that r ′

x,0ν ′ (x) ≤ ǫ ′ , for x ∈ X j0 , but also such that ν ′ (x) + r ′ 0,x ≤ ǫ ′ for x ∈ X α1 . In the former case, ν ′ is (ǫ + ǫ ′ )-tight in (r ′ , S 1 r ′ ), and in the latter case, ν ′ is (ǫ + ǫ ′ )-tight in (r ′ , S 2 r ′ ). 3. The cases where α ′ i ≤ k 0 < α i+1 for i > 1 or α ′ m ≤ k 0 < i 0 are treated similarly to the previous case: Here α ′ i has the role of j 0 , and α i+1 has the role of α 1 . 4. Assume that α i ≤ k 0 < α ′ i . Then S r ′ has the same diagonal components as S r , and for any x ∈ X αi ∪ . . . ∪ X k0 , (S r ′ ) x,0 = 0 and (S r ′ ) 0,x = ∞, while for any x ∈ X k0+1 ∪ . . . ∪ X α ′ i , (S r ′ ) x,0 = ∞ and (S r ′ ) 0,x = 0. Furthermore, for any other clock x ∈ C, (S r ′ ) x,0 = (S r ′ ) 0,x = ∞.

If we fix SMs P and Q such that Post time (r -δP ) ∩ r ′ ⊆ r ′ -δQ, then for any ǫ-tight valuation ν ∈ r -δP , any delay d with ν + d ∈ r ′ is ǫ-tight in (r ′ , S r ′ ). In fact, the diagonal components stay unchanged during delays, and the fractional values of clocks X αi ∪ . . . ∪ X α ′ i differ by at most ǫ in ν.

Assume that j

0 + 1 = i 0 (there is no α i , α ′ i ).
Consider the case k 0 = j 0 . The proof follows again the same ideas as before, but is simpler. We give the details. We define (S 1 r ′ ) x,y = (S 2 r ′ ) x,y = (S r ) x,y for all x, y ∈ C. We let (S 1 r ′ ) x,0 = 0 and (S r ′ ) 0,x = ∞ for all x ∈ C, and (S 2 r ′ ) 0,x = ∞ and (S r ′ ) 0,x = 0 for all x ∈ C. S 1 r ′ is represented in Figure 11(a) (with the difference that there is no α i 's).

Let Q i ≤ S i r ′ for i = 1, 2. Let j ′ 0 = min{j | 1 ≤ j ≤ j 0 , X j = ∅}. Define P , where P x,y ≥ Q 1 0,x for all x ∈ X i0 ∪ . . . ∪ X n and y ∈ X j ′ 0 . Let P x,i0 ≥ Q 1 0,y + Q 2 x,0 for all x ∈ C \ X i0 and y ∈ C. Consider ν ∈ r -δP . Let ν ′ = ν + d such that ν ′ ∈ r ′ . If -r ′ 0,x + δ ≺ r ′ 0,x ν ′ (x) for all x ∈ C, then ν ′ ∈ r ′ -δQ 1 since (Q 1 )
x,0 = 0 and P x,y ≥ Q 1

x,y for all x, y ∈ C.

Otherwise, we have ν ′ (y ′ ) ≤ -r ′ 0,y ′ + δQ 1 0,y ′ for some y ′ ∈ C, so ν ′ (i 0 ) ≤ -r ′ 0,i0 + δQ 1 0,y ′ since frac(ν ′ (i 0 )) ≤ frac(ν ′ (y ′ )). This means that ν ′ (i 0 ) ≺ r ′ i0,0 r ′ i0,0 -δQ 2 x,0 for small enough δ > 0. For all x ∈ C \ X i0 , we have ν ′ (x)ν ′ (i 0 ) ≺ r ′

x,i0 r ′ x,i0 -δP x,i0 . This implies, by the above constraint on ν ′ (i 0 ) that ν ′ (x) ≺ r ′

x,0 r ′ x,0δ(P x,i0 + Q 1 0,y ′ ). This implies ν ′ (x) ≺ r ′ x,0 r ′ x,0 -δQ 2

x,0 since P x,i0 ≥ Q 1 0,y ′ + Q 2 x,0 . We are done since Q 2 0,x = 0 for all x ∈ C. It is clear that from ǫ-tight valuations in r -δP , one can delay to (ǫ + ǫ ′ )-tight valuations both in r ′ -δQ 1 and r ′ -δQ 2 , for any ǫ ′ > 0.

We can now generalize the abstract game to turn-based timed games, and prove the main theorem for these games.

Let us fix a timed game A = (L C ∪ L P , C, ℓ 0 , E). We define RG(A) as follows. The states of RG(A) is again given as a set of square nodes (ℓ, r, S r ), where ℓ ∈ L C and r, S r is a well constrained region. The diamond nodes are now either of the form (ℓ, r, S r , e) with ℓ ∈ L C and e is an edge leaving ℓ, or (ℓ, r, S r ) with ℓ ∈ L P . As before, square nodes belong to Controller, and diamond nodes belong to Perturbator. The edges leaving square nodes and the diamond nodes of the form (ℓ, r, S r , e) are defined as for timed automata. There is an edge from a diamond node (ℓ, r, S r ) to (ℓ ′ , t, S t ), if there is an edge e = (ℓ, g, R, ℓ ′ ) in A, and the following conditions hold: i) There is a region s with r ⋖ * s and t

= s[R ← 0],
ii) Let m ∈ {1, 2} and (s, S i ) for i = {1, m} be the constrained region(s) given by Lemma 5.3 applied to r, S r . There exists i ∈ {1, 2} such that for all SMs P , P ≤ S t iff there exists an SM Q ≤ S i with (s ′ , Q) = Unreset R ((t, P )), for some s ′ = s.

Notice that (t, S t ) can be computed in polynomial time thanks to Lemmas 5.3 and 3.12. Also, all constrained regions of the square nodes admit tight valuations by Lemma 5. Proof. Assume that Controller wins RG(A). As in the proof of Proposition 4.1, we assign to nodes n = (ℓ, r, S r ) in RG(A), shrunk DBMs (r ′ , P n ) with r ′ = r, describing the set of winning states from the corresponding locations in G δ (A). The construction and the proof are the same for square nodes. If n is a diamond node of the form (ℓ, r, S r ), then fix any s with r ⋖ * s and an edge e = (ℓ, g, R, ℓ ′ ) from n with s ⊆ g. Assume, by induction hypothesis, that we have shrunk DBMs (t, P n1 ) and (t, P n2 ) describing winning states from the successors n 1 = (ℓ ′ , t, S 1 t ) and n 2 = (ℓ ′ , t, S 2 t ) of n through the edge e, where t = s[R ← 0] (Assume n 1 = n 2 if there is only one such successor). Consider (s, S 1 ) and (s, S 2 ) given by Lemma 5.3 applied to r, S r (assume again that S 1 = S 2 if there is only one such constrained region). By construction, for each i ∈ {1, 2}, t, S i t is defined by Lemma 3.12, such that for all SMs P ni , P ni ≤ S i t iff there exists SM Q i ≤ S i with (s i , Q i ) = Unreset R ((t, P ni )), for some s i = s and s ⊆ s i . Then, by Lemma 5.

(s i , Q i ),
for some r s e = r with r ⊆ r s e . Here, (r s e , P s e ) describes a set of winning states from location ℓ assuming Perturbator chooses the edge e and delays anywhere in the region s. We define (r e , P e ) as the intersection of all (r s e , P s e ) with r ⋖ * s, and define (r ′ , P n ) as the intersection of all (r e , P e ) for all edges e leaving n. This concludes one direction of the proof. Now, assume that Perturbator wins RG(A). The proof of Proposition 4.1 is based on the construction of a strategy for G δ (A), that ensured that the valuation is always ǫ-tight inside any visited constrained region. When one projects the play in RG(A), this property allows Perturbator to choose valuations in G δ (A) belonging to any successor it would choose in RG(A) in order to win. Thus, Perturbator's strategy simply consists in following in G δ (A) its winning strategy in RG(A). The same proof carries over to timed games since Lemma 5.3 shows that given a ǫ-tight valuation of r, S r , there exist delays that lead to (ǫ + ǫ ′ )-tight valuations inside s, S 1 and s, S 2 for any ǫ ′ > 0.

Hardness Result

The hardness result is shown by reduction from the halting problem in linear-bounded alternating Turing machines. These are Turing machines whose computations do not use more tape cells than the size of the input, and checking whether there is an accepting computation is EXPTIME-complete. Each transition is either an instruction, a disjunction, or a conjunction. Disjunction and conjunction transitions are given with pairs of successor states. Given an input, the set of accepting states are defined inductively as follows. There is a distinguished accepting state which is accepting by definition. A state with an instruction is accepting if its successor is. A disjunctive state accepts if, and only if one of the successors is accepting, and a conjunctive state accepts if, and only if both of its successors are accepting. The acceptance condition can thus be formalized by a two-player game played on the Turing machine; the first player controls the disjunctive states and instructions, and the second player controls the conjunctive states. Proposition 6.1. The robust reachability problem is EXPTIME-hard.

The reduction has the following idea. We adapt a standard encoding of linearly bounded Turing machines for timed automata in order to take care of imprecisions. In addition, the gadget of Figure 14 allows the simulation of the alternation, thanks to the ability of distinguishing positive and negative perturbations. We now give the detailed proofs.

Proof. We use a reduction from the halting problem in linear-bounded alternating Turing machines over a two-letter alphabet Σ = {a, b}. Let M be such a Turing machine, and write n for the bound on the tape length. We assume w.l.o.g. that n ≥ 3 and that instructions are of the form:

• (disjunction) δ(q) = q ′ ∨ q ′′ • (conjunction) δ(q) = q ′ ∧ q ′′ • (instruction) δ(q) = (γ, γ ′ , dir, q ′ ) where γ, γ ′ ∈ {a, b} and dir ∈ {←, →}. Such a transition reads γ in the current cell, writes γ ′ and follows direction given by dir.

Our encoding of M uses the set of n + 2 clocks X = {x i | i = 1 . . . n} ∪ {y, z}. The content of cell i is encoded by clock x i : it is an a if the value of clock x i is ni, and a b if the value of clock x i is bounded below by 2ni. Due to robustness concerns, these guards will be relaxed a bit in the construction.

We assume the content of the tape is represented by a word w over alphabet Σ of length n. Let k ∈ N and ǫ ≥ 0. We say that a valuation v over X is a k-shift encoding of w with precision ǫ whenever v(y) = v(z) = 0, and for every 1 ≤ i ≤ n:

• w i = a iff -ǫ ≤ v(x i ) -(n -i) -k ≤ ǫ • w i = b iff -ǫ ≤ v(x i ) -(2n -i) -k
We encode the instructions as follows.

◮ Regular instruction. A transition δ(q) = (γ, γ ′ , dir, q ′ ) is mimicked thanks to modules instr i,k δ(q)=(γ,γ ′ ,dir,q ′ ) for every 1 ≤ i ≤ n and 0 ≤ k < n. Such a module is depicted on Figure 13: it is a sequence of n modules, the ith one being of a special shape. The initial state is (q, i, k, 1). We write I for the interval module instr i,k δ(q)=(γ,γ ′ ,dir,q ′ ) ab 1 ab 2 (γ → γ ′ ) i ab n q,i,k,1 q,i,k,2 q,i,k,3 q,i,k,i q,i,k,i+1 q,i,k,n q,i,k,n+1 q ′ ,dir(i),0,1 z=n y,z:=0 δ(q)=(γ,γ ′ ,dir,q ′ ) for the simulation of the regular instruction δ(q) = (γ, γ ′ , dir, q ′ ), and its constituent submodules. If dir = →, dir(i) = i + 1 if 1 ≤ i < n, and undefined otherwise. If dir = ←, dir(i) = i -1 if 1 < i ≤ n, and undefined otherwise.

The correctness of this module is given by the following lemma: Lemma 6.2. Let 0 ≤ ǫ ≤ 1 and 0 ≤ δ ≤ 1. Let w ∈ Σ n such that w i = γ. Assume module instr i,k δ(q)=(γ,γ ′ ,dir,q ′ ) is entered with valuation v which is a k-shift encoding of w with precision ǫ. The Controller has a unique strategy in this module, and for every response of the δ-perturbator, the valuation v ′ when leaving the module is a 0-shift encoding of w[w i ← γ ′ ] (the word obtained from w by replacing w i with γ ′ ) with precision 2δ.

Proof. There is a unique strategy for Controller, which is to play from state (q, i, k, j) when z reaches j with the unique possible transition: if initially |v(x j ) -(nj) -k| ≤ ǫ, then he will choose the top-most transition, and if initially v(x j ) ≥ 2nj + kǫ, then it will choose the bottom-most transition. Indeed note that in the first case, since ǫ ≤ 1, the value of clock x j when z reaches j lies within I + k. When clock x j is reset clock z is almost j (more precisely it lies between jδ and j + δ), whereas clock z is almost n when leaving the module (more precisely it lies between nδ and n + δ). In the second case, the value of x j is increased by almost n. This straightforwardly implies the mentioned property. Remark 6.3. Note that if the module above is entered while w i = γ, then it reaches a deadlock. This could be avoided using extra transitions to a sink state. ◮ Conjunction. δ(q) = q ′ ∧ q ′′ is mimicked thanks to modules conj i,k δ(q)=q ′ ∧q ′′ (for every 1 ≤ i ≤ n and 0 ≤ k < n) on Figure 14. As in the previous module, the Controller has no other choice than selecting the next transition when the constraint is satisfied. For the first transition, the δ-Perturbator can choose to do it a bit earlier, or a bit later, and depending on this, the controller will next choose either y = 1 ∧ z ≤ 2 or y = 1 ∧ z > 2.

q,i,k,1 q ′ ,i,k+3,1 q ′′ ,i,k+3,1 Let w ∈ Σ n . Assume module conj i,k δ(q)=q ′ ∧q ′′ is entered with valuation v which is a k-shift encoding of w with precision ǫ. The Controller has a unique strategy in this module, and the δ-Perturbator can choose to reach either (q ′ , i, k + 3, 1) or (q ′′ , i, k + 3, 1). In both cases, the valuation v ′ when leaving the module is a (k + 3)-shift encoding of w with precision ǫ + δ.

Proof. The Controller has no other choice than satisfying the next constraint of the next transition. On the other hand, the δ-Perturbator can either choose to postpone the first transition, or to fire it earlier. In the first case, the Controller has then to choose the bottom-most transition, and in the second case, the Controller has to choose the top-most transition. Globally the values of the clocks are increased by 3 (plus or minus δ), which yields the expected property.

Conclusion

We considered a game-based approach to robust reachability in timed automata, by modelling the semantics as a game between the controller and its environment. We proved that a bound on the imprecisions, and a corresponding robust strategy for reachability objectives in turn-based timed games can be synthesized, and that the existence of such a bound and a strategy is EXPTIMEcomplete. The problem is thus harder than classical reachability [START_REF] Alur | A theory of timed automata[END_REF]. A similar semantics was studied in [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF], and our result partially answers to an open problem posed there for parity objectives on general timed games.

A natural continuation of this work would be to look at zone-based on-the-fly algorithms, as for usual timed games in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF]. Note that solving usual timed games is also an EXPTIME-complete problem and on-the-fly algorithms allowed efficient implementations.

Developing algorithms for safety objectives, that is, ensuring infinite executions that avoid some given state would require the use of different techniques and seems to be a challenging problem. In fact, in that setting, one has to deal with the accumulation of the imprecisions over infinite runs, which cannot be avoided by adjusting δ.

We are currently studying a different model in which the controller is required to choose delays for which the guard of the chosen edge is satisfied no matter what the perturbation is, which is the parameterized version of the framework of [START_REF] Chatterjee | Timed parity games: Complexity and robustness[END_REF]. We believe both semantics are interesting and allow different ways of incorporating perturbations in the model. Another interesting perturbation model is to assume that imprecisions are probabilistic, that is, once Controller has chosen a delay d, the actual delay is chosen from [dδ, d + δ] following a probability distribution. We use synchronization on labels lock i : the meaning of lock i ! is that the corresponding edge can only be taken if another component takes an edge labeled with lock i ?, and vice versa. For instance, in automaton P 1 , the task A can be executed on M 1 (first edge), only if lock 1 can be taken. The lock is released upon the termination of the task (second edge). Automaton M has two boolean variables b 1 , b 2 , where b i is set to true if machine M i is busy. The two self-loops are defined for i = 1, 2. For instance, the automaton M synchronizes with action lock i only if b i is not set to true. It has the invariants ∀i ∈ {1, 2}, ¬b i ∧ Waiting i ⇒ u = 0 and t ≤ c. The first one ensures greedy scheduling, while the second one blocks the time above c time units. 2 Here, Waiting i is a formula stating that some task is ready for execution on machine i. We omit the definition of Waiting i here but it can be easily defined once we add a boolean variable for each task that is true if, and only if the task has finished. Hence, automaton M blocks time in the whole system if some task is ready for execution on a machine that is free. Now, the reachability of the location (p 5 , q 7 , r) in the product of P 1 , P 2 and M means that the tasks are schedulable in c time units. For instance, this location is reachable for c = 6 in the usual semantics as shown in Section 2.2. A strategy that ensures the reachability of this location gives a greedy scheduler. However, this location is not robustly reachable for c = 6, but it is only for c = 8. In fact, the product automaton contains the following transitions. The automaton must indeed start by scheduling the task A on M 1 . At state (p 3 , q 1 ), it can choose between scheduling C (upper transition) and scheduling B (lower transition). The former one is always enabled in the usual semantics, and yields a total scheduling time of 6. But in the game semantics, the lower transition may be the only option if we have a negative perturbation during the transition (p 2 , q 1 ) → (p 3 , q 1 ). This can only yield a scheduling time of 8 as shown before.

Figure 2 :Figure 3 :

 23 Figure 2: Timed automaton A.

  [a,b] (Z) = {v | v + [a, b] ⊆ Z} for any zone Z. We only use operators shrink [0,δ] and shrink [-δ,δ] in the sequel. For a zone Z represented as a DBM, shrink [0,δ] (Z) is the DBM Z

  Figure 4: On the right of Fig.4(a), the gray area represents a zone N 1 , while the dark gray area is some shrinking (N 1 , Q). On the left, the dark area is the shrunk zone (M, P ) where M = Pre time (N 1 ). Similarly, Fig.4(b) to 4(d) illustrate the intersection of two shrunk zones and the shrinking of zones.

Figure 5 :

 5 Figure 5: Perturbing one transition.

  ,y = S x1,xn = 0, we also have S x1,x2 = 0 and S x2,xn = 0 By induction, Q ′ x1,x2 = 0 and all paths of Π x2,xn (G(M )) of length at most n -1 have weight 0 in Q ′ . Hence, π has weight 0 in Q ′ .

  y , and S xj ,xj+1 = 0 for all 1 ≤ j ≤ n -1, as S is normalized. It follows that P xj ,xj+1 = 0, hence also P ′ xj ,xj+1 = 0. Suppose now that for some 1 ≤ j ≤ n -1, M xj ,xj+1 < N xj ,xj+1 . We have P ′ xj ,xj+1 = 0. On the other hand, S ′ x1,xj = S ′ xj+1,xn = 0 since otherwise we would get S ′ x,y = ∞. By induction, all paths of length at most n -1 in Π x1,xj (G(M )) and Π xj+1,xn (G(M )) have weight 0 in P ′ . So π has weight 0 in P ′ .

Figure 8 :

 8 Figure 8: Examples for both cases of Lemma 3.13

Figure 9 :

 9 Figure 9: Constrained neighborhood of two constrained regions. Notice that inside any shrinking of the constrained region, there is always a valuation such that a perturbation of [-δ, δ] moves the valuation to any region of the neighborhood.

4. 1 .

 1 Proof of Proposition 4.1 4.1.1. Controller wins RG(A) ⇒ Controller wins G δ (A) for all small enough δ > 0.

  A region r and its time successors inside r ′ .

  If (S r ) xi,xi+1 = 0 for all 1 ≤ i ≤ n -1 and (S r ) x1,xn = ∞, then consider any SM P withP x1,xn = 1. If ν is ǫ-tight in r -δP , then we have r xi,xi+1ǫ ≤ ν(x i )ν(x i+1 ) for all 1 ≤ i ≤ n -1. Summing these yield n-1 i=1 r xi,xi+1nǫ ≤ ν(x 1 )ν(x n ). We have n-1 i=1 r xi,xi+1 = r x1,xnby hypothesis, and also ν(x 1 )ν(x n ) ≤ rδ. Now, this means r x1,xnǫn ≤ r x1,xnδ, which is a contradiction for small enough ǫ > 0.

  Post time (M ) and S ≤ Well(M ). There exists a shrinking constraint S ′ for N such that for all SMs Q, Q ≤ S ′ if, and only if there exists P ≤ S with Post time ((M, P )) = (N ′ , Q) with N ′ = N.

Proposition 5 . 4 .

 54 3 and Corollary 4.8. Theorem 2.3, for turn-based timed games, follows from the following proposition. For any turn-based timed game A, Controller has a winning strategy in RG(A) if, and only if there exists δ 0 > 0 such that Controller wins G δ (A) for all δ ∈ [0, δ 0 ].

Figure 12 :

 12 Figure12: Intermediary modules: when traversing module abp, either clock xp belongs to I + k while z = p, corresponding to an a at position p. Clock xp is then reset, so that position p still contains an a; or clock xp is in I ′ + k when z = p, encoding a b at position p. In that case, clock xp is not reset, and the content of cell p is preserved. Using similar ideas, modules (γ → γ ′ )p, with γ, γ ′ ∈ {a, b}, check that cell p initially contains γ, and replace it with γ ′ .

Figure 13 :

 13 Figure 13: Module instr i,kδ(q)=(γ,γ ′ ,dir,q ′ ) for the simulation of the regular instruction δ(q) = (γ, γ ′ , dir, q ′ ), and its constituent submodules. If dir = →, dir(i) = i + 1 if 1 ≤ i < n, and undefined otherwise. If dir = ←, dir(i) = i -1 if 1 < i ≤ n, and undefined otherwise.

y=1, y:=0 y = 1 ∧ z ≤ 2 y = 1 ∧ z > 2 z=3Figure 14 :

 121214 Figure 14: Module conj i,k δ(q)=q ′ ∧q ′′ for conjunctive transition

1 Figure A. 18 :Figure A. 19 :

 11819 Figure A.18: Timed automaton P 2 modeling Process 2.

Here, the non-emptiness hypothesis in only significant for i = 1.

Note that we do not really need to consider invariants. We could as well add this constraint as guards in the edges of M.

✩ Partly supported by the French ANR project ImpRo (ANR-10-BLAN-0317), by ERC Starting grants EQualIS (FP7-308087) and inVEST (FP7-279499), and by European FET project Cassting (FP7-601148)

How much can m grow? A quick analysis shows that it is at most doubly exponential in the size of the input. In fact, the size of RG(A) can be exponential in the size of the automaton, and the number of shrunk DBMs involved in our computations are linear in the size of RG(A). In fact, we apply, for each edge, a constant number of operations on shrunk DBMs. Whenever we apply such an operation, and say, obtain (M, P ), we apply normalization on (M, P ), which consists in assigning to each P i,j , the P -weight of the longest path in G(M ) from i to j. So at each operation, the maximal constant of shrinking matrices is multiplied at most by |C 0 |. Considering the size of M, we get that m = O(|C 0 | 2 |A| ). Note however that this is an extremely pessimistic estimation; it is unlikely that parameters will grow that much at each step, and never be reset along a path. This is confirmed by the experimental results of [START_REF] Sankur | Shrinktech: A tool for the robustness analysis of timed automata[END_REF], where shrunk DBMs are used to solve a different problem. To prove the theorem, we will assume the Controller loses in RG(A), and we will construct a winning strategy for the δ-Perturbator in G δ (A) by looking at the projection of the plays in RG(A), and by imitating the moves of a winning strategy for the Perturbator in RG(A). The core idea is to show that the Perturbator can always force the game to be close, by some chosen ǫ, to all boundaries of the current region for which the shrinking constraint is 0. This will ensure that from any state of the play, for any move of Controller, Perturbator can force the game to some state inside any successor in RG(A).

Let us first formalize what we mean by being close to boundaries.

Definition 4.3. Let M, S any constrained DBM. For any ǫ ≥ 0, we say that a valuation ν is ǫ-tight in M w.r.t. S if ν ∈ M , and,

We say that M admits tight valuations w.r.t. S if it admits ǫ-tight valuations for any ǫ > 0.

We say that M, S admits tight valuations if for any P ≤ S, and for all small enough δ > 0, M -δP admits tight valuations w.r.t. S.

In the proofs, we will also say that ν is ǫ-tight in M for a component (x, y) ∈ C 2 0 when M x,yǫ ≤ ν(x)ν(y).

We show that for any move of Controller in G δ (A) from an ǫ-tight valuation, the corresponding edge exists in RG(A): Lemma 4.4. Fix δ > 0 and ǫ ≤ δ 2 . Assume that ν is ǫ-tight in r w.r.t. S, and let ν ′ = (ν + d) for some d ≥ δ, and some edge e = (ℓ, g, R, ℓ ′ ) with ν ′ |= g. Then, RG(A) has an edge from (ℓ, r, S r ) to (ℓ, r ′ , S r ′ , e) for r ′ = reg(ν ′ ) and for some S r ′ .

Proof. Let N = Pre time (r ′ ), and consider, by Lemma 3.12, the shrinking constraint S N such that for any SM Q, Q ≤ S N if, and only if the SM P such that (r, P ) = r ∩ (N, Q) satisfies P ≤ S r . Thanks to Lemma 3.16, it is sufficient to show that (S N ) x,0 = ∞ for all x ∈ C. To get a contradiction, assume that (S N ) x,0 = 0 for some x ∈ C. By (the proof of) Lemma 3.12, S N is the normalization of S ′ r defined by (S ′ r ) x,y = (S r ) x,y if r x,y = N x,y and (S ′ r ) x,y = ∞ otherwise. So, (S N ) x,0 = 0 means that there exists (z, z ′ ) such that (x, 0) is on some path π of Π z,z ′ (G(N )), r z,z ′ = N z,z ′ and (S r ) z,z ′ = 0. But since r ⊆ N and r z,z ′ = N z,z ′ we have Π z,z ′ (G(N )) ⊆ Π z,z ′ (G(r)). Moreover, all weights along π are the same in r and N . We get (S r ) x,0 = 0. On the other hand, since r ′ ⊆ N and r ⋖ * r ′ , we have r x,0 ≤ r ′

x,0 ≤ N x,0 . So r x,0 = r ′ x,0 . By hypothesis, we have r x,0ǫ ≤ ν(x) ≤ r x,0 . But ǫ ≤ δ/2 and d ≥ δ, so ν(x) + d > r x,0 = r ′

x,0 , a contradiction.

(S r ) x,y = 0 implies that (S r ) x ′ ,y ′ = 0 for all x ′ ∈ X k ′ and y ′ ∈ X l ′ with k ≤ k ′ < l ′ ≤ l, because S r is normalized. Moreover, for such a pair x, y, if for z ∈ X l+1 , we have (S r ) y,z = 0, then also (S r ) x,z = 0. This follows from the hypothesis since x, y, z ∈ Π x,z (G(r)) and has S r -weight equal to 0. Thus, the sequence (α i , α ′ i ) i is well-defined. Consider x ∈ X k and y ∈ X l for k ∈ [α i , α ′ i ] and y ∈ [α j , α ′ j ] with i < j, then (S r ) x,y = ∞. In fact, for any clock z ∈ X α ′ i and z ′ ∈ X αj , we have x, z, z ′ , y ∈ Π x,y (G(r)), and (S r ) z,z ′ = ∞ by definition of the sequence α, α ′ .

We now show that (r, S r ) has ǫ-tight valuations. Consider any normalized SM P ≤ S r and 1/δ > 2(|C| + 2) max x,y∈C0 (P x,y ).

Fix any 0 < ǫ < δ/2. We define a valuation ν as follows. We let ν(x) = r x,0 for x ∈ X 1 . We choose the values ν(x) for x ∈ X 2 ∪ . . . ∪ X j0 as -r 0,x < ν(x) < -r 0,x + ǫ/2, such that they respect the fractional ordering. Similarly, we choose r x,0ǫ/2 < ν(x) < r x,0 for x ∈ X i0 ∪ . . . ∪ X n , respecting the fractional ordering. Define

respecting the fractional orderings. The valuation is illustrated in the following figure.

We show that ν is ǫ-tight in r -δP . We verify at the same time that ν belongs to r -δP , and that it is ǫ-tight. We first consider the constraints between clocks X 2 ∪ . . . X j0 and X i0 ∪ . . . ∪ X n , then between clocks in x j0+1 ∪ . . . ∪ X i0-1 , and finally for pairs between the two sets.

1. For all x ∈ X 2 ∪ . . . ∪ X j0 , we have, by definition (S r ) 0,x = 0 and -r 0,x < ν(x) < -r 0,x + ǫ/2, and (S r ) x,0 = ∞. By the choice of δ, ν(x) < -r 0,x + ǫ/2 < r x,0 -δQ x,0 . For any pair x ∈ X k and y ∈ X l with 1 ≤ k < l ≤ j 0 , we have (S r ) x,y = 0 by normalization since 0, x, y is in Π 0,y (G(r)), but the previous inequality implies that r x,yǫ/2 < ν(x)ν(y) < r x,y . We have, therefore, (S r ) y,x = ∞, and ν(y)ν(x) < -r x,y + ǫ/2 < r y,x -δP x,y by the choice of δ.

2. Similarly, for all x ∈ X i0 ∪ . . . ∪ X n , we have (S r ) 0,x = ∞, (S r ) x,0 = 0 and r x,0ǫ/2 < ν(x) < r x,0 . For any pair x ∈ X k and y ∈ X l with i 0 ≤ k < l ≤ n, we have (S r ) x,y = 0 as before, and r x,yǫ/2 < ν(x)ν(y) < r x,y . We have (S r ) y,x = ∞, and ν(y)ν(x) < -r x,y + ǫ/2 < r y,x -δP y,x by the choice of δ and ǫ.

3. For any pair x ∈ X 2 ∪ . . . ∪ X j0 and y ∈ X i0 ∪ . . . ∪ X n , we have (S r ) y,x = 0 by hypothesis, since y, 0, x is in Π y,x (G(r)) and all edges have S r -weight 0. Thus, ν(y)ν(x) < r y,x -δP y,x , and we have r y,xǫ < ν(y)ν(x) since ν(x) > r x,0ǫ/2 and ν(y) < -r 0,y + ǫ/2. Furthermore, -r x,y + δP x,y < ν(y)ν(x) since -r x,y + δP x,y < r y,xǫ by the choice of δ and ǫ.

Let us now consider constraints between clocks in

5. Consider now clock x ∈ X 2 ∪ . . . ∪ X j0 and y ∈ X j0+1 ∪ . . . ∪ X i0-1 . We have (S r ) x,y = ∞ by hypothesis. In fact, (0, x, y) ∈ Π 0,y (G(r)) and (S r ) x,y = 0 would imply (S r ) 0,y = 0. Also, there exists an SM P ≤ S r with

for all small δ > 0. Moreover, in this case, for any ǫ-tight valuation v ∈ (r, P ) and any i ∈ {1, 2} and ǫ ′ > 0, there exists

Proof. Consider the clock ordering of a constrained region with tight valuations as in the proof of Lemma 5.1. We assume the indices 1 ≤ i 0 , j 0 ≤ n and α i , α ′ i 's are defined (see figure below). We distinguish cases according to the last clock that crosses an integer value during the delay from r to r ′ : There exists 1 ≤ k 0 ≤ n and m ∈ N such that for all x ∈ X 1 ∪ . . . ∪ X k0 , -r ′ 0,x = -r 0,x + m, while for all x ∈ X k0+1 ∪ . . . ∪ X n , we have -r ′ 0,x = -r 0,x + m + 1. Notice that -r 0,x is the integer part of the clock x in region r. If all integer parts have grown by m, then we let k 0 = 1. In the following figure, we represent by a vertical gray line some possible values of the index k 0 .

We distinguish several cases according to the relative position of k 0 .

1. Assume that 1 ≤ k 0 ≤ j 0 -1. The clock ordering before the delay is illustrated in the following figure in black, whereas the ordering after the delay is given between the gray 0 and 1.

Let us consider the shrinking constraint S r ′ given by Lemmas 3.12 and 5.2, so that for all SMs Q, we have Q ≤ S r ′ iff there is P ≤ S with Post time (r -δP ) ∩ r ′ ⊆ r ′ -δQ. The constraint S r ′ can be obtained from S r by only changing the following components: for all x ∈ X 1 ∪ . . . ∪ X k0 (S r ′ ) x,0 = 0, and either r ′ x,0 = -r ′ x,0 and (S r ′ ) 0,x = 0 or (S r ′ ) 0,x = ∞. In fact, since r ′ -δQ contains the successors of r -δP , the diagonal constraints are the same. Moreover, the partition of the clocks given by i 0 , j 0 and α i , α ′ i 's are preserved by delays; while time is only translated. So the clocks X 0 , . . . , X k0 will be mixed with X i0 , . . . , X n but the constraints on the rest of the clocks will remain. By Lemma 5.1, (r ′ , S r ′ ) has tight valuations.

Consider SMs Q and P such that Post time (r -δP ) ∩ r ′ ⊆ r ′ -δQ for all small enough δ > 0. Let ν ∈ r -δP be an ǫ-tight valuation in (r, S r ). Define

otherwise (if k 0 = n, then let us assume x n+1 = 1). Then, according to the definition of k 0 and m, ν + d belongs to r ′ . Therefore, also ν + d ∈ r -δQ. We show that ν + d is ǫ-tight in (r ′ , S r ′ ). Diagonal components stay unchanged both in shrinking constraints and in valuations, so we only need to verify the constraints (S r ′ ) x,0 and (S r ′ ) 0,x . Since the distances between the first j 0 clocks are at most ǫ in ν (i.e. ν(x j0 ) -

This follows from the fact that r y,xǫ ≤ ν(y)ν(x) ≤ r y,x (which holds by hypothesis on (r, S r )).

The case where k 0 ≥ i 0 + 1 is symmetric.

2. Assume that j 0 ≤ k 0 < α 1 . Note that we may have X j0 = ∅ or X i0 = ∅, or both. We define two shrinking constraints S 1 r ′ and S 2 r ′ , such that (r, S i r ′ ) admits tight valuations for both i = 1, 2. Both have the same diagonal components as S r , since these do not change along delays. The first one corresponds to delaying to points where clocks X k0 can be very close to their upper integer values (Fig. 11(a)), and the second one to points where clocks X α1 are very close to their integer parts (Fig. 11(b)). We will show that for any pair Q 1 ≤ S 1 r ′ and Q 2 ≤ S 2 r ′ , there is a corresponding P ≤ S r such that any valuation obtained by delaying from r -δP inside r ′ lies either in (r ′ -δQ 1 ) or (r ′ -δQ 2 ), and moreover ǫ-tight valuations are reached in these shrunk regions if one starts at an ǫ-tight valuation in (r, S r ).

To define (S i r ′ ), we modify S r as follows. We let (S 1 r ′ ) x,0 = 0 and (S 1

Then, similarly, (S 2 r ′ ) admits ǫ-tight valuations. The definitions are illustrated in Figure 11. Consider any pair of SMs Q i ≤ (S i r ′ ) for i ∈ {1, 2}. We define P satisfying S r as follows. We let P x,0 = 0 whenever (S r ) x,0 = 0 or (S r ′ ) x,0 = 0, and P 0,x = 0 whenever (S r ) 0,x = 0. We choose arbitrary values for other components satisfying S r and the following constraints: (a) P x,y ≥ max(Q 1

x,y , Q 2 x,y ) for all x, y ∈ C. Notice here that Q 1

x,y = Q 2 x,y = 0 whenever (S r ) x,y = 0 by definition of S 1 r ′ and S

This shows that one can choose values for P while satisfying S r . Note also that normalization of P can only increase its components, so all lower bounds given above will still be satisfied.

Consider any ν ∈ r -δP . Let us show that for any d ≥ 0 with ν + d ∈ r ′ , we have

x,y for small enough δ > 0. In fact, either (S r ′ ) x,y = 0 and (Q i ) x,y = 0 for i = 1, 2, since S i r ′ has the same diagonal components as S r , or P x,y ≥ max((Q 1 ) x,y , (Q 2 ) x,y ).

It remains to choose i ∈ {1, 2} such that the constraints on the components (x, 0) and (0, x) are satisfied. Let us write ν ′ = ν + d. ◮ Disjunction. δ(q) = q ′ ∨ q ′′ is mimicked thanks to modules disj i,k δ(q)=q ′ ∨q ′′ (for every 1 ≤ i ≤ n and 0 ≤ k < n) on Figure 15.

q,i,k,1 q ′ ,i,k+1,1 q ′′ ,i,k+1,1 y,z:=0 y = 1 , y ,z := 0 y = 1 , y ,z := 0 Figure 15: Module disj i,k δ(q)=q ′ ∧q ′′ for disjunctive transition Lemma 6.5. Let ǫ ≥ 0 and δ ≥ 0. Let w ∈ Σ n . Assume module disj i,k δ(q)=q ′ ∨q ′′ is entered with valuation v which is a k-shift encoding of w with precision ǫ. The Controller can choose to reach either (q ′ , i, k + 1, 1) or (q ′′ , i, k + 1, 1). In both cases, the valuation v ′ when leaving the module is a (k + 1)-shift encoding of w with precision ǫ + δ.

Proof. Similar to the previous proof.

◮ Reset module. We fix an integer 0 ≤ k < n. Shifts encodings accumulate when stacking disjunctive and conjunctive instructions. We present a module reset i,k q which resets the shift from state q, position i. module reset i,k q ab 1 ab 2 ab n q,i,k,1 q,i,k,2 q,i,k,3 q,i,k,n q,i,k,n+1 q,i,0,1 z=n y,z:=0 q which resets the shift in the encoding.

Lemma 6.6. Let 0 ≤ ǫ ≤ 1 and 0 ≤ δ ≤ 1. Let w ∈ Σ n . Assume module reset q,i,k is entered with valuation v which is a k-shift encoding of w with precision ǫ. The Controller has a unique strategy in this module, and for every response of the δ-Perturbator, the valuation v ′ when leaving the module is a 0-shift encoding of w with precision 2δ.

Proof. This proof is similar to the proof of Lemma 6.2.

◮ Global reduction. It remains to glue all the modules together. An easy solution is to apply the reset module after each conjunctive or disjunctive instruction (though there are some more thrifty solutions). The reset module allows both to reset the shift and to reinitialize the imprecision. We write A for the resulting timed automaton. The halting location of the Turing machine is called final in A.

One can easily check that in A, letting 0 ≤ δ < 1 2 , the Controller has a winning strategy against the δ-Perturbator to reach location final if, and only if, the Turing machine M halts.

Appendix A. Modelling of our scheduling example

The scheduling problem described in Fig. 1 contains two processes: Process 1 executing A and B, and Process 2 executing C, D, and E. Both processes need the same resources (machines M 1 and M 2 ), which can only be used exclusively. This system can be modelled by a network of timed automata, as follows. We define a timed automaton P 1 corresponding to Process 1, and P 2 corresponding to Process 2. A third timed automaton M will make sure the mutual exclusion for both machines: no more than one task is executed on a machine at any time. Moreover, we will also use M in order to impose a greedy scheduling: this automaton will block time if some task is waiting for execution on a machine that is free (more details follow below). Each automaton P i makes sure that its tasks are executed respecting the dependences and timing constraints. All three timed automata are given in figures below. Note that we use additional features such as invariants, boolean variables and synchronization, which we didn't define, but it can be seen that an equivalent system can be defined as an ordinary timed automaton.