Youssouf Oualhadj

Pierre-Alain Reynier

Ocan Sankur

Probabilistic Robust Timed Games ⋆

Solving games played on timed automata is a well-known problem and has led to tools and industrial case studies. In these games, the first player (Controller) chooses delays and actions and the second player (Perturbator) resolves the non-determinism of actions. However, the model of timed automata suffers from mathematical idealizations such as infinite precision of clocks and instantaneous synchronization of actions. To address this issue, we extend the theory of timed games in two directions. First, we study the synthesis of robust strategies for Controller which should be tolerant to adversarially chosen clock imprecisions. Second, we address the case of a stochastic perturbation model where both clock imprecisions and the non-determinism are resolved randomly. These notions of robustness guarantee the implementability of synthesized controllers. We provide characterizations of the resulting games for Büchi conditions, and prove the EXPTIME-completeness of the corresponding decision problems.

Introduction

For real-time systems, timed games are a standard mathematical formalism which can model control synthesis problems under timing constraints. These consist in two-players games played on arenas, defined by timed automata, whose state space consists in discrete locations and continuous clock values. The two players represent the control law and the environment. Since the first theoretical works [2], symbolic algorithms have been studied [10], tools have been developed and successfully applied to several case studies.

Robustness Because model-based techniques rely on abstract mathematical models, an important question is whether systems synthesized in a formalism are implementable in practice. In timed automata, the abstract mathematical semantics offers arbitrarily precise clocks and time delays, while real-world 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 major challenge is thus to ensure that the synthesized control software is robust, i.e. ensures the specification even in presence of imprecisions [START_REF] Henzinger | The embedded systems design challenge[END_REF]. Following these observations there has been a growing interest in lifting the theory of verification and synthesis to take robustness into account. Modelchecking problems were re-visited by considering an unknown perturbation parameter to be synthesized for several kinds of properties [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] De Wulf | Robust safety of timed automata[END_REF]7], see also [9]. Robustness is also a critical issue in controller synthesis problems. In fact, due to the infinite precision of the semantics, synthesized strategies may not be realizable in a finite-precision environment; the controlled systems synthesized using timed games technology may not satisfy the proven properties at all. In particular, due to perturbations in timings, some infinite behaviors may disappear completely. A first goal of our work is to develop algorithms for robust controller synthesis: we consider this problem by studying robust strategies in timed games, namely, those guaranteeing winning despite imprecisions bounded by a parameter.

Adversarial or Stochastic Environments We consider controller synthesis problems under two types of environments. In order to synthesize correct controllers for critical systems, one often considers an adversarial (or worst-case) environment, so as to ensure that all behaviors of the system are correct. However, in some cases, one is rather interested considering a stochastic environment which determines the resolution of non-determinism, and the choice of clock perturbations following probability distributions. We are then interested in satisfying a property almost-surely, that is, with probability 1, or limit-surely, that is, for every ε > 0, there should exist a strategy for Controller under which the property is satisfied with probability at least 1ε.

Contributions We formalize the robust controller synthesis problem against an adversarial environment as a (non-stochastic) game played on timed automata with an unknown imprecision parameter δ, between players Controller and Perturbator. The game proceeds by Controller suggesting an action and a delay, and Perturbator perturbing each delay by at most δ and resolving the nondeterminism by choosing an edge with the given action. Thus, the environment's behaviors model both uncontrollable moves and the limited precision Controller has. We prove the EXPTIME-completeness of deciding whether there exists a positive δ for which Controller has a winning strategy for a Büchi objective, matching the complexity of timed games in the classical sense. Our algorithm also allows one to compute δ > 0 and a witness strategy on positive instances.

For stochastic environments, we study two probabilistic variants of the semantics: we first consider the case of adversarially resolved non-determinism and independently and randomly chosen perturbations, and then the case where both the non-determinism and perturbations are randomly resolved and chosen. In each case, we are interested in the existence of δ > 0 such that Controller wins almost-surely (resp. limit-surely). We give decidable characterizations based on finite abstractions, and EXPTIME algorithms. All problems are formulated in a parametric setting: the parameter δ is unknown and is to be computed by our algorithms. This is one of the technical challenges in this paper.

Our results on stochastic perturbations can also be seen as a new interpretation of robustness phenomena in timed automata. In fact, in the literature on robustness in timed automata, non-robust behaviors are due to the accumulation of the imprecisions δ along long runs, and in the proofs, one exhibits non-robustness by artificially constructing such runs (e.g. [START_REF] De Wulf | Robust safety of timed automata[END_REF][START_REF] Sankur | Robust controller synthesis in timed automata[END_REF]). In contrast, in the present setting, we show that non-robust behaviors either occur almost surely, or can be avoided surely (Theorem 13).

Related Work While several works have studied robustness issues for modelchecking, there are very few works on robust controller synthesis in timed systems:

-The (non-stochastic) semantics we consider was studied for fixed δ in [11] encoding by timed games; but the parameterized version of the problem was not considered.

-The restriction of the parameterized problem to (non-stochastic) deterministic timed automata was considered in [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF]. Here, the power of Perturbator is restricted as it only modifies the delays suggested by Controller, but has no non-determinism to resolve. Therefore, the results consist in a robust Büchi acceptance condition for timed automata, but they do not generalize to timed games. Technically, the algorithm consists in finding an aperiodic cycle, which are cycles that are "stable" against perturbations. This notion was defined in [3] to study entropy in timed languages. We will also use aperiodic cycles in the present paper.

-A variant of the semantics we consider was studied in [8] for (deterministic) timed automata and shown to be EXPTIME-complete already for reachability due to an implicit presence of alternation. Timed games, Büchi conditions, or stochastic environments were not considered.

-Probabilistic timed automata where the non-determinism is resolved following probability distributions have been studied [START_REF] Jensen | Model checking probabilistic real time systems[END_REF]4,[START_REF] Kwiatkowska | Automatic verification of real-time systems with discrete probability distributions[END_REF]. Our results consist in deciding almost-sure and limit-sure Büchi objectives in PTAs subject to random perturbations in the delays. Note that PTAs are equipped with a possibly different probability distribution for each action. Although we only consider uniform distributions, the two settings are equivalent for almost-sure and limitsure objectives. Games played on PTA were considered in [START_REF] Forejt | Expected reachability-time games[END_REF] for minimizing expected time to reachability with NEXPTIME ∩ co-NEXPTIME algorithms.

To the best of our knowledge, this work is the first to study a stochastic model of perturbations for synthesis in timed automata.

Organization Definitions are given in Section 2. Preliminaries concerning the notions of regions graphs, orbit graphs and shrunk difference bound matrices are presented in Section 3. The finite-state game abstraction used to characterize the positive instances of the (non-stochastic) problem is presented in Section 4 and the proof of correction is given in Section 5. In Section 6, we consider the two stochastic models for the environment.

2 Robust Timed Games Timed automata. Given a finite set of clocks C, we call valuations the elements of R C ≥0 . For a subset R ⊆ C and a valuation ν, ν[R ← 0] is the valuation defined by ν[R ← 0](x) = 0 if x ∈ R and ν[R ← 0](x) = ν(x) otherwise. Given d ∈ R ≥0 and a valuation ν, the valuation ν + d is defined by (ν + d)(x) = ν(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 x-y ′ l where x, y ∈ C, k, l ∈ Z ∪ {-∞, ∞} and , ′ ∈ {<, ≤}. A guard is a conjunction of atomic clock constraints. A valuation ν satisfies a guard g, denoted ν |= g, if all constraints are satisfied when each x ∈ C is replaced with ν(x). We write Φ C for the set of guards built on C. A zone is a subset of R C ≥0 defined by a guard. A timed automaton A over a finite alphabet of actions Act is a tuple (L, C, ℓ 0 , Act, E), where L is a finite set of locations, C is a finite set of clocks, E ⊆ L × Φ C × Act × 2 C × L is a set of edges, and ℓ 0 ∈ L is the initial location. An edge e = (ℓ, g, a, R, ℓ ′ ) is also written as ℓ g,a,R ---→ ℓ ′ . A state is a pair q = (ℓ, ν) ∈ L×R C ≥0 . An edge e = (ℓ, g, a, R, ℓ ′ ) is enabled in a state (ℓ, ν) if ν satisfies the guard g.

The set of possible behaviors of a timed automaton can be described by the set of its runs, as follows. A run of A is a sequence q 1 e 1 q 2 e 2 . . . where q i ∈ L × R C ≥0 , and writing q i = (ℓ, ν), either e i ∈ R >0 , in which case q i+1 = (ℓ, ν + e i ), or e i = (ℓ, g, a, R, ℓ ′ ) ∈ E, in which case ν |= g and q i+1 = (ℓ ′ , ν[R ← 0]). The set of runs of A starting in q is denoted Runs(A, q). Parameterized timed game. In order to define perturbations, and to capture the reactivity of a controller to these, we define the following parameterized timed game semantics. Intuitively, the parameterized timed game semantics of a timed automaton is a two-player game parameterized by δ > 0, where Player 1, also called Controller chooses a delay d > δ and an action a ∈ Act such that every a-labeled enabled edge is such that its guard is satisfied after any delay in the set d + [-δ, δ] (and there exists at least one such edge). Then, Player 2, also called Perturbator chooses an actual delay d ′ ∈ d + [-δ, δ] after which the edge is taken, and chooses one of the enabled a-labeled edges. Hence, Controller is required to always suggest delays that satisfy the guards whatever the perturbations are.

Formally, given a timed automaton A = (L, C, ℓ 0 , Act, E) and δ > 0, we define the parameterized timed game of A w.r.t. δ as a two-player turn-based game G δ (A) between players Controller and Perturbator. The state space of

G δ (A) is partitioned into V C ∪ V P where V C = L × R C
≥0 belong to Controller, and

V P = L × R C ≥0 × R ≥0 × Act belong to Perturbator. The initial state is (ℓ 0 , 0) ∈ V C .
The transitions are defined as follows: from any state (ℓ, ν) ∈ V C , there is a transition to (ℓ, ν, d, a) ∈ V P whenever d > δ, for every edge e = (ℓ, g, a, R, ℓ ′ ) such that ν + d |= g, we have ν + d + ε |= g for all ε ∈ [-δ, δ], and there exists at least one such edge e. Then, from any such state (ℓ, ν, d, a) ∈ V P , there is a transition to (ℓ ′ , ν ′ ) ∈ V C iff there exists an edge e = (ℓ, g, a, R, ℓ ′ ) as before, and

ε ∈ [-δ, δ] such that ν ′ = (ν + d + ε)[R ← 0]). A play of G δ (A)
is a finite or infinite sequence q 1 e 1 q 2 e 2 . . . of states and transitions of G δ (A), with q 1 = (ℓ 0 , 0), where e i is a transition from q i to q i+1 . It is said to be maximal if it is infinite or cannot be extended. A strategy for Controller is a function that assigns to every non-maximal play ending in some (ℓ, ν) ∈ V C , a pair (d, a) where d > δ and a is an action such that there is a transition from (ℓ, ν) to (ℓ, ν, d, a). A strategy for Perturbator is a function that assigns, to every play ending in (ℓ, ν, d, a), a state (ℓ ′ , ν ′ ) such that there is a transition from the former to the latter state. A play ρ is compatible with a strategy f for Controller if for every prefix ρ ′ of ρ ending in V C , the next transition along ρ after ρ ′ is given by f . We define similarly compatibility for Perturbator's strategies. A play naturally gives rise to a unique run, where the states are in V C , and the delays and the edges are those chosen by Perturbator.

Robust timed game problem. Given δ > 0, and a pair of strategies f, g, respectively for Controller and Perturbator, we denote ρ the unique maximal run that is compatible with both f and g. A Büchi objective is a subset of the locations of A. A Controller's strategy f is winning for a Büchi objective B if for any Perturbator's strategy g the run ρ that is compatible with f and g is infinite and visits infinitely often a location of B. The robust timed game problem asks, for a timed automaton A and a Büchi objective B, if there exists δ > 0 such On the left, a timed automaton from [START_REF] Puri | Dynamical properties of timed automata[END_REF] that is not robustly controllable for the Büchi objective {ℓ2}. In fact, Perturbator can enforce that the value of x be increased by δ at each arrival at ℓ1, thus blocking the run eventually (see [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF]). On the right, a timed automaton that is robustly controllable for the Büchi objective {ℓ1, ℓ2, ℓ3}. We assume that all transitions have the same label. The cycle around ℓ1 cannot be taken forever, as value of x increases due to perturbations. The cycle around ℓ2 can be taken forever, but Controller cannot reach ℓ2 due to the equality x = 1. Controller's strategy is thus to loop forever around ℓ3. This is possible as for both choices of Perturbator in location ℓ4, clock x will be reset, and thus perturbations do not accumulate. If one of the two resets were absent, Perturbator could force the run to always take that branch, and would win the game.

that Controller has a winning strategy in G δ (A) for the objective B. When this holds, we say that Controller wins the robust timed game for A, and otherwise that Perturbator does. Note that these games are determined since for each δ > 0, the semantics is a timed game.

Figure 1 shows examples of timed automata where either Controller or Perturbator wins the robust timed game according to our definitions. The main result of this paper for this non-stochastic setting is the following.

Theorem 1. The robust timed game problem is EXPTIME-complete. EXPTIME-hardness is proved in Appendix D. We focus on presenting the EXPTIME membership in Sections 4 and 5. The algorithm relies on a characterization of winning strategies in a refinement of the region automaton construction.

In order to formally introduce the appropriate notions for this characterization, we need definitions given in the following section.

Regions, Orbit Graphs and Shrunk DBMs

Regions and Region Automata. Following [START_REF] De Wulf | Robust safety of timed automata[END_REF][START_REF] Puri | Dynamical properties of timed automata[END_REF]3], we assume that the clocks are bounded above by a known constant4 in all timed automata we consider. Fix a timed automaton A = (L, C, ℓ 0 , Act, E). We define regions as in [1], as subsets of R C ≥0 . Any region r is defined by fixing the integer parts of the clocks, and giving a partition X 0 , X 1 , . . . , X m of the clocks, ordered according to their fractional values: for any ν ∈ r, 0 = frac(ν(x 0 )) < frac(ν(x 1 )) < . . . < frac(ν(x m )) for any x 0 ∈ X 0 , . . . , x m ∈ X m , and frac(ν(x)) = frac(ν(y)) for any x, y ∈ X i . Here, X i = ∅ for all 1 ≤ i ≤ m but X 0 might be empty. For any valuation ν, let [ν] denote the region to which ν belongs. Reg(A) denotes the set of regions of A. A region r is said to be non-punctual if it contains some ν ∈ r such that ν + [-ε, ε] ⊆ r for some ε > 0. It is said punctual otherwise. By extension, we say that (ℓ, r) is non-punctual if r is.

We define the region automaton as a finite automaton R(A) whose states are pairs (ℓ, r) where ℓ ∈ L and r is a region. Given (r ′ , a) ∈ Reg(A) × Act, there is a transition (ℓ, r) 5 , there exist ν ∈ r, ν ′ ∈ r ′ and d > 0 such that ν ′ = ν + d, and there is an edge e = (ℓ, g, R, ℓ ′ ) such that r ′ |= g and r ′ [R ← 0] = s. We write the paths of the region automaton as π = q 1 e 1 q 2 e 2 . . . q n where each q i is a state, and e i ∈ Reg(A) × Act, such that q i ei -→ q i+1 for all 1 ≤ i ≤ n -1. The length of the path is n, and is denoted by |π|. If a Büchi condition B is given, a cycle of the region automaton is winning if it contains an occurrence of a state (ℓ, r) with ℓ ∈ B. Vertices and Orbit Graphs. A vertex of a region r is any point of r ∩ N C , where r denotes the topological closure of r. Let V(r) denote the set of vertices of r. We also extend this definition to V((ℓ, r)) = V(r).

(r ′ ,a) ---→ (ℓ ′ , s) if r ′ is non-punctual
With any path π of the region automaton, we associate a labeled bipartite graph Γ (π) called the folded orbit graph of π [START_REF] Puri | Dynamical properties of timed automata[END_REF] (FOG for short). Intuitively, the FOG of a path gives the reachability relation between the vertices of the first and the last regions, assuming the guards are closed. For any path π from state q to q ′ , the node set of the graph Γ (π) is defined as the disjoint union of V(q) and V(q ′ ). There is an edge from v ∈ V(q) to v ′ ∈ V(q ′ ), if, and only if v ′ is reachable from v along the path π when all guards are replaced by their closed counterparts. It was shown that any run along π can be written as a convex combination of runs along vertices; using this observation orbit graphs can be used to characterize runs along given paths [START_REF] Puri | Dynamical properties of timed automata[END_REF]. An important property that we will use is that there is a monoid morphism from paths to orbit graphs. In fact, the orbit graph of a path can be obtained by combining the orbit graphs of a factorization of the path.

When the path π is a cycle around q, then Γ (π) is defined on the node set V(q), by merging the nodes of the bipartite graph corresponding to the same vertex. A cycle π is aperiodic if for all k ≥ 1, Γ (π k ) is strongly connected. Aperiodic cycles are closely related to cycles whose FOG is a complete graph since a long enough iteration of the former gives a complete FOG and conversely, any cycle that has some power with a complete FOG is aperiodic (Appendix B Lemma 21). In the timed automaton of Fig. 1(b), the cycles around locations ℓ 2 and ℓ 3 are aperiodic while that of ℓ 1 is not. Appendix A contains examples. Complete FOG are of particular interest to us as they exactly correspond to paths whose reachability relation (between valuations of the initial and last region) is complete [3]. This means that there is no convergence phenomena along the path. DBMs and shrunk DBMs. We assume the reader is familiar with the data structure of difference-bound matrix (DBM) which are square matrices over (R × {<, ≤}) ∪ {(∞, <)} used to represent zones. DBMs were introduced in [6,[START_REF] David | Timing assumptions and verification of finite-state concurrent systems[END_REF] for analyzing timed automata; see also [5]. Standard operations used to explore the state space of timed automata have been defined on DBMs: intersection is written M ∩ N , Pre (M ) is the set of time predecessors of M , Unreset R (M ) is the set of valuations that end in M when the clocks in R are reset. We also consider Pre >δ (M ), time predecessors with a delay of more than δ.

x y

= Pre      x y      Fig. 2.
Time-predecessors operation (M, P ) = Pre(N, Q) applied on a shrunk DBM. Here, the shaded area on the left represents the set M -δP , while the zone with the thick contour represents M .

To analyze the parametric game G δ (A), we need to express shrinkings of zones, e.g. sets of states satisfying constraints of the form g = 1 + δ < x < 2δ ∧ 2δ < y, where δ is a parameter. Formally, a shrunk DBM is a pair (M, P ), where M is a DBM, and P is a nonnegative integer matrix called a shrinking matrix (SM). This pair represents the set of valuations defined by the DBM M -δP , for any δ > 0. For instance, M is the guard g obtained by setting δ = 0, and P is made of the integer multipliers of δ.

We adopt the following notation: when we write a statement involving a shrunk DBM (M, P ), we mean that for some δ 0 > 0, the statement holds for (M -δP ) for all δ ∈ [0, δ 0 ]. For instance, (M, P ) = Pre >δ (N, Q) means that M -δP = Pre >δ (N -δQ) for all small enough δ > 0. Additional operations are defined for shrunk DBMs: for any (M, P ), we define shrink [-δ,δ] (M, P ) as the set of valuations ν with ν + [-δ, δ] ⊆ M -δP , for small enough δ > 0. Figure 2 shows an example of a shrunk DBM and an operation applied on it. Standard operations on zones can also be performed on shrunk DBMs in poly-time [START_REF] Sankur | Shrinking timed automata[END_REF]8].

Playing in the Region Automaton

In this section, we will define an appropriate abstraction based on region automata in order to characterize winning in the robust timed game. We note that the usual region automaton does not carry enough information for our purpose; for instance, the blocking behavior in Fig. 1(a) cannot be detected in the region automaton (which does contain infinite runs). We therefore define, on top of the usual region construction, a complex winning condition W characterizing accepting runs along aperiodic cycles. In order to be able to transfer the condition W to the continuous semantics, we study the properties of W on the abstract region game, and derive two necessary and sufficient conditions (C C and C P ) for winning which will be used in the next section to derive the algorithm. Abstract Arena and Strategies We fix a timed automaton A = (L, C, ℓ 0 , Act, E) and a Büchi condition φ. We define a two-player turn-based game played on the region automaton R(A). In this game, Controller's strategy consists in choosing actions, while Perturbator's strategy consists in resolving non-determinism.

We consider standard notions of (finite-memory, memoryless) strategies in this game and, given a finite-memory strategy σ, we denote by R(A)[σ] the automaton obtained under strategy σ. Winning Condition on R(A) We define set W of winning plays in the game R(A): an infinite play is winning iff the following two conditions are satisfied: 1) an accepting state in φ is visited infinitely often 2) disjoint finite factors with complete folded orbit graphs are visited infinitely often.

Proposition 2. The game (R(A), W) is determined, admits finite-memory strategies for both players, and wining strategies can be computed in EXPTIME.

The above proposition is proved by showing that condition 2) of W can be rewritten as a Büchi condition: the set of folded orbit graphs constitute a finite monoid (of exponential size) which can be used to build a Büchi automaton encoding condition 2). Using a product construction for Büchi automata, one can define a Büchi game of exponential size where winning for any player is equivalent to winning in (R(A), W). See Appendix B.

From the abstract game to the robust timed game We introduce two conditions for Perturbator and Controller which are used in Section 5 to build concrete strategies in the robust timed game.

C P : there exists a finite memory strategy τ for Perturbator such that no cycle in R(A)[τ ] reachable from the initial state is winning aperiodic. C C : there exists a finite-memory strategy σ for Controller such that every cycle in R(A)[σ] reachable from the initial state is winning aperiodic.

Intuitively, determinacy allows us to write that either all cycles are aperiodic, or none is, respectively under each player's winning strategies. We prove that these properties are sufficient and necessary for respective players to win (R(A), W): The proof is obtained by the following facts: finite-memory strategies are sufficient to win the game (R(A), W), thanks to the previous proposition; given a folded orbit graph γ, there exists n such that γ n is complete iff γ is aperiodic; last, the concatenation of a complete FOG with an arbitrary FOG is complete.

Lemma 3.

Solving the Robust Timed Game

In this section, we show that condition C P (resp. C C ) is sufficient to witness the existence of a winning strategy in the robust timed game for Perturbator (resp. Controller). By Lemma 3, the robust timed game problem is then reduced to (R(A), W) and we obtain: Theorem 4. Let A be a timed automaton with a Büchi condition. Then, Controller wins the robust timed game for A iff he wins the game (R(A), W).

By Proposition 2, the robust timed game can be solved in EXPTIME. In addition, when Controller wins the robust timed game, one can also compute δ > 0 and an actual strategy in G δ (A): Lemma 3 gives an effective strategy σ satisfying C C and the proof of Lemma 6 will effectively derive a strategy (given as shrunk DBMs).

Sufficient condition for Perturbator

We first prove that under condition C P , Perturbator wins the robust timed game. We use the following observations. Once one fixes a strategy for Perturbator satisfying C P , intuitively, one obtains a timed automaton (where there is no more non-determinism in actions), such that all accepting cycles are non-aperiodic. As Perturbator has no more non-determinism to resolve, results of [START_REF] Sankur | Robust controller synthesis in timed automata[END_REF] apply and the next lemma follows (see Appendix C). Lemma 5. If C P holds, then Perturbator wins the robust timed game.

Sufficient condition for Controller

Proving that C C is a sufficient condition for Controller is the main difficulty in the paper; the proof for the next lemma is given in this section. Lemma 6. If C C holds, then Controller wins the robust timed game.

Proof outline. We consider the non-deterministic automaton B = R(A)[σ] which represents the behavior of game R(A) when Controller plays according to σ, given by condition C C . Without loss of generality, we assume that σ is a memoryless strategy played on the game R(A)[σ] (states of R(A) can be augmented with memory) and that B is trim. Given an edge e = q → q ′ of B, we denote by edge(e) the underlying transition in A.

Given a state p of B, we denote by Unfold(B, p) the infinite labeled tree obtained as the unfolding of B, rooted in state p. Formally, nodes are labeled by states of B and given a node x labeled by q, σ(q) is defined and there exists q ′ such that q σ(q) ---→ q ′ in B. Then x has one child node for each such q ′ . We may abusively use nodes to refer to labels to simplify notations.

We first choose states q 1 , . . . , q n such that every cycle of B contains one of the q i 's. Let us denote by q 0 the initial state of B, for i = 0..n, one can choose a finite prefix t i of Unfold(B, q i ) such that every leaf of t i is labeled by some q j , j = 1..n. Indeed, as B is trim and σ is a winning strategy for Controller in the game (R(A), W), every branch of Unfold(B, q i ) is infinite. Strategies for standard timed games can be described by means of regions. In our robustness setting, we use shrinkings of regions. Let (ℓ i , r i ) be the label of state q i . To build a strategy for Controller, we will identify δ > 0 and zones s i , i = 1..n, obtained as shrinking of regions r i . These zones satisfy that the controllable predecessors through the tree t i computed with zones (s j ) j at leafs contains the zone s i : this means that from any configuration in (ℓ i , s i ), Controller has a strategy to ensure reaching a configuration in one of the (ℓ j , s j )'s, when following the tree t i . These strategies can thus be repeated, yielding infinite outcomes. This idea is illustrated in Fig. 3 where the computations along some prefix t are depicted: the shrunk zone at a node represents the controllable predecessors of the shrunk zones of its children. Here, from the shrunk set of the root node, one can ensure reaching a shrinking of each leaf which is included in the shrinking of the starting state of its cycle, yielding a kind of fixpoint. We have in fact (r, Q i ) ⊆ (r, Q 1 ) for i = 3, 4, and (s,

(r, Q 1 ) (r, Q 3 ) (r, Q 4 ) (s, Q 5 ) (s, Q 2 ) (t, Q 6 )
Q 5 ) ⊆ (s, Q 2 ).
To identify these zones s i , we will successively prove the three following facts: 1) Prefixes t i 's can be chosen such that every branch has a complete FOG 2) Controllable predecessors through t i 's of non-empty shrunk zones are nonempty shrunk zones 3) Controllable predecessors through t i 's can be faithfully over-approximated by the intersection of controllable predecessors through branches of t i Ensuring branches with complete FOGs. To prove property 1) of the Proof outline, we use condition C C and the fact that long enough repetitions of aperiodic cycles yield complete FOGs. We obtain: Lemma 7. Under condition C C , there exists an integer N such that every path ρ in B of length at least N has a complete folded orbit graph.

Controllable Predecessors and Merge. In order to compute winning states in G δ (A) through unfoldings, we define two operators. CPre is the standard set of controllable predecessors along a single edge: Definition 8 (Operator CPre). Let e = q → q 1 be an edge in some unfolding of B. Let us write q = (ℓ, r), q 1 = (ℓ 1 , r 1 ), σ(q) = (r ′ , a) and edge(q

→ q 1 ) = (ℓ, g 1 , a, R 1 , ℓ 1 ). Let M 1 be a DBM such that M 1 ⊆ r 1 and δ ≥ 0. We define the set of δ-controllable predecessors of M 1 through edge e as CPre δ e (M 1 ) = r ∩ Pre >δ Shrink [-δ,δ] (r ′ ∩ Unreset R1 (M 1 )) .
The above definition is extended to paths. Intuitively, CPre δ e (M 1 ) are the valuations in region r from which M 1 can be surely reached through a delay in r ′ and the edge e despite perturbations up to δ.

We now consider the case of branching paths, where Perturbator resolves non-determinism. In this case, in order for Controller to ensure reaching given subsets in all branches, one needs a stronger operator, which we call CMerge. Intuitively, CMerge δ e1,e2 (M 1 , M 2 ) is the set of valuations in the region starting r from which Controller can ensure reaching either M 1 or M 2 by a single strategy, whatever Perturbator's strategy is. The operator is illustrated in Fig. 4.

Definition 9 (Operator CMerge). Let e 1 = q → q 1 and e 2 = q → q 2 be edges in some unfolding of B, and write q = (ℓ, r), σ(q) = (r ′ , a) and for i ∈ {1, 2},

q i = (ℓ i , r i ), edge(q → q i ) = (ℓ, g i , a, R i , ℓ i ). Let M i be a DBM such that M i ⊆ r i for i ∈ {1, 2}. For any δ ≥ 0, define the set of δ-controllable predecessors of M 1 , M 2 through edges e 1 , e 2 as CMerge δ e1,e2 (M 1 , M 2 ) = r ∩ Pre >δ Shrink [-δ,δ] r ′ ∩ i∈{1,2} Unreset Ri (M i ) .
We extend CMerge by induction to finite prefixes of unfoldings of B (see Appendix C.2). Informally, consider a tree t and shrunk DBMs (M i , P i ) i for its leaves, CMerge δ t (M i , P i ) i is the set of states for which there is a strategy ensuring reaching one of (M i , P i ). It should be clear that because CMerge δ e1,e2 is more restrictive than CPre δ e1 ∩ CPre δ e2 , we always have CMerge δ t ⊆ β CPre δ β , where β ranges over all branches of t (See Fig. 4).

The following lemma states property 2) of the proof outline. Existence of the SM Q follows from standard results on shrunk DBMs. Non-emptiness of (M, Q) follows from the fact that every delay edge leads to a non-punctual region. Define a full-dimensional subset of a set r ⊆ R n is a subset r ′ ⊆ r such that there is ν ∈ r ′ and ε > 0 satisfying Ball d∞ (ν, ε) ∩ r ⊆ r ′ , where Ball d∞ (ν, ε) is the standard ball of radius ε for the infinity norm on R n . Lemma 10. Let t be a finite prefix of Unfold(B, q), r the region labeling the root, and r 1 , . . . , r k those of the leafs. M, N 1 , . . . , N k be non-empty DBMs that are full dimensional subsets of r, r 1 , . . . , r k satisfying M = CMerge 0 t ((N j ) j ). We consider shrinking matrices

P j , 1 ≤ j ≤ k, of DBM N j such that (N j , P j ) = ∅. Then, there exists a SM Q such that (M, Q) = CMerge δ t ((N j , P j ) j ), and (M, Q) = ∅. x y r r ′ r2, P2 r1, P1 s Fig. 4.
We have s = CMerge 0 ((ri, Pi)i), which is strictly included in ∩iCPre 0 (ri, Pi) but has the same shape.

Over-Approximation of CMerge. Given a prefix t where each branch β i ends in a leaf labeled with (r i , P i ), we see ∩ βi CPre 0 βi ((r i , P i )) as an over-approximation of CMerge 0 t ((r i , P i ) i ). We will show that both sets have the same "shape", i.e. any facet that is not shrunk in one set, is not shrunk in the other one. This is illustrated in Fig. 4.

We introduce the notion of 0-dominance as follows: for a pair of SMs P, Q, Q 0-dominates P , written

P 0 Q, if Q[i, j] ≤ P [i, j],
and Q[i, j] = 0 implies P [i, j] = 0 for all i, j. Informally, a set shrunk by P is smaller than that shrunk by Q, but yields the same shape. The 0-dominance is the notion we use for a "precise" over-approximation of CMerge: (see Appendix C.3) Lemma 11. Let t be a finite prefix of Unfold(B, q), with q = (ℓ, r), and let (ℓ i , r i ), 1 ≤ i ≤ k denote the (labels of ) leafs of t. We denote by

β i , 1 ≤ i ≤ k, the branches of t. Consider SMs P i , 1 ≤ i ≤ k, for regions r i . Let us denote (r, P ) = CMerge 0 t ((r i , P i ) 1≤i≤k ) and (r, Q) = k i=1 CPre 0 βi (r i , P i ), then P 0 Q.
Putting everything together. In order to complete the proof of Lemma 6, we first recall the following simple lemma:

Lemma 12 ([21]

). For any DBM M , there is a SM P 0 s.t. (M, P 0 ) = ∅, and is fully dimensional, and for any SM P and ε>0 with (M, P ) = ∅ and M -εP 0 = ∅, we have M -εP 0 ⊆ (M, P ).

Remember we have identified states q i and trees t i , i = 0..n. Denote (ℓ i , r i ) the label of q i . For each i = 1..n, we denote by P i the SM obtained by Lemma 12 for r i . Consider now some tree t i , i = 0..n, with ((r j , P j ) j ) at leafs. Let β j be a branch of t i and denote by (r j , P j ) its leaf. By Lemma 7, the FOG of β j is complete, and thus from any valuation in r i , one can reach every valuation in the target region r j along β j (see [3]), and thus r i = CPre 0 βj (r j , P j ). This holds for every branch and we obtain r i = j CPre 0 βj (r j , P j ). By Lemma 11, this entails r i = CMerge 0 ti ((r j , P j ) j ). We can choose ε > 0 small enough such that the zone s i = r i -εP i is non-empty for every i = 1..n and we obtain r i = CMerge 0 ti ((s j ) j ). We can then apply Lemma 10, yielding some SM

Q i of r i such that ∅ = (r i , Q i ) = CMerge δ ti ((s j ) j ).
There are two cases: -i = 0: as r 0 is the singleton {0}, we have (r 0 , Q 0 ) = r 0 , and thus r 0 = CMerge δ t0 ((s j ) j ). In other terms, for small enough δ's, Controller has a strategy in G δ (A) along t 0 to reach one of the (ℓ j , s j )'s starting from the initial configuration (ℓ 0 , 0). -i ≥ 1: Lemma 12 entails s i ⊆ CMerge δ ti ((s j ) j ), which precisely states that for small enough δ's, Controller has a strategy in G δ (A) along t i , starting in (ℓ i , s i ), to reach one of the (ℓ j , s j )'s.

These strategies can thus be combined and repeated, yielding the result.

Probabilistic Semantics

In some systems, considering the environment as a completely adversarial opponent is too strong an assumption. In order to model the environment with more realistic behavior, we define two semantics as probabilistic variants of the robust timed games. The first variant is the stochastic game semantics where Perturbator only resolves the non-determinism in actions, but the perturbations are chosen independently and uniformly at random in the interval [-δ, δ]. The second semantics is the Markov decision process semantics (MDP for short), where the non-determinism is also resolved by a uniform distribution on the edges. Note that there is no player Perturbator in the latter semantics.

Stochastic Game Semantics

Formally, given δ > 0, the state space is partitioned into V C ∪ V P as previously. At each step, Controller picks a delay d ≥ δ, and an action a such that for every edge e = (ℓ, g, a, R, ℓ ′ ) such that ν + d |= g, we have ν

+ d + ε |= g for all ε ∈ [-δ, δ],
and there exists at least one such edge e. Perturbator then chooses an edge e with label a, and a perturbation ε ∈ [-δ, δ] is chosen independently and uniformly at random. The next state is determined by delaying d + ε and taking the edge e. To ensure that probability measures exist, we restrict to measurable strategies.

In this semantics, we are interested in deciding whether Controller can ensure a given Büchi objective almost surely, for some δ > 0. It turns out that the same characterization as in Theorem 4 holds in the probabilistic case. This is a powerful result showing a strong distinction between robust and nonrobust timed games: in the first case, a controller that ensures the specification almost surely can be computed, while in non-robust timed games, any controller will fail almost surely. Thus, while in previous works on robustness in timed automata (e.g. [START_REF] Puri | Dynamical properties of timed automata[END_REF]) the emphasis was on additional behaviors that might appear in the worst-case due to the accumulation of perturbations, we show that in our setting, this is inevitable. Note that this also shows that limit-sure winning (see next section) is equivalent to almost-sure winning.

Markov decision process semantics

The Markov decision process semantics consists in choosing both the perturbations, and the edges uniformly at random (and independently). Formally, it consists in restricting Perturbator to choose all possible edges uniformly at random in the stochastic game semantics. We denote by G MDP δ (A) the resulting game, and P σ G MDP δ (A),s the probability measure on Runs(A, s) under strategy σ. For a given timed Büchi automaton, denote φ the set of accepting runs. We are interested in the two following problems: (we let s 0 = (ℓ 0 , 0)) Almost-sure winning: does there exist δ > 0 and a strategy σ for Controller such that P σ G MDP δ (A),s0 (φ) = 1? Limit-sure winning: does there exist, for every 0 ≤ ε ≤ 1, a perturbation upper bound δ, and a strategy σ for Controller such that P σ

G MDP δ (A),s0 (φ) ≥ 1 -ε? ℓ 0 ℓ 1 x≤1,a,x:=0 x≤1,a
x≤1,a,x:=0 Fig. 5. This automaton is losing in the MDP semantics for the almost-sure winning but winning under the same semantics for the limit-sure winning.

In fact, a blocking state (ℓ0, x) with x > 1δ is reachable with positive probability for any δ.

Observe that if almost-sure winning cannot be ensured, then limit-sure winning still has a concrete interpretation in terms of controller synthesis: given a quantitative constraint on the quality of the controller, what should be the precision on clocks measurements to be able to synthesize a correct controller? Consider the timed automaton depicted on the right. It is easy to see that Controller loses the (non-stochastic) robust game, the stochastic game and in the MDP semantics with almost-sure condition, but he wins in the MDP semantics with limit-sure condition.

Theorem 14. It is EXPTIME-complete to decide whether Controller wins almost-surely (resp. limitsurely) in the MDP semantics of a timed Büchi automaton.

To prove this theorem, we will define decidable characterizations on R(A) which we will see as a finite Markov decision process. In this MDP, the nondeterminism of actions is resolved according to a uniform distribution. Given a strategy σ for Controller and a state v, we denote by P σ R(A),v the resulting measure on Runs(R(A), v). The initial state of R(A) is v 0 . We will use well-known notions about finite MDPs; we refer to [START_REF] Putterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF].

Almost-sure winning We introduce the following winning condition Intuitively, the first condition is required to ensure winning almost-surely, and the second condition allows to forbid blocking behaviors. Notice the resemblance with condition W; the difference is that φ only needs to be ensured almost-surely rather than surely. We prove the decidability of this condition.

W ′ : a Controller's strategy σ in R(A) is winning in state v iff P σ R(A),v (φ) =
Lemma 16. The game (R(A), W ′ ) admits finite-memory strategies, and winning strategies can be computed in EXPTIME.

The proof of Prop. 15 uses the following ideas. We first assume that Controller wins the abstract game using some strategy σ. We derive from σ a strategy σ in the MDP semantics by concretizing the delays chosen by σ. To do so, we consider the automaton R(A)[σ] and proceed as in Section 5, which results in a strategy defined by means of shrinking matrices. Using the results of Section 5, we can prove that the outcomes of σ are never blocked, and thus the probabilities of paths in R(A) under σ are preserved by σ. As a consequence, σ wins almost-surely.

Conversely, by contradiction, we assume that Controller does not satisfy W ′ in R(A) while there exists an almost-sure strategy σ for the MDP semantics. We build from σ a strategy σ in R(A), and prove that it satisfies φ almost-surely. This entails the existence of a run ρ in R(A)[σ] such that ρ eventually does not contain factors with a complete FOG. We finally show that, with positive probability, perturbations can be chosen to ensure that the run gets blocked along a finite prefix of this path, Lemma 43), which ensures that σ is not almost-surely winning.

Limit-sure winning As illustrated in Fig. 5, it is sometimes possible, according to any ε > 0, to choose the parameter δ > 0 small enough to ensure a winning probability of at least 1ε. The idea is that in such cases one can ensure reaching the set of almost-sure winning states with arbitrarily high probability, although the run can still be blocked with a small probability before reaching this set.

To characterize limit-sure winning, we define a new condition W ′′ as follows. If Win ′ denotes the set of winning states for Controller in the game (R(A), W ′ ), then W ′′ is defined as the set of states from which one can almost surely reach Win ′ . Proposition 17. Controller wins limit-surely in the MDP semantics of a timed Büchi automaton A from s 0 iff Controller wins the game (R(A), W ′′ ) in v 0 .

The proof of this proposition relies on the following lemma, and uses techniques similar as those introduced to prove Proposition 15.

Lemma 18. The game (R(A), W ′′ ) admits finite-memory strategies, and winning strategies can be computed in EXPTIME.

Conclusion

In this paper, we defined robust timed games with Büchi conditions and unknown imprecision parameters. Our formalism allows one to solve robust controller synthesis problems both against an adversarial (or worst-case) environment, and two variants of probabilistic environments. The procedures we have developed allow, when they exist, to effectively build a bound δ > 0 on the perturbation and a winning strategy for Controller. Some questions remain open including the generalization of these results to concurrent timed games with parity conditions considered in [11]. We believe it is possible to derive symbolic algorithms but this will require extending the theory to detect aperiodic cycles in zone graphs rather than in the region graph.

A Orbit Graphs

We start with some complements on the region automaton R(A). We may sometimes decompose edges (ℓ, r) ---→ (ℓ ′ , s) of R(A). This representation of edges in R(A) is thus more precise. We will use it in the appendices.

Using this notation, given a run ρ = p 1 e 1 p 2 e 2 . . . p n of A with e i ∈ R >0 ∪ E, its projection on regions is the path π = q 1 e ′ 1 q 2 e ′ 2 . . . q n in the region automaton s.t. p i ∈ q i , and e ′ i = e i if e i ∈ E and e ′ i = ∆ otherwise.

y 0 x 1 1 2 2 ℓ 1 ∆ y 0 x 1 1 2 2 ℓ 1 e 1 y 0 x 1 1 2 2 ℓ 2 ∆ y 0 x 1 1 2 2 ℓ 2 e 2 y 0 x 1 1 2 2 ℓ 1 ∆ y 0 x 1 1 2 2 ℓ 1
Fig. 6. The orbit graph of a (cyclic) path in the region automaton of the automaton of Fig. 1(a). With any path π of the region automaton, we associate a labeled bipartite graph Γ (π) called the folded orbit graph of π [8] (FOG for short). Intuitively, the FOG of a path gives the reachability relation between the vertices of the first and last regions. Formally, for a transition τ = q 1 e 1 q 2 , its orbit graph

Γ (τ ) = (V 1 ∪ V 2 , (q 1 , q 2 ), E) is a bipartite graph where V 1 = {(1, v)} v∈V(q1) , and V 2 = {(2, v)} v∈V(q2) . For any (1, u), (2, v) ∈ V 1 × V 2 , we have an edge ((1, u), (2, v)) ∈ E, if,

and only if u ē1

-→ v, where e 1 = ∆ if e 1 = ∆, and otherwise e 1 is obtained by replacing the guard by its closed counterpart. Note that each vertex has at least one successor through e 1 [1]. In order to extend Γ (•) to paths, we use a composition operator ⊕ between FOGs, defined as follows.

If G = (V 1 ∪ V 2 , (q 1 , q 2 ), E) and G ′ = (V ′ 1 ∪ V ′ 2 , (q ′ 1 , q ′ 2 ), E ′ ) denote two FOGs, then G ⊕ G ′ is defined if, and only if, q 2 = q ′
1 , that is, when the path defining the former graph ends in the first state of the path defining the latter graph. In this case, the graph

G ′′ = G ⊕ G ′ = (V 1 ∪ . . . V ′ 2 , (q 1 , q ′ 2 ), E ′′
) is defined by taking the disjoint union of G and G ′ , merging each node (2, v) of V 2 with the node (1, v) of V ′ 1 . Now, we extend Γ (•) to paths by induction, as follows. Consider any path π = q 1 e 1 . . . q n-1 e n-1 q n , and let G = (V 1 ∪ V 2 , (q 1 , q n-1 ), E) be the FOG Γ (q 1 e 1 . . . q n-1 ), given by induction. Let G ′ = (U ∪ U ′ , (q n-1 , q n ), E ′ ) denote the bipartite graph of q n-1 e n-1 q n . Then, we let Γ (π) = G ⊕ G ′ . If the given path π = q 1 . . . q 1 is a cycle, then we define Γ (π) on the node set V(q 1 ), by merging the nodes of the bipartite graph corresponding to the same vertex. Note that delays of duration zero are allowed when defining orbit graphs. Figure 6 displays a path in the region automaton of the automaton depicted on Fig. 1(a). Figure 7 shows the FOG of this path.

Orbit graphs are used to characterize runs along a given path on regions:

Lemma 19 ( [8]). Let π be a path from region r to s. Consider any ν ∈ r with ν = v∈V(r) λ v v for some coefficients λ v ≥ 0 and

λ v = 1. If ν π -→ ν ′ , then
for each v ∈ V(r), there exists a probability distribution

{p ν,ν ′ v,w } w∈R Γ (π) (v) over R Γ (π) (v) such that ν ′ = v∈V(r) λ v w∈R Γ (π) (v) p ν,ν ′ v,w w. 6
B Proofs of Section 4 (Playing in the Region Automaton)

In order to prepare the proof of Prop. 2, we first construct a deterministic Büchi automaton B recognizing runs of R(A) that contain an infinite number of disjoint factors with complete FOGs.

The goal of B is to take track of the current folded orbit graph, and recognize complete orbit graphs. The state space contains all G and triples (G, a, r) where G ranges over all folded orbit graphs of A, r is a region, and a a label. The size of the state space is thus bounded by an exponential (see Section 3); the initial state is Γ (∅) (that is, the graph of the identity relation). Informally, the transitions implement the operation ⊕ on the monoid of folded orbit graphs. More precisely, we have G a,r ′ --→ (G, a, r ′ ), and (G, a, r ′ ) e -→ (G ⊕ Γ ((ℓ, r)∆(ℓ, r ′ )e(ℓ ′ , s))), where (ℓ, r)∆(ℓ, r ′ )e(ℓ ′ , s) is the path generated by delaying to r ′ and taking the edge e. More precisely, if we write e = (ℓ, g, a, R, ℓ ′ ), then s = r ′ [R ← 0]. All states G such that G is a complete FOG are accepting. Furthermore, from any such accepting state G, we remove the previously defined outgoing edges, and add the edges G a,r ′ --→ (Γ (∅), a, r ′ ). Hence, the automaton tracks the FOG of the current factor it is reading, and reinitializes the FOG when it visits a complete graph. Note that B is a deterministic Büchi automaton.

Lemma 20. Given any timed automaton A, the Büchi automaton B constructed as above is deterministic and recognizes the set of runs of R(A) that contain an infinite number of disjoint factors with complete FOGs. Proposition 2. The game (R(A), W) is determined, admits finite-memory strategies for both players, and wining strategies can be computed in EXPTIME.

Proof. We first define a game B 1 as a slight modification of R(A) where the moves of both players are made explicit, in order to allow parallel composition with the automaton B we just defined. Given a timed automaton A = (L, C, ℓ 0 , Σ, E) and a Büchi condition B, the state space of B 1 is defined as Player 1 states (ℓ, r) and Player 2 states (ℓ, r, r ′ , a), where ℓ is a location, r and r ′ regions, and a a label of A. The labels of B 1 are either pairs (r, a) where r is a region, and a is the label of an action, or edges e ∈ E. The transitions are defined as follows. We have (ℓ, r)

(r ′ ,a) ---→ (ℓ, r, r ′ , a) iff (ℓ, r) (r ′ ,a)
---→ (ℓ ′ , s) in R(A) for some state (ℓ ′ , s). For any edge e = (ℓ, g, a, R, ℓ ′ ) with label a, such that g is satisfied by r ′ , we let (ℓ, r, r ′ , a) e -→ (ℓ ′ , s) where s = r ′ [R ← 0]. Hence, these transitions "simulate" those of R(A) while the moves of both players are made visible at intermediate states. As before, the accepting states are (ℓ, r) such that ℓ ∈ B. The initial state is {(ℓ 0 , r 0 )}. Now, let B B 1 denote the parallel composition of B 1 and B endowed with the generalized Büchi condition given by the conditions of the two automata. We already noted that B 1 simply visits the region automaton given moves by both players, and that given the same path, B keeps track of the orbit graph of the factors. We see B B 1 as a game where any state with a Player 1 component in B 1 is a Player 1 state. It is now clear that any winning strategy for (R(A), W) can be translated into a winning strategy in B B 1 and conversely. We know that in B B 1 , 1-bit memory strategies are sufficient to win. Given such a strategy, one can derive a strategy for B 1 by seeing B as the memory (thanks to the fact that it is deterministic). This provides a winning strategy for (R(A), W) with at most exponential memory.

Note that the equivalence with a Büchi game means that the game is determined.

⊓ ⊔

In order to prepare the proof of Lemma 3, we need a couple of results proven in previous works.

The following lemma explains the relation between aperiodic cycles and cycles with complete orbit graphs.

Lemma 21. If π is an aperiodic cycle, then Γ (π n ) is a complete graph for all n ≥ |C 0 | × |C 0 |!. Conversely, if π is a cycle such that Γ (π n ) is a complete graph for some n ≥ 1, then π is aperiodic.
Proof. For the direct implication, Lemma 13 in [11] actually states that Γ (π n ) is complete for some n ≤ |C 0 | × |C 0 |!. To conclude, it suffices to observe that the (left or right) concatenation of a complete folded orbit graph with any folded orbit graph is still complete. Conversely, first note that if Γ (π n ) is complete for some n, then it is also complete for any n ′ ≥ n. Suppose that π is not aperiodic, then there exists k such that the graph Γ (π k ) is not strongly connected. But then Γ (π ki ) is also not strongly connected, for any i ≥ 1. Contradiction.

⊓ ⊔

The following lemma is a factorization lemma à la Ramsey. Although Ramsey's theorem can be used to prove it, better bounds were obtained in [11].

Lemma 22 ( [11]). Let π be a path of R(A) written as π = π 0 π 1 π 2 . . . π n where each π i is a cycle that starts in the same state, for i ≥ 1. Then, one can write

π = π ′ 0 π ′ 1 π ′ 2 . . . π ′ m+1 such that m ≥ n/r -2 -1
, where r = 2 (|C|+1) 2 |R(A)|, and for some indices 0 = α 0 < α 1 < . . ., we have π

′ i = π αi • . . . • π αi+1-1 for each i ≥ 0, and Γ (π ′ 1 ) = Γ (π ′ i ) for all 1 ≤ i ≤ m.
Once a strategy σ for Controller is fixed and a strategy τ for Perturbator is fixed, this defines a unique play ρ in R(A). We say that ρ is consistent with the couple (σ, τ ). Lemma 3. The winning condition W is equivalent to C P and C C : 1. Perturbator wins the game (R(A), W) iff property C P holds. 2. Controller wins the game (R(A), W) iff property C C holds. In both cases, a winning strategy for W is also a witness for C C (resp. C P ).

Proof (Proof of Lemma 3).

1. We start by showing the direct implication. Assuming Perturbator wins the game (R(A), W), we know by Proposition 2, that there exists a winning finite-memory strategy τ for Perturbator. Let us show that condition C P holds. Assume towards a contradiction that there exists a reachable winning aperiodic cycle in R(A)[τ ]. Denote by π such a cycle. This means that Controller has a strategy σ to eventually reach π and repeat π forever. Since π is aperiodic, for some n, we know that Γ (π n ) is a complete graph (Lemma 21). Thus, the play consistent with (σ, τ ) that starts in (ℓ 0 , r 0 ) belongs to W, a contradiction. We show the converse implication. Assume that C P holds and let us prove that Perturbator wins the game (R(A), W). Let τ be the finite memory strategy given by C P . By contradiction, suppose that there exists a strategy σ for Controller such that the play ρ consistent with the couple of strategies (σ, τ ) starting in (ℓ 0 , r 0 ) belongs to W. ρ is a run in the automaton R(A)[τ ], and therefore one can factorize ρ into ρ 0 ρ 1 • • • such that ρ i for any i > 0 is a cycle in R(A)[τ ] around a same state. Now, as ρ is accepting and there are finitely many folded orbit graphs, one can use a Lemma 22 to factor

ρ 1 ρ 2 • • • into ρ ′ 1 ρ ′ 2 • • • such that ρ ′
i is an accepting cycle around a same state for i > 0, and

Γ (ρ ′ 1 ) = Γ (ρ ′ 2 ) = • • • = γ.
Since C P holds, γ is not aperiodic. As ρ ∈ W, there exist i < j such that ρ ′ i • • • ρ ′ j contains a factor with a complete FOG. Then we have that Γ (ρ ′ i • • • ρ ′ j ) = γ j-i+1 is complete, contradiction, as γ is not aperiodic (Lemma 21). 2. Direct implication. Assume that Controller wins in (R(A), W) and let us show that C C holds. By Proposition 2, there exists a winning finite-memory strategy σ for Controller. Let us show that every reachable cycle in R(A)[σ] is winning aperiodic. Assume towards a contradiction the existence of a cycle which is not winning aperiodic. Denote this cycle by π. This means that there exists a strategy τ for Perturbator such that the cycle π is eventually reached and repeated forever. Because π is not winning aperiodic, the play that starts in (ℓ 0 , r 0 ) and stays consistent with the couple of strategies (σ, τ ) cannot belong to W, a contradiction. Let us show the converse implication. Assume that C C holds, and let σ the finite memory strategy given by C C . We show that the strategy σ is wining for Controller in (R(A), W). Let τ be an arbitrary strategy for Perturbator and let ρ be the play consistent with (σ, ρ). As in case 1., one can factorize

ρ into ρ ′ 0 ρ ′ 1 ρ ′ 2 • • • such that ρ ′ i for i > 0 are cycles around a same state and Γ (ρ ′ 1 ) = Γ (ρ ′ 2 ) = • • • = γ.
To see that ρ ∈ W, it suffices to notice that ρ ′ i for i > 1 is an accepting cycle and that γ is aperiodic, thus there exists n such that γ n is complete.

⊓ ⊔

C Proofs of Section 5 (Solving the Robust Timed Game)

We note the following lemma from [11].

Lemma 23 ( [11]). For a timed automaton A with distinct labels Controller wins the robust timed game in A iff R(A) has a reachable winning aperiodic cycle.

Lemma 5. If C P holds, then Perturbator wins the robust timed game.

Proof. Let τ be Perturbator's finite-memory strategy yielding R(A)[τ ] witnessing property C P .

Let A ′ be the timed automaton defined on the set of locations R(A)[τ ], where the clock set is that of A. We have an edge (ℓ, r) -→ (ℓ, r ′ ) with the guard r ′ , whenever r ′ is a time-successor region of r (that is, ∃d ≥ 0, r + d ∈ r ′ ). Furthermore, there exists an edge (ℓ, r) a -→ (ℓ ′ , s) with guard r ′ if there exists an edge (ℓ, g, a, R, ℓ ′ ) with r ′ |= g in A . By Lemma 23, Perturbator has a winning strategy τ ′ in A ′ , since R(A ′ ) = R(A), and it has no reachable aperiodic cycles. Now, we show that the combination of τ and τ ′ is a winning strategy for Perturbator in the robust timed game on A.

We define strategy τ ′′ in A as follows. At any state (ℓ, ν), if Controller chooses the delay d ≥ 0 and action a, then τ ′′ determines the edge (ℓ, g, a, R, ℓ ′ ) following strategy τ , and the perturbation is chosen following τ ′ . The fact that we respect the strategy τ ensures that the projection of the play to regions stay within R(A) [τ ]. So the projection to regions of any outcome is also a path in R(A ′ ). The fact that the perturbations are chosen by τ ′ means that the generated play of A is also a play of A ′ . If some play of A under τ ′′ were infinite and accepting, this would mean that there is a corresponding play in A ′ winning for Controller, which is a contradiction.

⊓ ⊔ Lemma 7. Under condition C C , there exists an integer N such that every path ρ in B of length at least N has a complete folded orbit graph.

Proof. The arguments used in this proof already appear in the proof of Lemma 3; we sketch the ideas. It suffices to choose N large enough and apply Lemma 22 (with n ← N ). In fact, if all branches of the tree are long enough, then for each branch π, we get a factorization of the form Lemma 21, this means that π contains a factor with a complete FOG.

π = π ′ 0 π ′ 1 π ′ 2 . . . π ′ m+1 with m ≥ |C 0 | × |C 0 |!. By

⊓ ⊔

C.1 Shrunk DBMs

In order to make the presentation of the paper self-contained, we summarize here some results about shrunk DBMs and give details about elementary operations on this data structure. Most of the content of this section is from [5].

We call elementary operator on shrunk DBMs any operator obtained by mean of elementary operations that is : ∩, Pre >0 , Pre >δ , Unreset R (, ) and Shrink [-δ,δ] . The following lemma states that these elementary operator can be computed at the level of shrunk DBMs, in poly-time.

Lemma 24 ( [10,5]). Let M = f 0 (N 1 , . . . , N k ) be an equation where f is an elementary operator and N 1 , . . . , N k are normalized DBMs. Let P 1 , . . . , P k be SMs. Then, there exists a SM Q such that (M, Q) = f δ (N 1 , P 1 ), . . . , (N k , P k ) . The SM Q and an upper bound on δ can be computed in poly-time.

We now give some computational details about the result of Lemma 24 which we will need in subsequent proofs.

The operations on shrunk DBMs follow closely the counterparts on DBMs. Essentially, the matrices are defined on a richer algebra where elements are of the form ((m, ≺), p), which represent a constraint xy ≺ mδp, instead of only (m, ≺). We consider the following operations and relations. The addition is defined by ((m 1 , ≺ 1 ),

p 1 ) + ((m 2 , ≺ 2 ), p 2 ) = ((m 1 + m 2 , ≺), p 1 + p 2 ), where ≺ = ≤ if ≺ = ≺ ′ = ≤, and < otherwise.
Further, we let

((α, ≺), k) ((β, ≺ ′ ), l) ⇔    α < β or α = β and k > l, or α = β and k = l and ≺ ′ =< ⇒ ≺=< .
(1) Intuitively, the above relation can be obtained easily by instantiating δ to a sufficiently small value; the smaller constraint is the most restrictive. We also define the minimum as follows.

min (((α, ≺), k), ((β, ≺ ′ ), l)) = ((α, ≺), k) if ((α, ≺), k) ((β, ≺ ′ ), l), ((β, ≺ ′ ), l) otherwise. (2)
Given these operations, elementary operations are computed in shrunk DBMs just like in usual DBMs. For instance, to compute (O, R) = (M, P ) ∩ (N, Q), we let (O, R) x,y = min ((M, P ) x,y , (N, Q) x,y ), and we apply normalization (see below). To compute Pre ((M, P )), we set the first row of the matrix to ((0, ≤), 0) and apply normalization.

It remains to explain the normalization procedure, which is again very similar to that in DBMs. 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 ). We say that M is normalized when it is stable under normalization [4].

Similarly to DBMs, the normalization of shrunk DBMs is defined using finite shortest paths in the graph G(M ) of a given DBM M . Definition 25. 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 . In the rest of this paper, we consider paths π = π 1 . . . π n ∈ Π x,y (G(M )) weighted by a given DBM or any matrix. The M -sign of a path π, written sign M (π) is < if ≺ M πi,πi+1 =< for some i, and ≤ otherwise. 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. Finite-weighted shortest paths can be used to characterize the non-emptiness and the normalization of shrunk DBMs. In fact, the normalization consists in replacing each component of a shrunk DBM with the weight of its shortest path. Now, normalization consists in computing shortest paths in our algebra: Given a shrunk DBM (M, P ) we define norm(M, P ) = (M ′ , P ′ ) as follows: for each (x, y) ∈ C 0 , let P ′

x,y be the largest P -weight of the paths in Π x,y (G(M )). We let 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 sign <, and ≤ otherwise.

Lemma 26 ( [5]). 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, writing (M ′ , P ′ ) = norm(M, P ), there exists δ 0 > 0 such that M ′ -δP ′ is normalized and defines the same set as M -δP for all δ ∈ [0, δ 0 ].

C.2 Controllable Predecessors and Merge Operations

The goal of this subsection is to prove several properties about the controllable predecessor and merge operators. We prove that these operators yield non-empty sets along non-punctual paths. This crucial property will allow us to apply these operator to solve our robust timed games. Let us first give the formal definition of CMerge on the whole unfolding.

Definition 27 (CMerge on trees). Let t be a finite prefix of an unfolding Unfold(B, q), denote by q 1 , . . . , q n the (labels of ) leafs of t with q i = (ℓ i , r i ), and let δ ≥ 0. Let (M i ) 1≤i≤n be DBMs such that M i ⊆ r i , we define the set of δ-controllable predecessors of M i 's through t as follows:

if the depth of t is equal to 0, then we have n = 1 and q = q 1 and we let: CMerge δ t (M 1 ) = M 1 -otherwise, we can write t = q(t 1 , . . . , t k ). Then there exist indices i j and n j , with 1 ≤ j ≤ k, such that (labels of ) leafs of subtree t j are precisely q ij , . . . , q ij +nj . We let q ′ j denote the root of t j , e j = q → q ′ j , with 1 ≤ j ≤ k, and define: CMerge δ t ((M i ) 1≤i≤n ) = CMerge δ e1,...,e k ((N j ) 1≤j≤k ) where

N j = CMerge δ tj ((M p ) ij ≤p≤ij +nj )
The following lemma shows that the controllable predecessors of a nonpunctual path is non-empty provided that the target set has non-empty interior.

We consider the usual

d ∞ metric on R C , defined as d ∞ (ν, ν ′ ) = max x∈C |ν(x)- ν ′ (x)|. We define Ball d∞ (u, ε)
as the open ball of radius ε around the valuation u using the infinite norm on valuations.

Lemma 28 ( [11]). Let π be a non-punctual path from a region r to s. Let s ′ ⊆ s such that there exists v ′ ∈ s ′ and ε > 0 with Ball d∞ (v ′ , ε)∩s ⊆ s ′ . Then, CPre δ π (s ′ ) is non-empty for small enough δ > 0.

We state here a more precise version of the above lemma.

Lemma 29. Let π be a non-punctual path from a region r to s. Let r ′ ⊆ r and s ′ ⊆ s such that there is v ′ ∈ s ′ and ε > 0 with Ball d∞ (v ′ , ε) ∩ s ⊆ s ′ , and r ′ = CPre 0 π (s ′ ). We suppose that r ′ and s ′ are defined by DBMs. Consider P a SM such that (s ′ , P ) = ∅. Then, there exists Q a SM such that:

-(r ′ , Q) = CPre δ
π (s ′ , P ), and -(r ′ , Q) is non-empty for small enough δ.

Proof. To prove the first item, it is sufficient to notice that CPre is an elementary operator, thus thanks to Lemma 24 there exists a SM Q such that the first item holds.

Let us show the second item. For this notice first that (s ′ , P ) = ∅ means that for small enough δ > 0, s ′δ • P has a non-empty interior in the topology induced on s. Therefore, the requirements of Lemma 28 hold, and it follows that there exists δ ′ such that CPre δ ′ π (s ′δ • P ) = ∅. To obtain the desired result, it is sufficient to show that the second item holds when δ ′ = δ. Assume first that δ ′ ≥ δ, then the second item of the lemma follows because CPre δ0 π (Z)

⊆ CPre δ1 π (Z) for δ 0 > δ 1 . If δ ′ < δ, then the result still holds because z -δ • M ⊆ z -δ ′ • M for δ ′ < δ. ⊓ ⊔
A similar property can be proved on the CMerge operator.

Lemma 30. Let r, r 1 , • • • , r n be a set of regions satisfying r = CMerge 0 e1,...,en (r

1 , • • • , r n ). Consider r ′ ⊆ r, and r ′ i ⊆ r i for each i such that there is v ′ i ∈ r ′ i and ε > 0 with Ball d∞ (v ′ i , ε) ∩ r i ⊆ r ′ i , and r ′ = CMerge 0 e1,...,en (r ′ 1 , • • • , r ′ n ).
We suppose that r ′ , r ′ 1 , . . . , r ′ n are defined by DBMs. Let P 1 , • • • , P n be a set of SMs such that (r ′ i , P i ) = ∅. Then there exits a SM Q such that: -(r ′ , Q) = CMerge δ e1,...,en ((r ′ i , P i ) i ), and -(r ′ , Q) is non-empty for small enough δ.

Proof. Let us denote by (ℓ, g i , a, R i , ℓ i ) the transition associated with edge e i , and denote by s the non-punctual intermediate region time-successor of r and such that s[R i ← 0] = r i . For any i, there exists a SM P ′ i such that Unreset Ri ((

r ′ i , P i )) ∩ s = (s ′ i , P ′ i ) = ∅ where s ′ i = Unreset Ri (r ′ i ) ∩ s.
Moreover because (r ′ i , P i ) has nonempty interior in the topology induced on r i and s is non-punctual, s ′ i is also non-punctual. Then there exists a SM P ′ such that n i=1 (s ′ i , P ′ i ) = (s ′ , P ′ ) = ∅, where s ′ is non-punctual. We get the desired result thanks to the following facts. On one hand, r is a temporal predecessor of s ′ . Therefore, there exists a valuation ν ∈ r and a delay d such that we have ν • d = ν ′ . On the other hand, s ′ is non-punctual, hence there exists η > 0 such that

ν ′ + [-η, η] ⊆ Ball d∞ (ν ′ , ε ′ ). ⊓ ⊔
It is then easy to deduce from Lemmas 29 and 30 that Lemma 10 holds, by induction on the size of the (finite) prefix of an unfolding.

C.3 The notion of 0-dominance

The subsection contains the proof of the results related to 0-dominance. The goal of these developments is to prove Lemma 11, which is the only lemma used in the rest of the proof.

The following lemma shows that the 0-dominance relation is monotonous; in other terms, it shows how the zeros of the shrinking matrices are (backward-) propagated along computations.

Lemma 31. The operations Pre, Unreset(), ∩ are monotonous for the relation 0 in the following sense.

-Let (N, P ′ ) = (M 1 , P 1 ) ∩ (M 2 , P 2 ) and (N,

Q ′ ) = (M 1 , Q 1 ) ∩ (M 2 , Q 2 ). Then P 1 0 Q 1 ∧ P 2 0 Q 2 ⇒ P ′ 0 Q ′ . -Let (N, P ′ ) = Pre((M, P )) and (N, Q ′ ) = Pre((M, Q)). Then P 0 Q ⇒ P ′ 0 Q ′ . -Let (N, P ′ ) = Unreset R ((M, P )) and (N, Q ′ ) = Unreset R ((M, Q)). Then P 0 Q ⇒ P ′ 0 Q ′ .
Proof. -That Q ′ ≤ P ′ follows from the monotonicity of the operation (Z, Z ′ ) → Z ∩ Z ′ . We show that Q ′ x,y = 0 implies P ′ x,y = 0 for any x, y. We recall the intersection operation on shrunk DBMs. We first define a SM P ′′ as follows. For any x, y ∈ C 0 , if (M i ) x,y < (M 3-i ) x,y for some i = 1, 2, then (N ′ i ) x,y = (M i ) x,y and P ′′

x,y = (P 1 ) x,y . Otherwise P ′′ x,y = max((P 1 ) x,y , (P 2 ) x,y ). Then, (N, P ′ ) is the normalization of (N ′ , P ′′ ). Let us denote by Q ′′ this intermediate SM computed for the other equation. It is clear that under the assumption

P 1 0 Q 1 ∧ P 2 0 Q 2 , Q ′′
x,y = 0 implies P ′′ x,y = 0. Now, the normalization consists in assigning to each P ′

x,y , the maximum P ′′ -weight of the shortest paths from x to y in G(N ′ ). So, if P ′

x,y > 0, then there exists a shortest path in G(N ′ ) from x to y whose P ′′ -weight is positive, that is, there exists an edge (z, z ′ ) in this path with P ′′ z,z ′ > 0. But we must have Q ′′ z,z ′ > 0 by assumption. This implies that Q ′

x,y > 0. -That Q ′ ≤ P ′ follows again from the monotonicity of the operation Z → Pre(Z). Given (M, P ), the Pre((M, P )) is computed as follows. We first define (M ′ , P ′′ ) by assigning (0, 0) to all components of the first row, and then define (N, P ′ ) as the normalization of (M ′ , P ′′ ). By the same reasoning on the normalization procedure as in the first case, we obtain that P 0 Q implies P ′ 0 Q ′ . -That Q ′ ≤ P ′ follows again from the monotonicity of the operation Z → Unreset R (Z). The unreset operation is defined as Unreset R (Z) = free R (R = 0 ∧ Z), that is we first intersect with the zone ∧ x∈R x = 0, and free all constraints on the clocks x ∈ R. The intersection was treated by the first case of this lemma. Thus, if we denote (M ′ , P 1 ) = (R = 0) ∧ (M, P ) and (M ′ , Q 1 ) = (R = 0) ∧ (M, Q), then we know that P 1 0 Q 1 . We now concentrate on the free R operation which consists in replacing by (∞, 0) all components (x, y) of the given shrunk DBM where x ∈ R or y ∈ R, and applying normalization. The 0-dominance relation is preserved before normalization by construction, and after normalization by the same reasoning as in the first case of this lemma.

⊓ ⊔

The following two lemmas compare the operators CPre and CMerge with respect to 0-dominance.

Lemma 32. Let r, r ′ , r 1 , r 2 be regions and P, P 1 , P 2 , Q, Q 1 , Q 2 be SMs such that:

-(r, P ) = CMerge 0 a,r ′ ((r 1 , P 1 ), (r 2 , P 2 )) ∩ r, -(r, Q) = CPre 0 e1 (r 1 , Q 1 ) ∩ CPre 0 e2 (r 2 , Q 2 ) ∩ r, -P i 0 Q i for i ∈ {1, 2}.
Then P 0 Q.

Proof. We start by rewriting the shrunk DBMs under consideration. We have :

(r, P ) = CMerge 0 a,r ′ ((r 1 , P 1 ), (r

2 , P 2 )) ∩ r = Pre(r ′ ∩ Unreset R1 ((r 1 , P 1 )) ∩ Unreset R2 ((r 2 , P 2 ))) ∩ r = Pre((r ′ ∩ Unreset R1 ((r 1 , P 1 ))) ∩ (r ′ ∩ Unreset R2 ((r 2 , P 2 )))) ∩ r . and: (r, Q) = CPre 0 e1 (r 1 , Q 1 ) ∩ CPre 0 e2 (r 2 , Q 2 ) ∩ r = Pre(r ′ ∩ Unreset R1 ((r 1 , Q 1 ))) ∩ Pre(r ′ ∩ Unreset R2 ((r 2 , Q 2 ))) ∩ r . We let (r ′ , P ′ i ) = r ′ ∩ Unreset Ri ((r i , P i )), (r ′ , Q ′ i ) = r ′ ∩ Unreset Ri ((r i , Q i ))
, and (r,

Q ′′ i ) = r ∩ Pre((r ′ , Q ′ i )) for i ∈ {1, 2}
and we obtain :

(r, P ) = Pre((r ′ , max(P ′ 1 , P ′ 2 ))) , (r, Q) = (r, max(Q ′′ 1 , Q ′′ 2 )) .
We let (M, P M ) = Pre ((r

′ , P ′ 1 ) ∩ (r ′ , P ′ 2 )) and (M, Q M ) = Pre ((r ′ , Q ′ 1 )) ∩ Pre ((r ′ , Q ′ 2 )
). It suffices to show that P M 0 Q M since this implies, by Lemma 31 that P 0 Q. Again by Lemma 31, we already know that P ′ i 0 Q ′ i for all i = 1, 2. We will need the following observation. For any shrunk DBMs satisfying

(N ′ , R ′ ) = Pre((N, R)), for any x, y ∈ C 0 with x = 0, R x,y = R ′
x,y . In other terms, the diagonal constraints and upper bounds are preserved under the pretime operation. This can be seen as follows. In DBMs, the pretime consists in assigning 0 to the first row and applying normalization. Because the first row always takes nonpositive values, the normalization only changes the first row. In fact, consider any component (z, z ′ ) with z = 0. Because the value of a component (0, x) cannot decrease after being assigned 0, this operation does not introduce any new shortest paths from z to z ′ , so the component (z, z ′ ) is not updated during normalization. In shrunk DBMs, the situation is similar: because no new shortest paths are introduced from z to z ′ , R z,z ′ is not updated during normalization, hence R ′ z,z ′ = R z,z ′ . We now show P M 0 Q M . Assume that (P M ) x,y > 0 for some x, y ∈ C 0 with y = 0. Given the previous remark, we get that either (P ′ 1 ) x,y > 0 or (P ′ 2 ) x,y > 0. But because

P ′ i 0 Q ′ i , this means that either (Q ′ 1 ) x,y > 0 or (Q ′ 2 ) x,y > 0. It follows that Pre((r ′ , Q ′ i )) x,y > 0 for some i = 1, 2, thus (Q M ) x,y > 0. It remains to show that (P M ) 0,x > 0 implies (Q M ) 0,x > 0. Let (r ′ , P ′′ ) = (r ′ , P ′ 1 ) ∩ (r ′ , P ′ 2 )
. Because the pretime operation first resets the row of (r ′ , P ′′ ) to (0, 0) before applying normalization, this means that there exists a shortest path in G(M ) from 0 to x along which there is an edge (z, z ′ ) such that (P ′′ ) z,z ′ > 0. This implies that (

P ′ i ) z,z ′ > 0 for some i = 1, 2, so (Q ′ i ) z,z ′ > 0. It follows that the component (z, z ′ ) of Pre((r ′ , Q ′ i )) is positive, so (Q M ) z,z ′ > 0. ⊓ ⊔
Lemma 33. Let r, r 1 , r 2 be regions and P, P 1 , P 2 , Q, Q 1 , Q 2 be SMs such that:

-(r, P ) = CPre 0 π0 CPre 0 π1 ((r 1 , P 1 )) ∩ CPre 0 π2 (r 2 , P 2 )) , -(r, Q) = CPre 0 π0π1 (r 1 , Q 1 ) ∩ CPre 0 π0π2 (r 2 , Q 2 ), -(s, P 1 ) = CPre 0 π ′ ((s, P ′ 1 ) ∩ (s, P ′ 2 )), -(s, Q 1 ) = CPre 0 π ′ ((s, Q ′ 1 )) ∩ CPre 0 π ′ ((s, Q ′ 2 )
). By induction hypothesis, we have P 1 0 Q 1 . We now consider

-(r, P ) = CPre 0 e CPre 0 π ′ ((s, P ′ 1 ) ∩ (s, P ′ 2 )) , -(r, Q 2 ) = CPre 0 e CPre 0 π ′ ((s, Q ′ 1 )) ∩ CPre 0 π ′ ((s, Q ′ 2 )
) . which yields P 0 Q 2 by Lemma 31. Last, we consider the following equations.

-(r, Q 2 ) = CPre 0 e CPre 0 π ′ ((s, Q ′ 1 )) ∩ CPre 0 π ′ ((s, Q ′ 2 )) . -(r, Q) = CPre 0 e CPre 0 π ′ ((s, Q ′ 1 )) ∩ CPre 0 e CPre 0 π ′ ((s, Q ′ 2 )
) , By Lemma 32, applied with e 1 = e 2 , we get that Q 2 0 Q. It follows that

P 0 Q. ⊓ ⊔

D EXPTIME-hardness

We reduce the halting problem for linearly-bounded alternating Turing machines to the reachability of an absorbing state in our semantics, which implies the hardness for Büchi objectives as well. We first explain the reduction for robust timed games, i.e. in the adversarial semantics. At the end of this section, we will adapt the reduction to almost-sure reachability in the MDP semantics. Note that the EXPTIME-hardness of the stochastic game semantics follows from the equivalence with the adversarial semantics.

D.1 Hardness of Robust Timed Games

The reduction follows that of [11] from non-alternating Turing machines that shows the PSPACE-hardness of the problem when Perturbator can only perturb delays. The encoding is quite standard for timed automata with the particularity that it should allow the operations to be defined without the use of equality guards. The alternation is introduced thanks to the ability of both players to determine the successor locations. An alternating Turing machine contains three types of states:

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

We do not recall the acceptance condition on disjunctive and conjunctive states, and refer to [7]. We assume that there is one distinguished state halt where the machine halts.

Let M be a linearly-bounded alternating Turing machine, and w 0 be an input to M. Let N be the bound on the tape of M when simulating on input word w 0 (N is linear in |w 0 |). We assume the alphabet is {a, b}, and we encode the content of the i-th cell C i of M using a clock x i with the following convention: when the module is entered, cell C i contains an a whenever x i < 1, and it contains a b whenever x i > 2.

To simulate a transition at a state q with trans(q) = (α, β, dir, q ′ ) of M, where α, β ∈ {a, b} and dir ∈ {-1, 1}, we build a module as in Fig. 9 for every index i such that both i and i + dir lie between 1 and N . Along this module, after any initial delay of duration u 0 ∈ (2, 3), cell C j contains a iff x j < 4, and it contains b iff x j > 4. Transitions between p j and p j+1 , for j = i, ensure preservation of this encoding. Between p i and p i+1 , the module checks that C i = α (through guard g α,i ), and replace this content with β (through reset Y β,i ). This way, one run through the module updates the content of the tape and the position of the tape head according to the selected transition of M.

q, i p1 p2 . . . pi pi+1 . . . pN pN+1 q ′ , i + dir u:=0 2<u<3 u<3 u:=0 g a,1
x 1 :=0

g b,1 g α,i Y β,i g a,N
x N :=0 g b,N Fig. 9. Simulating states q with trans(q) = (α, β, dir, q ′ ) where α, β ∈ {a, b}. Index i is such that 1 ≤ i ≤ N and 1 ≤ i + dir ≤ N . Guards and resets are defined as follows: ga,j is (xj < 4 ∧ u < 3) and g b,j is (xj > 4 ∧ u < 3), while Ya,j is {xj} and Y b,j is empty. Notice that at any state pi, only one transition is enabled. So we assume that all edges have distinct labels in this module.

A disjunctive state q with trans(q) = q ′ ∨ q ′′ is simulated by the following module, which allows Controller to pick any successor.

A conjunctive state q with trans(q) = q ′ ∧ q ′′ is simulated by the following module, which allows Perturbator to pick the successor.

We also need a simple normalization module which will make sure that the clocks are bounded. Assume that an a in cell C j is encoded with clock constraint x j < 1, and a b with clock constraint 2 < x j < 4 when entering a state (q, i). Then all above modules ensure that, when leaving the module, either x j < 1 (in q, i q ′ , i q ′′ , i 2<u<3 2<u<3,q ′ 2<u<3,q ′′ Fig. 10. Simulating states q with trans(q) = q ′ ∨ q ′′ . The edges leaving the state (q, i) have distinct labels q ′ and q ′′ which correspond to Controller's choice. q, i q ′ , i q ′′ , i 2<u<3 2<u<3,q 2<u<3,q Fig. 11. Simulating states q with trans(q) = q ′ ∧ q ′′ . The edges leaving the state (q, i) have the same label q. Thus Perturbator has full control on the successor location at this state.

Fig. 9, in case cell C j now contains an a), or either 2 < x j < 4 or 4 < x j < 7 (the two possible cases for cell C j to contain a b). It is easy to plug at the end of each module another module, which ensures that 2 < x j < 4 when cell C j contains an a, and x j < 1 when cell C j contains a b. Then we can plug at the end of this second module another one which ensures that x j < 1 when cell C j contains an a, and 2 < x j < 4 when cell C j contains a b, which is the initial encoding. Using this trick, the constructed timed automata has only bounded clocks.

We complete the construction with an initialization module (encoding input w 0 on the tape). We write A for this timed automaton and write halt for the halting location (which is made a sink). The set {halt} is the Büchi condition.

We show the following lemma:

Lemma 34. Let s 0 be the initial configuration of A. The following conditions are equivalent:

1. M has a halting computation on w 0 ; 2. Controller has a strategy in G δ (A) to reach halt, for all δ < 1 4N ;

Proof. First assume that M has a halting computation on w 0 . We describe a robust winning strategy for the Controller in A. We consider the simulation of the state q and transition (α, β, dir, q ′ ) of M. Assume state (q, i) is entered with some valuation v 0 that properly encodes some content of the tape of M: if cell C j contains an a, then v 0 (x j ) < 1, and if cell C j contains a b, then v 0 (x j ) > 2.

We describe a strategy for Controller, and then pick a corresponding outcome (with perturbations). The candidate strategy is as follows: leave (q, i) when u = 2.5, and in each of the p j 's, wait for δ time units, and then takes the next feasible transition. Under this strategy, and assuming that Perturbator perturbs by -δ ≤ ε 0 ≤ δ on transition leaving (q, i), and by -δ ≤ ε j ≤ δ on transition leaving p j , the valuation when arriving in p j is v j (resp. in (q ′ , i + dir) is v ′ 0 ) such that:

29

-if i = j and cell C j contains a b, or if i = j and β = b, then for every

1 ≤ k ≤ N + 1, v k (x j ) = v 0 (x j ) + 2.5 + (k -1)δ + k-1
h=0 ε h ; -if i = j and cell C j contains an a, or if i = j and β = a, then for every 1 ≤ k ≤ j, v k (x j ) = v 0 (x j ) + 2.5 + (k -1)δ + k-1 h=0 ε h , v j+1 (x j ) = 0, and for every j

+ 2 ≤ k ≤ N + 1, v k (x j ) = (k -j -1)δ + k-1 h=j+1 ε h .
Note that in all cases, since δ < 1 4N , if cell C j contains an a, then v j +δ +ε j |= g a,j , and if cell C j contains a b, then v j + δ + ε j |= g b,j . Note also that if either i = j and cell C j contains an a, or if i = j and β = a, then v ′ 0 (x j ) < 1, and if either i = j and cell C j contains a b, or if i = j and β = b, then v ′ 0 (x j ) > 2. This means that whatever the perturbation, at the end of the module the clocks properly encode the new content of the tape of M after the mentioned transition has been taken. The same strategy is applied in the normalization modules; this ensures that perturbations are not accumulated too much along disjunctive or conjunctive states.

We can apply this strategy in every module simulating a transition of the Turing machine. Since M halts on w 0 , the halt state can be reached by following this strategy.

Conversely, if M does not halt on w 0 , then when playing without perturbations, Controller cannot reach the halting state. In particular, Controller has no robust strategy. ⊓ ⊔

D.2 Hardness of the MDP semantics

We consider the same reduction with a slight modification. Observe that if a linearly bounded alternating Turing machine M accepts a word w 0 , then it accepts in at most |M |2 N steps. In other terms, this is the bound on the execution tree witnessing the acceptance. Now, in each module we constructed, the automaton spends at most 3 + 4N time units, where 3 time units are spent for simulating a transition, and at most 4N for normalization of the encoding. Given an instance M, w 0 , let A ′ denote the timed automaton obtained from A by adding a new clock t which is guarded by t ≤ (3 + 4N )|M |2 N at each transition, except on the self-loop of state halt. We can now rewrite Lemma 34, as follow: the word w 0 is accepted by M if, and only if Controller has a strategy in G δ (A ′ ) reaching halt for δ < 1 4N . Note also that A ′ can be constructed in polynomial time. In particular, the constants can be encoded in polynomial space.

Because time progresses in each module of A ′ the only infinite behaviors are those reaching halt. The reduction for the MDP semantics follows. In fact, if the Turing machine accepts, then Controllerhas a strategy ensuring that all compatible runs reach halt in less than (3 + 4N )|M |2 N time units, so this also holds if perturbations and the non-determinism are probabilistic. Conversely, if M does not accept, then for any Controllerstrategy, there exists a choice for the conjunctions such that the machine does not end in halt after |M |2 N steps; it follows that with positive probability, halt is not reached before (3 + 4N )|M |2 N time units.

Lemma 35. Let s 0 be the initial configuration of A. The following conditions are equivalent:

1. M has a halting computation on w 0 ; 2. Controller has a strategy in G MDP δ (A ′ ) to reach halt almost surely, for all δ < 1 4N ;

E Probabilistic Semantics

In this section, we formally define a probability space on timed automata runs under given strategies, and prove our results in this setting. Our definitions follow closely [2]. In particular, we define the probability measure on cylinders defined by the same constrained symbolic paths (see below). This allows us to reuse the proofs of [2] to derive the well-definedness of our measure. We start by formally defining the stochastic game semantics, and then define the MDP semantics as a particular case.

E.1 Probability Measures

Fix a timed automaton A. For any state s = (ℓ, ν), and set of edges e 1 . . . e n , we will define a symbolic path as the set of runs that start at s and follow the edges e 1 . . . e n . We will moreover consider a constraint C ⊆ R n over the sequence of delays of such runs. Formally,

π (s, e 1 . . . e n ) = {ρ = s τ1,e1 ---→ s 1 - → . . . - → s n | ρ ∈ Runs f (A, s), (τ i ) i ∈ C}.
We define the cylinder of π C (s, e 1 . . . e n ) as the set of infinite runs whose prefix of length n belongs to π C (s, e 1 . . . e n ). Given a pair of strategies, we will define a probability measure based on these cylinders. A Controller's strategy σ is measurable if for any action a ∈ Act, the subset of histories σ -1 (R × {a}) is Lebesgue-measurable. A Perturbator's strategy τ is measurable if for any edge e, the subset of histories τ -1 ({e}) is Lebesgue-measurable.

We will write the histories as sequences of the form sd 1 t 1 e 1 . . . d n t n e n , where s is the starting state, d i the delay suggested by Controller, t i the perturbed delay (such that |t i -d i | ≤ δ, and e i the edge that is taken after the delay. Histories where Controller has made a move will be denoted by sd 1 t 1 e 1 . . . d n t n e n (d n+1 , a n+1 ). Note that e i determines the action chosen by Controller along with the delay d i . For Controller's strategy σ, we denote by σ d (h) the delay prescribed at history h.

In the probabilistic setting, we will restrict to pairs of measurable strategies. Let σ, τ be such a pair. Consider a sequence of edges ē = e 1 . . . e n , and denote by a i the label of edge e i . We consider a sequence of nonnegative reals t 1 , . . . , t n , and use the notation ti = (t 1 , . . . , t i ). We also denote by h σ,τ s,i = sd 1 t 1 e 1 . . . d i t i e i , the history of length i starting at s under σ, τ . We define for 1 ≤ i < n,

I σ,τ i (s, ti-1 , ē) = σ d (h σ,τ s,i-1 ) ± δ ∩{t i | h σ,τ s,i ∈ σ -1 (R × {a i+1 })} ∩{t i | h σ,τ s,i • (d i , a i ) ∈ τ -1 ({e i+1 })}
For i = n, we let I σ,τ n (s, tn , ē) = σ d (h σ,τ s,n-1 ) ± δ. This defines the set of perturbed delays that can be observed at given history when Controller has strategy σ, such that the players' next moves conform to the edge sequence ē. By hypothesis, each set I σ,τ i (•) is measurable. 7 For any measurable constraint C, we define the probability of a constrained symbolic path as follows.

P σ,τ G SG δ (A),s (π C (s, e 1 • • • e n )) = t1∈I σ,τ 1 (s,ē) t2∈I σ,τ 2 (s, t1 ,ē) tn∈I σ,τ n (s, tn-1 ,ē) 1 C dt1 2δ • dt2 2δ • • • • dtn 2δ ,
We initialize by P σ,τ G SG δ (A),s (π C (s)) = 1. This definition makes sure that we sum over values for t 1 , . . . , t n which are compatible with the strategies, satisfies C, and follow the symbolic path e 1 . . . e n . Note that each integral is well-defined thanks to the measurability assumption on the strategies.

We define the MDP semantics by restricting to a unique strategy of Perturbator, consisting, given a move (d, a) by Controller, in choosing all available edges with label a with equal probability. We define the probability measure P σ G MDP δ (A),s (•) given state s, and Controller strategy σ.

Let us denote Ω s A the σ-algebra generated by the cylinders. Theorem 36. For any timed automaton A, state s, and pair of measurable strategies σ, τ , P σ,τ G SG δ (A),s and P σ G MDP δ (A),s define a probability measure over (Runs(A, s), Ω s A ).

Proof. The proof follows step by step that of [2], see [3, pages 40-42].

⊓ ⊔

Notice that the probability measure in the MDP semantics is a particular case of that of the stochastic game semantics; so it suffices to show the correctness of the latter. Note that the set of Büchi-accepting runs is measurable since it can be written as the intersection, for n > 0, of all cylinders that visit at least n times accepting locations. Let us denote by φ the set of runs that are accepting for the given Büchi condition. We say that a strategy σ for Controller is almost surely winning if for any Perturbator's strategy τ , P σ,τ G SG δ (A),s (φ) = 1.

E.2 Stochastic Game Semantics: Characterization

Our main result on the stochastic game semantics is that considering probabilistic perturbations rather than adversarial ones do not weaken Perturbator: the characterization for the robust game semantics also holds in the stochastic game semantics. The idea is the following. If condition C C holds, then we know that Controller can win against adversarial perturbations, so he can also win against Perturbator with probabilistic perturbations. The converse is more tricky: we show that if C P holds, then under any Controllerstrategy, a non-aperiodic cycle is repeated a large number of times, and almost surely the run is blocking; thus finite, and fails to satisfy the Büchi condition.

We will now formalize these ideas and give the full proof. Let us first recall some definitions: We define ε-far runs and show that such runs are blocking along non-aperiodic cycles. 7 In fact, if Cyl(h σ,τ s,i-1 ) denotes all histories extending h σ,τ s,i-1 , then we have

I σ,τ i (•) = pi Cyl(h σ,τ s,i-1 ) ∩ σ -1 (R × {ai+1}
, where pi denotes the canonical projection from R n to the i-th component.

Let us call a valuation

v ε-far if v + [-ε, ε] ⊆ [v].
A run is ε-far if all delays end in ε-far valuations. We show that after any Controller's move the perturbed delay is ε-far with nonzero probability. ⊓ ⊔

We say that a run is ε-far if all perturbed delays end in ε-far valuations. It was shown in [11] that these runs along non-aperiodic cycles necessarily lead to a deadlock.

Lemma 38 ([11, Section 5]). For any timed automaton A, let ε be as in Lemma 37. There exists n > 0 such that along any non-aperiodic cycle, there is no ε-far run of length n.

Before we prove Theorem 13, observe that the strategy σ derived from condition C C is measurable since it has finite-memory and described via shrunk DBMs. Similarly, the strategy τ derived from C P is also measurable. Now the idea behind the proof in our case is to show that along any infinite run, almost-surely, some n consecutive delays will be ε-far. Proof. We first show that if C C holds then Controller wins almost-surely. This is a straightforward corollary of the fact that if C C holds, then there exists a strategy σ that wins against any strategy of Perturbator, this in particular includes the strategies of Perturbator where the perturbations are chosen at random.

Let us show that if C P holds then Perturbator wins almost-surely. In order to obtain the desired result, we first show that under C P , for any choice of strategies (σ, τ ) any maximal play that is infinite and consistent with the couple (σ, τ ) is eventually ε-far for n steps with n > 0.

Denote by A k,n the set of plays that are are either of length less than k +n and cannot be extended or of length k + n and are ε-far between steps k + 1 . . . k + n. Note the ε-far requirement can be written as a set of constraints over n variables, therefore we can express this set of plays by set of symbolic paths. Hence this set is measurable. Moreover, because k, n are both finite and at each step the choice of ε is independent of the current prefix of the play it follows that:

∀σ, ∀τ, P σ,τ G SG δ (A),s (A k,n ) ≥ δ 4(C + 1) n . It follows that ∀σ, ∀τ, P σ,τ G SG δ (A),s (∃k > 0, A k,n ) = 1 .
We now consider the strategy τ for Perturbator given by C P under which all cycles are non-aperiodic. It follows from Lemma 38 that there is no infinite run under τ , so P σ,τ G SG δ (A),s (φ | ∃k > 0, A k,n ) = 0. Therefore, for any strategy σ for Controller we have:

P σ,τ G SG δ (A),s (φ) = P σ,τ G SG δ (A),s (φ | ∃k > 0, A k,n )P σ,τ G SG δ (A),s (∃k > 0, A k,n ) + P σ,τ G SG δ (A),s (φ | ∀k > 0, ¬A k,n )(1 -P σ,τ G SG δ (A),A (∃k > 0, A k,n )) = P σ,τ G SG δ (A),s (φ | ∀k > 0, ¬A k,n )(1 -P G SG δ (A),σ,τ s (∃k > 0, A k,n )) = 0 . ⊓ ⊔

E.3 MDP semantics: Characterization

In the MDP semantics, for given δ > 0, at each step, Controller picks a delay d ≥ δ, and an action a such that for every edge e = (ℓ, g, a, R, ℓ ′ ) such that ν + d |= g, we have ν + d + ε |= g for all ε ∈ [-δ, δ], and there exists at least one such edge e. Then, a perturbation ε ∈ [-δ, δ], and an edge satisfying the above conditions are chosen independently and uniformly at random. Thus in this semantics, Controller's strategy resolves all non-determinism, and defines a random process.

For a given timed Büchi automaton, denote φ the set of accepting runs. The almost-sure winning problem under the MDP semantics consists in deciding the following equation: ∃δ > 0, ∃σ, P σ s0 (φ) = 1.

(3)

We will present a decidable characterization on the region graph R(A). First we define formally what an MDP is. Definition 39. An MDP is a tuple (S, A, P ), where S is a finite set of states, A is a finite set of actions, and P is the following mapping P : S × A → dist(S) where dist(S) is the set of probability distributions of S.

We will see R(A) as an MDP by assigning uniform probability distributions to all available actions (r ′ , a) at each state (ℓ, r). We then consider the deterministic Büchi automaton B of Lemma 20 which recognizes infinite paths in the region automaton containing infinitely many disjoint factors with complete FOGs. We consider the direct product of the MDP R(A) with the (deterministic) automaton B, which is again a finite-state MDP, which we denote by G. Let us denote by F B the set of states of G whose projections to B are accepting. By an abuse of notation, we still denote by φ the set of states of G whose projections to R(A) are accepting for φ.

A run in an MDP is infinite sequence of states, a history is a finite run, and a strategy is a mapping that assigns to every history an action. Once an initial state s and a strategy σ are chosen in an MDP M , one can define a unique measure over the runs of M denoted P σ M (c.f. [9]).

Algorithm for almost-sure winning We are now ready to state two equivalent conditions on R(A), which we will then prove to characterize almost sure Büchi winning condition for the MDP semantics. The first condition C 1 corresponds to W ′ in the core of the paper; however, we also need to introduce the equivalent condition C 2 in order to carry out the proofs.

Lemma 40. The following conditions are equivalent:

(C 1 ) there exists a finite-memory strategy σ for R(A) such that every reachable cycle in R(A)[σ] is aperiodic, and P σ R(A) (φ) = 1. (C 2 ) there exists a finite memory strategy σ for G such that Büchi condition F B is surely satisfied, and P σ G (φ) = 1.

Proof. We start by showing that C 1 =⇒ C 2 . Let σ be the strategy defined by C 1 . We denote by σ the strategy of Controller in G defined for any finite prefix h of G by σ(h) = σ(f (h)),

where f is the projection of h over the states of R(A). Since B does not restrict the moves of R(A) and P σ R(A) (φ) = 1 it follows that P σ G (φ) = 1. We show that under σ, F B is satisfied surely. Let π be an infinite run over G[σ] and let ρ = f (π) be the projection of π over R(A) [σ]. As in the proof of Lemma 3, because all cycles of R(A)[σ] are aperiodic, by Lemma 7, ρ contains infinitely many factors with complete FOGs. Furthermore, any path that contains a factor with a complete FOG has a complete FOG too. By construction of B, it follows that B accepts ρ.

We show now that C 2 =⇒ C 1 . Assume C 2 and let σ be the strategy witnessing C 2 . We define the strategy σ for every finite prefix h over the states of R(A) as follows:

σ(h) = σ(h ′ ),

where h ′ = f -1 (h), which is well defined since B is deterministic. Again since σ satisfies φ almost-surely in G and the fact that B does not restrict the actions of R(A), it follows that P σ R(A) (φ) = 1. It remains to show that under σ, every reachable cycle in R(A)[σ] is aperiodic. Assume towards a contradiction the existence of a reachable non-aperiodic cycle in R(A)[σ] and let ρ 0 ρ ω be a run in R(A) compatible with σ such that γ(ρ) is non-aperiodic. Then, there exists an infinite run π 0 π ω in G compatible with σ such that f (π 0 ) = ρ and f (π) = ρ. We show that π 0 π ω is not accepted by B. In fact, if a complete FOG appears in this word, then any longer suffix has a complete FOG, which is not the case since for each n >, π 0 π n has a non-aperiodic FOG.

⊓ ⊔ Before proving that these conditions characterize almost-sure winning in the MDP semantics, let us prove that they are decidable in exponential time, thus proving Lemma 16. For this, we prove a more general result showing how to compute winning states and strategies in MDPs given with one almost-sure and one sure Büchi objectives.

For an MDP M , and a subset of states S ′ ⊆ S, we say that S ′ induces a sub-MDP if the MDP M restricted to states of S ′ is an MDP. In this case, we abuse of notation and say that S ′ is a sub-MDP. We also say that a strategy σ is compatible with a sub-MDP S ′ if, when started in any state of S ′ , all actions prescribed by σ surely lead to states in S ′ . Lemma 41. Let M be any MDP with state space S, φ 1 , φ 2 Büchi objectives. Let Q ⊆ S be the largest sub-MDP satisfying the following two conditions: i) for every q ∈ Q there exists a strategy σ 1 compatible with Q such that φ 1 is satisfied surely in Q, ii) for every q ∈ Q there exists a strategy σ 2 compatible with Q such that φ 2 is satisfied almost-surely in Q.

Then Q is the set of all states of M from which there exists a strategy σ surely satisfying φ 1 , and almost-surely satisfying φ 2 . Moreover, strategies with linear memory are sufficient, and one can compute Q, and a winning strategy in polynomial time.

Proof. Note that both strategies σ 1 and σ 2 can be assumed to be memoryless. For any state q ∈ Q, let σ be the strategy defined as follows:

-apply σ 1 until a state in φ 1 is visited, -apply σ 2 for |S| steps, -restart from scratch.

Let us show that σ satisfies φ 1 surely and φ 2 almost-surely from any state in Q. We denote by F i the Büchi states associated with the condition φ i for i ∈ {1, 2}. We start by showing that φ 1 is satisfied surely. Because i) holds it follows that from any state of q ∈ Q, any play compatible with σ 1 visits a state in F 1 ∩ Q in at most |S| steps. Since σ switches back to σ 1 after a finite number of time it follows that a state in F 1 ∩ Q is visited once every 2|S| steps. It follows that φ 1 is surely satisfied.

We show that φ 2 is satisfied almost-surely. Denote by A the set of runs that start from a state in Q and visits a state in F 2 ∩ Q after the |S| first steps. Thanks to ii) we know that under σ 2 we have: P σ2 G (A) ≥ p |S| min , where p min denotes the least positive probability in M . Now since p |S| min is positive and since σ plays according to σ 2 for |S| steps infinitely many times it follows that in almost all runs consistent with σ a state if F 2 is visited infinitely many times. Thus φ 2 is satisfied almost-surely. Now notice that any set of states satisfying φ 1 surely and φ 2 almost-surely satisfies i) and ii), thus Q is the set of all states in M satisfying φ 1 surely and φ 2 almost-surely.

We exhibit now a procedure that computes the largest set of states satisfying i) and ii). For any subset of states S ′ ⊆ S inducing a sub-MDP, we write Sure(S ′ , φ 1 ) to denote an algorithm computing the set of sure winning states for the objective φ 1 . We also write AlmostSure(S ′ , φ 2 ) to denote an algorithm computing set of almost-sure winning states for the objective φ 2 . Note that both Sure(•, φ 1 ) and AlmostSure(•, φ 2 ) always return sets of states that induce sub-MDPs. We define W 1 = S, and W i = AlmostSure(Sure(W i-1 , φ 1 ), φ 2 ). Define W * as the fixpoint of this sequence.

Let us show that from any state in W * there exists a strategy σ surely satisfying φ 1 , and almost-surely satisfying φ 2 . Notice that by definition of Let us distinguish the end-components inside Lose'. We will define events which lead to losing unless the end-component is left. For any MEC e, 1. if e ∩ B = ∅, then any run ρ ∈ proj -1 (F Lose') which enters e, if ρ stays forever inside e, then ρ is losing w.r.t. objective φ. Let us call the set of such runs L e . Thus, when a run enters e, either L e occurs, or e eventually left. 2. If e ∩ B = ∅, then we define a set of runs Z e which are losing. We recall that the second objective in the condition W ′ (abstract MDP in R(A)) is to ensure that every outcome contains infinitely many disjoint factors whose FOG is complete. This can be understood as a Büchi objective in the product MDP R(A) B (the deterministic Büchi automaton B has been defined before, see Lemma 20). We denote this objective by the set of states B ′ . Let us denote by Lose(GF B') the set of states in R(A) that are losing for Controller in the two-player game (R(A) is now viewed as two-player game and not as an MDP) restricted to e w.r.t. objective GF B ′ . Runs that stay infinitely in e must visit infinitely often states of e ∩ Lose(GF B') = ∅ since otherwise we can show that e ⊆ Win ′ (combine σ with a strategy winning the objective GF B', see Lemma 41).

Let q be such a state. As the above objective is considered in a two-player finite-state (Büchi) game, q is losing implies that Perturbator has a finitememory strategy τ to ensure Controller is losing, i.e. a finite lasso whose cycle contains no state in B ′ . In addition, the memory needed is bounded in terms of the size of R(A) B. We can show as we did before that the cycle reached is actually non-aperiodic. We can thus exhibit an integer N f such that the following this lasso during N f steps is impossible if in addition the valuations are always α-far, with α = δ 4(C+1) . Consider now runs in the MDP semantics compatible with σ which belong to proj -1 (F Lose'). Now, when some state in proj -1 (q) is reached, unless e is left before N f steps, with probability at least p N f , the (stochastic) resolutions of non-determinism are compatible with τ , and the run is α-far for N f steps. 8Let us call Z e the set of such runs. We saw earlier that all runs in Z e are losing (c.f. proof of Proposition 15). Since states of Lose(GF B') are visited infinitely often, it follows that when any run enters e, either Z e occurs or e is eventually left.

It follows from the above case by case analysis that non-losing runs almost surely reach bottom end-components. But because a bottom end-component cannot be left, such runs are also losing.

This shows that any run entering Lose' is almost surely losing, as required and yield the completeness of the characterization. ⊓ ⊔

  Fig.1. On the left, a timed automaton from[START_REF] Puri | Dynamical properties of timed automata[END_REF] that is not robustly controllable for the Büchi objective {ℓ2}. In fact, Perturbator can enforce that the value of x be increased by δ at each arrival at ℓ1, thus blocking the run eventually (see[START_REF] Sankur | Robust controller synthesis in timed automata[END_REF]). On the right, a timed automaton that is robustly controllable for the Büchi objective {ℓ1, ℓ2, ℓ3}. We assume that all transitions have the same label. The cycle around ℓ1 cannot be taken forever, as value of x increases due to perturbations. The cycle around ℓ2 can be taken forever, but Controller cannot reach ℓ2 due to the equality x = 1. Controller's strategy is thus to loop forever around ℓ3. This is possible as for both choices of Perturbator in location ℓ4, clock x will be reset, and thus perturbations do not accumulate. If one of the two resets were absent, Perturbator could force the run to always take that branch, and would win the game.

Fig. 3 .

 3 Fig. 3. Proof idea of Lemma 6. Dashed arrows represent cycles.

Theorem 13 .

 13 It is EXPTIME-complete to decide whether for some δ > 0, Controller has a strategy achieving a given Büchi objective almost surely in the stochastic game semantics. Moreover, if C C holds then Controller wins almostsurely; if C P holds then Perturbator wins almost-surely.

  1 and every run in Runs(R(A)[σ], v) contains infinitely many disjoint factors whose FOG is complete. Observe that this combines an almost-sure requirement with a sure requirement. This winning condition is our characterization for almost-sure winning: Proposition 15. Controller wins almost-surely in the MDP semantics of a timed Büchi automaton A iff Controller wins the game (R(A), W ′ ) in v 0 .

  (r ′ ,a)---→ (ℓ ′ , s), as the two following edges:(ℓ, r) ∆ -→ (ℓ, r ′ ) denotes the delay edge, which represents time-elapsing in the timed automaton, and (ℓ, r ′ ) e -→ (ℓ ′ , s) with e = (ℓ, g, a, R, ℓ ′ ) ∈ E is the edge of A used to build the transition (ℓ, r) (r ′ ,a)

Fig. 7 .

 7 Fig. 7. The folded orbit graph of the (non-forgetful) cycle of Fig. 6.

Fig. 8 .

 8 Fig. 8. The folded orbit graph of a forgetful cycle.

Lemma 37 .δ 4 (

 374 Given any δ > 0, and any timed automaton with C clocks, let ε = C+1) . For any state (ℓ, ν), and Controller's valid move (d, a), there exists an interval I ⊆ [dδ, d + δ] such that |I| ≥ ε, and for all d ′ ∈ I, ν + d ′ is ε-far. Proof. After any delay ν d -→ ν ′ , d ≥ δ, chosen by Controller, consider the regions spanned by the set ν ′ + [0, δ]. It is easy to see that this set intersects at most |C| + 1 different regions (See also [5, Lemma 6]), all of which must satisfy the guard by definition of the game. So some region r satisfies ν ′ + [α, β] ⊆ r, for some 0 ≤ α < β ≤ δ with βα ≥ δ |C|+1 . Thus, [α, β] contains an interval with desired properties.

Theorem 13 .

 13 It is EXPTIME-complete to decide whether for some δ > 0, Controller has a strategy achieving a given Büchi objective almost surely in the stochastic game semantics. Moreover, if C C holds then Controller wins almostsurely; if C P holds then Perturbator wins almost-surely.

  The winning condition W is equivalent to C P and C C : 1. Perturbator wins the game (R(A), W) iff property C P holds. 2. Controller wins the game (R(A), W) iff property C C holds. In both cases, a winning strategy for W is also a witness for C C (resp. C P ).

Any timed automaton can be transformed to satisfy this property.

Note this slight modification in the definition of the region automaton.

R Γ (π) (v) denotes here the successors of v in Γ (π).

One can choose p = 1 d8(C+1) where d is the maximal degree of non-determinism. Indeed, with probability at least 1 d the resolution of non-determinism is compatible with τ , and with probability at least 1 8(C+1) , the selection of the perturbation yields an α-far valuation.

⋆ This work was partly supported by ANR projects ECSPER (ANR-2009-JCJC-0069)

and ImpRo (ANR-2010-BLAN-0317), European project Cassting (FP7-ICT-601148), and the ERC starting grant inVEST (FP7-279499).

-P i 0 Q i for i ∈ {1, 2}.

Then P 0 Q.

Proof. Let us write (s, P ′ i ) = CPre 0 π1 ((r i , P i )) and (s, Q ′ i ) = CPre 0 π1 ((r i , Q i )) for i = 1, 2. We rewrite -(r, P ) = CPre 0 π0 ((s, P ′ 1 ) ∩ (s, P ′ 2 )), -and (r, Q) = CPre 0 π0 ((s, Q ′ 1 )) ∩ CPre 0 π0 ((s, Q ′ 2 )). By Lemma 31, we have

We prove the result by induction on |π 0 | ≥ 0. For the base case, assume that π 0 = e consists of one edge. In this case, notice that (r, P ) = CMerge a,r ′ ((s, P ′ 1 ), (s, P ′ 2 )). The result then follows from Lemma 32. Assume |π 0 | > 0 and write π 0 = eπ ′ . Let us write AlmostSure(•, φ 2 ) and Sure(•, φ 2 ) we know that AlmostSure(S ′ , φ 2 ) ⊆ S ′ and Sure(S ′ , φ 2 ) ⊆ S ′ for any sub-MDP S ′ . It follows that AlmostSure(W * , φ 2 ) = W * and Sure(W * , φ 1 ) = W * , thus W * satisfies i) and ii) and from the first part of the proof we obtain that all states in W * satisfy φ 1 surely and φ 2 almost-surely. This shows the correction of our procedure.

We now need to prove that W * contains all states from which there exists a strategy σ surely satisfying φ 1 , and almost-surely satisfying φ 2 . We show that any state outside W * is either not surely winning with respect to φ 1 or not almost-surely winning with respect to φ 2 .

We prove by induction on i > 0 that all states outside W i are losing. This is trivial for i = 1 since W 1 = S. Let s be any state not in W * , and let

). If a) holds then for any strategy σ, either σ is not compatible with W i when started from s, which means it leaves W i , and it is losing by induction; or σ is compatible with W i and there exists an infinite run consistent with σ in the sub-MDP W i-1 and starting at s that is not surely winning with respect to φ 1 . If b) holds, then any strategy σ compatible with the sub-MDP Sure(W i-1 , φ 1 ) is not almost-surely winning with respect to φ 2 . Since strategies that are not compatible with Sure(W i-1 , φ 1 ) are losing as we showed in the case a), we get that no strategy from s satisfies φ 1 surely and φ 2 almost-surely.

Hence, W * is exactly the set of states from which some strategy satisfies φ 1 surely and φ 2 almost surely.

Last, W * can be computed in polynomial time since both AlmostSure(•, φ 2 ) and Sure(•, φ 2 ) can be computed in polynomial time and at each iteration we have

It follows that since R(A) has exponential size, the conditions of Lemma 40 can be decided in exponential time, and exponential-memory strategies exists in (R(A), W ′ ), proving Lemma 16.

Proof of Correctness It remains to prove that these conditions are equivalent with almost-sure winning in the MDP semantics, proving Proposition 15.

We first prove Lemma 42 which allows one to lift a strategy in the MDP semantics to R(A).

Lemma 42. Let σ be any strategy in G MDP δ (A). Let X be a measurable subset of Runs(A, s) with positive probability. There exists a strategy σ in R(A) such that for any path h of R(A),

Proof (of Lemma 42). For any history h, we define the strategy σ by

> 0 and arbitrarily otherwise. We show the required property by induction n ≥ 1, the length of h.

The base case n = 1 is trivial since

, where the value is 1 if r = r 0 and 0 otherwise.

Consider the property holds up to length n. Consider a path h(r, a) of R(A) of length n + 1. We write

Here the second line is by induction. Now, if P σ A,s0 (proj -1 (h) ∩ A) = 0, then we also have

which concludes the proof.

⊓ ⊔

Last, we need to construct a set of paths with nonzero measure which contain infinitely many ε-far factors. We will then use ideas similar to the stochastic game semantics case, once we condition on this event.

Lemma 43. There exists a subset Z of Runs(A, s 0 ) and some η > 0 such that under any strategy σ, P σ G MDP δ (A),s0 (Z) ≥ η. In addition, for every integer N 1 , there exists N 2 ≥ N 1 such that for any run ρ ∈ Z, the run is ε-far during N consecutive steps between positions N 1 and N 2 .

Proof. Assuming the timed automaton A has C clocks, we let ε = δ 4(C+1) . In any configuration (ℓ, ν) reached when playing according to Controller's strategy σ, there exists an interval I ⊆ [-δ, δ] such that |I| ≥ ε, and any perturbation d ′ picked in I is such that the resulting valuation ν + d ′ is ε-far. As a consequence, with probability at least |I| 2δ ≥ 1 8(C+1) > 0, Perturbator picks a delay resulting in an ε-far valuation. Observe also that the selections of perturbations constitute independent events.

We recall the following standard mathematical property on infinite products.

Lemma 44. Let us fix some real number α in the open interval (0, 1). We consider the infinite product ∞ j=1 (1α j ) which is known to be convergent to some number f (α) in the open interval (0, 1).

Let us fix some positive natural integer N . Given an integer j ≥ 1, we consider the following event X j : the perturbations selected by Perturbator at steps j * N + 1, j * N + 2, . . . , (j + 1) * N are such that the resulting valuations are ε-far. By the above observations, the event X j has probability at least ( 1 8(C+1) ) N which is strictly positive, and the events (X j ) j are iid.

We let η = ( 1 8(C+1) ) N . We define an increasing sequence of natural numbers (n k ) k∈N as follows

Observe that as (X j ) j are iid, we have that (Y k ) k are independent events as the intervals of natural numbers [n k-1 + 1, n k ] are disjoint for distinct values of k. The following computations give:

Then, we consider the event Z = k≥1 Y k . As events (Y k ) k are independent, we can easily prove, using Lemma 44: Proposition 15). We first suppose that Controller wins the abstract game (R(A), W ′ ). By Lemma 16, there exists a finite-memory winning strategy σ. By definition of W ′ , every outcome of R(A)[σ] contains infinitely many factors whose FOG is complete. Because condition C 1 is satisfied, this entails that every reachable cycle in R(A)[σ] an aperiodic FOG. Then, we apply the results of Section 5 to derive a positive value of δ and a concrete strategy σ which surely ensures infinite runs, that is, against any choice of the perturbations and the edges (in fact, condition C C holds if we consider a trivial Büchi condition). However, we still need to show that σ satisfies φ almost surely. By construction, the strategy σ ensures that for any path h of R(A) compatible with σ, all runs of G δ (A) compatible with σ are in proj -1 (h), regardless whether the perturbations are chosen randomly or adversarially. It follows that, in the MDP semantics, for any path h, P σ

h). Now, because σ almost surely satisfies φ in R(A), strategy σ almost surely satisfies φ in G MDP δ (A). Conversely, suppose that Controller loses the game (R(A), W ′ ). We proceed by contradiction, and suppose that there exists a winning strategy σ in the concrete game G MDP δ (A). Using Lemmas 42 and 43, we build a strategy σ from σ and Z. The property ensured by Lemma 42 and the fact that σ satisfies φ almost-surely allows to show that σ also does (in R(A)). As Controller loses the game (R(A), W ′ ), this entails that there exist an infinite execution w in R(A)[σ] and a bound N 0 after which no factor of w has a complete FOG. Let N ′ be the integer given by Lemma 43 and N 0 , and consider the prefix w N ′ of w of length N ′ . As Z has positive measure and by Lemma 42, we have that

Moreover, as shown in Section 5, any run ε-far during N consecutive steps along non-aperiodic cycles is necessarily blocking. Thus, with positive probability, strategy σ is losing, contradiction.

⊓ ⊔

Algorithm for limit-sure winning We now show that the characterization for the limit-sure winning is correct, namely: Controller wins limit-surely in the MDP semantics iff Controller can satisfy W ′′ in R(A).

First notice that for any MDP, the set of states satisfying a reachability objective almost-surely can be computed in polynomial time. Thus, Lemma 18 follows.

The proof of Proposition 17 uses the notion of end component. An endcomponent of an MDP is a strongly connected sub-MDP (see [6]). It is wellknown that there are finitely many end-components, and that almost-surely, the set of states and actions seen infinitely often defines an end-component. Because the union of two with non-empty intersection is again an end-component, one can define maximal end-components (MECs).

For any MDP M , and MEC D, we say that a run ρ enters D, if there exists i > 0 such that ρ i ∈ D. We say that ρ leaves D, if there exists j > i such that ρ j ∈ D. A MEC D is bottom if no other MEC D ′ is reachable from D. It is easy to see that in all MDPs, there exists at least one bottom MEC, and for all states s, and strategies σ, runs that leave all non-bottom MECs they enter eventually enter a bottom MEC almost surely.

Proof (of Proposition 17). We first show that if Controller satisfies W ′′ in R(A) from r 0 then he wins in the MDP semantics limit-surely. Suppose that Controller wins the game (R(A), W ′′ ). Then there exists a memoryless strategy σ1 such that any play compatible with σ in R(A) that starts is r 0 reaches almost-surely the set Win ′ , and a finite-memory strategy σ2 satisfying W ′ from states in Win ′ .

Let ε > 0. There exists an integer N such that at step N , with probability at least 1ε, the N -th step of any play consistent with σ1 and starting in r 0 is in the set Win ′ . Consider the unfolding of R(A)[σ 1 ] from the initial vertex of R(A), and of depth N . As we are interested in paths of finite length, one can compute shrinking matrices and an upper bound on δ such that the resulting shrunk zones are non-empty (see Lemma 10). We can thus derive a concrete strategy σ 1 along this finite unfolding, which preserves the probabilities of σ1 . In particular, with probability at least 1ε, the runs compatible with σ 1 have reached the set Win ′ after at most N steps. Using the construction done for the almost-sure case, we know that there exists an upper bound on δ and a concrete strategy σ 2 which wins almost-surely the game G MDP δ (A) w.r.t. the Büchi objective from states in Win ′ . This yields the desired implication.

Let us assume that Controller wins in the MDP semantics limit-surely, and prove that he satisfies W ′′ in R(A) from r 0 . By contradiction, suppose that it is not the case. Consider the set of states of the MDP R(A) from which there is no path to the set Win ′ , and denote this set Lose ′ (observe that this set is absorbing: once entered, one can not leave it). Because R(A) is a finite MDP, and W ′′ is not satisfied almost surely from v 0 , there exists ν > 0 such that for every strategy σ, the set Lose ′ is reached with probability at least ν from v 0 .

Consider ε < ν, and fix some δ > 0 and some strategy σ for G MDP δ (A) such that P σ G MDP δ (A),s0 (φ) ≥ 1ε, which exist by assumption. Let σ given by Lemma 42. By the above remark, it follows that P σ G MDP δ (A),v0 (proj -1 (F Lose')) ≥ ν where the property F Lose' means that a play compatible with σ eventually enters the set Lose'.

We will show that the set Lose' is almost-surely losing w.r.t. objective φ (recall that φ is a Büchi objective with accepting states B) in the MDP semantics, which yields to a contradiction.