Franck Cassez
email: franck.cassez@irccyn.ec-nantes.fr

Alexandre David
email: adavid@cs.aau.dk

Emmanuel Fleury
email: fleury@cs.aau.dk

Kim G Larsen

Didier Lime
email: didier@cs.aau.dk

Efficient On-the-fly Algorithms for the Analysis of Timed Games

In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties 1 . The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [15] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure. Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.

1 Though timed games for long have been known to be decidable there has until now been a lack of efficient and truly on-the-fly algorithms for their analysis.

Introduction

On-the-fly algorithms offer the benefit of settling properties of individual system states (e.g. an initial state) in a local fashion and without necessarily having to generate or examine the entire state-space of the given model. For finite-state (untimed) systems the search for optimal (linear) on-the-fly or local algorithms has been a very active research topic since the end of the 80's [START_REF] Larsen | Efficient Local Correctness Checking[END_REF][START_REF] Andersen | Model Checking and Boolean Graphs[END_REF][START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF] and is one of the most important techniques applied in finite-state model-checkers using enumerative or explicit state-space representation, as is the case with SPIN [START_REF] Holzmann | The SPIN Model Checker[END_REF], which performs on-the-fly model-checking of LTL properties.

Also for timed systems, on-the-fly algorithms have been absolutely crucial to the success of model-checking tools such as Kronos [START_REF] Bozga | Kronos: a Model-Checking Tool for Real-Time Systems[END_REF] and Uppaal [START_REF] Larsen | Uppaal in a Nutshell[END_REF] in their analysis of timed automata based models [START_REF] Alur | A theory of timed automata[END_REF]. Both reachability, safety as well as general liveness properties of such timed models may be decided using on-the-fly algorithms exploring the reachable state-space in a (symbolic) forward manner with the possibility of early termination. More recently, timed automata technology has been successfully applied to optimal scheduling problems with guiding and pruning heuristics being added to yield on-the-fly algorithms which quickly lead to near-optimal (time-or cost-wise) schedules [START_REF] Asarin | As Soon as Possible: Time Optimal Control for Timed Automata[END_REF][START_REF] Alur | Optimal Paths in Weighted Timed Automata[END_REF][START_REF] La Torre | Optimal-Reachability and Control for Acyclic Weighted Timed Automata[END_REF][START_REF] Rasmussen | Resource-optimal scheduling using priced timed automata[END_REF].

We consider timed game automata and how to x > 1;u1

x < 1 u2 x := 0

x ≥ 2;c2

x < 1 u3 c3

x ≤ 1;c4 Fig. 1. A Timed Game Automaton decide the existence of a winning strategy w.r.t. reachability or safety. As an example, consider the timed game automaton A of Fig. 1 consisting of a timed automaton with one clock x and two types of edges: controllable (c i ) and uncontrollable (u i ). The reachability game consists in finding a strategy for a controller, i.e. when to take the controllable transitions that will guarantee that the system, regardless of when and if the opponent chooses to take uncontrollable transitions, will eventually end up in the location Goal.

Obviously, for all initial states of the form (ℓ 1 , x) with x ≤ 1 there is such a winning strategy 2 .

Though such timed game automata for long have been known to be decidable [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF][START_REF] Asarin | Controller Synthesis for Timed Automata[END_REF][START_REF] Alfaro | Symbolic Algorithms for Infinite-State Games[END_REF] there is still a lack of efficient and truly on-the-fly algorithms for their analysis. Most of the suggested algorithms are based on backwards fix-point computations of the set of winning states [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF][START_REF] Asarin | Controller Synthesis for Timed Automata[END_REF][START_REF] Alfaro | Symbolic Algorithms for Infinite-State Games[END_REF]. In contrast, the on-the-fly algorithms used for model-checking timed automata models (w.r.t. reachability) makes a forward symbolic state-space exploration resulting in the so-called simulation graph. However, the simulation graph is by itself too abstract to be used as the basis for an on-the-fly algorithm for computing winning strategies. Fig. 2 (a) gives the simulation graph of the timed game automata of Fig. 1, which incorrectly classifies the initial state as being uncontrollable when viewed as a finite-state game.

As a remedy to this problem, the authors of [START_REF] Tripakis | On-the-Fly Controller Synthesis for Discrete and Timed Systems[END_REF][START_REF] Altisen | Tools for controller synthesis of timed systems[END_REF] propose a partially onthe-fly method for solving reachability games for a timed game automaton A. However, this method involves an extremely expensive preprocessing step in which the quotient graph of the dense time transition system S A w.r.t. timeabstracted bisimulation 3 needs to be built. Once obtained this quotient graph may be used with any on-the-fly game-solving algorithm for untimed (finitestate) systems. As an illustration, Fig. 2 (b) gives the time abstracted quotient graph for the timed game automaton of Fig. 1. It should be easy for the reader to see that the initial state will now (correctly) be classified as controllable.

ℓ1, x ≥ 0 ℓ2, x ≥ 0 ℓ3, x ≥ 0 ℓ4, x ≥ 0 Goal, x ≥ 2 Bad, x ≥ 1 c1 u1 u2 c2 u3 c3 c4 (a) Simulation Graph 1, x < 1 ℓ1, x = 1 ℓ1, x > 1 ℓ2, x < 1 ℓ2, x = 1 ℓ2, x > 1 ℓ3, x < 1 ℓ3, x = 1 ℓ3, x > 1 ℓ4, x < 1 ℓ4, x = 1 ℓ4, x > 1 Goal, x ≥ 2 ℓ5, x > 1 λ λ u1 c1 c1 λ λ λ, c2 u3 λ λ c3 c3 λ λ u2 c4 c4 (b) Time-abstracted Quotient Graph
In this paper, we propose an efficient, truly on-the-fly algorithm for the computation of winning states for timed game automata. Our algorithm is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate before having explored the entire state-space, i.e. as soon as a winning strategy has been identified. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure.

The rest of the paper is organized as follows. Section 2 provides definitions and preliminaries about timed game automata and classic backwards algorithm for solving them. Section 3 presents our instantiation of the general on-the-fly algorithm of Liu & Smolka [START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF] to untimed reachability games. Then, in Section 4, we present our symbolic extension of this algorithm, providing a first forward, zone-based and fully on-the-fly algorithm for solving timed reachability games. Section 5 discusses few optimizations of the basic algorithm and how to apply the algorithm to determine time-optimal winning strategies. Section 6 presents experimental evaluation of an efficient implementation of the algorithm to determine (time-optimal) winning strategies. The performance results obtained are very encouraging. Finally, Section 7 presents conclusion and future work and all proofs can be found in the Appendix .

Backward Algorithms for Solving Timed Games

Timed Game Automata [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] (TGA) were introduced for control problems on timed systems. This section recalls basic results of controller synthesis for TGA.

Let X be a finite set of real-valued variables called clocks. We note C(X) the set of constraints ϕ generated by the grammar:

ϕ ::= x ∼ k | x -y ∼ k | ϕ ∧ ϕ
where k ∈ Z, x, y ∈ X and ∼∈ {<, ≤, =, >, ≥}. B(X) is the subset of C(X) that uses only rectangular constraints of the form x ∼ k. A valuation of the variables in X is a mapping X → R ≥0 (thus R X ≥0 ). We write 0 for the valuation that assigns 0 to each clock. For Y ⊆ X, we denote by v[Y ] the valuation assigning 0 (resp. v(x)) for any

x ∈ Y (resp. x ∈ X \ Y ). We denote v + δ for δ ∈ R ≥0 the valuation s.t. for all x ∈ X, (v + δ)(x) = v(x) + δ. For g ∈ C(X) and v ∈ R X ≥0 , we write v |= g if v satisfies g and [[g]] denotes the set of valuations {v ∈ R X ≥0 | v |= g}. A zone Z is a subset of R X ≥0 s.t. [[g]]= Z for some g ∈ C(X).

Timed Game Automata & Simulation Graph

Definition 1 (Timed Automaton [START_REF] Alur | A theory of timed automata[END_REF]). A Timed Automaton (TA) is a tuple A = (L, ℓ 0 , Act, X, E, Inv) where L is a finite set of locations, ℓ 0 ∈ L is the initial location, Act is the set of actions, X is a finite set of real-valued clocks,

E ⊆ L × B(X) × Act × 2 X × L is a finite set of transitions, Inv : L → B(X)
associates to each location its invariant.

A state of a TA is a pair (ℓ, v) ∈ L × R X ≥0 that consists of a discrete part and a valuation of the clocks. From a state (ℓ, v) ∈ L × R X ≥0 s.t. v |= Inv(ℓ), a TA can either let time progress or do a discrete transition and reach a new state. This is defined by the transition relation -→ built as follows: for a ∈ Act,

(ℓ, v) a --→ (ℓ ′ , v ′ ) if there exists a transition ℓ g,a,Y -----→ ℓ ′ in E s.t. v |= g, v ′ = v[Y ] and v ′ |= Inv(ℓ ′ ); for δ ≥ 0, (ℓ, v) δ --→ (ℓ, v ′ ) if v ′ = v + δ and v, v ′ ∈[[Inv(ℓ)]].
Thus the semantics of a TA is the labeled transition system S A = (Q, q 0 , -→) where Q = L × R X ≥0 , q 0 = (ℓ 0 , 0) and the set of labels is Act ∪ R ≥0 . A run of a timed automaton A is a sequence of alternating time and discrete transitions in S A . We use Runs((ℓ, v), A) for the set of runs that start in (ℓ, v). We write Runs(A) for Runs((ℓ 0 , 0), A). If ρ is a finite run we denote last (ρ) the last state of the run and Duration(ρ) the total elapsed time all along the run.

The analysis of TA is based on the exploration of a finite graph, the simulation graph, where the nodes are symbolic states; a symbolic state is a pair (ℓ, Z) where

ℓ ∈ L and Z is a zone of R X ≥0 . Let X ⊆ Q and a ∈ Act we define the a-successor of X by Post a (X) = {(ℓ ′ , v ′ ) | ∃(ℓ, v) ∈ X, (ℓ, v) a --→ (ℓ ′ , v ′ )} and the a-predecessor Pred a (X) = {(ℓ, v) | ∃(ℓ ′ , v ′ ) ∈ X, (ℓ, v) a --→ (ℓ ′ , v ′ )}.
The timed successors and predecessors of X are respectively defined by

X ր = {(ℓ, v + d) | (ℓ, v) ∈ X∩ [[Inv(ℓ)]], (ℓ, v + d) ∈[[Inv(ℓ)]], d ∈ R ≥0 } and X ւ = {(ℓ, v -d) | (ℓ, v) ∈ X, d ∈ R ≥0 }.
Let → be the relation defined on symbolic states by: (ℓ, Z)

a --→ (ℓ ′ , Z ′ ) if (ℓ, g, a, Y, ℓ ′ ) ∈ E and Z ′ = ((Z∩ [[g]])[Y ]) ր .
The simulation graph SG(A) of A is defined as the transition system (Z(Q), S 0 , →), where Z(Q) is the set of zones of Q, S 0 = (({ℓ 0 , 0} ր )∩ [[Inv(ℓ 0 )]] and → defined as above.

Definition 2 (Timed Game Automaton [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]). A Timed Game Automaton (TGA) G is a timed automaton with its set of actions Act partitioned into controllable (Act c ) and uncontrollable (Act u ) actions.

Safety and Reachability Games

Given a TGA G and a set of states K ⊆ L × R X ≥0 the reachability control problem consists in finding a strategy f s.t. G supervised by f enforces K. The safety control problem is the dual asking for the strategy to constantly avoid K. By "a reachability game (G, K)" (resp. safety) we refer to the reachability (resp. safety) control problem for G and K.

Let (G, K) be a reachability (resp. safety) game. A finite or infinite (ruling out runs with an infinite number of consecutive time transitions of duration 0)

run ρ = (ℓ 0 , v 0 ) e0 -→ (ℓ 1 , v 1 ) e1 -→ • • • en -→ (ℓ n+1 , v n+1 ) • • • in Runs(G) is winning if there is some k ≥ 0 s.t. (ℓ k , v k ) ∈ K (resp. for all k ≥ 0 s.t. (ℓ k , v k ) ∈ K). The set of winning runs in G from (ℓ, v) is denoted WinRuns((ℓ, v), G).
For reachability games we assume w.l.o.g. that the goal is a particular location Goal. For safety games the goal is a set a locations to avoid.

The formal definition of the control problems is based on the definitions of strategies and outcomes. A strategy [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] is a function that during the course of the game constantly gives information as to what the controller should do in order to win the game. In a given situation, the strategy could suggest the controller to either i) "do a particular controllable action" or ii) "do nothing at this point in time, just wait" which will be denoted by the special symbol λ.

Definition 3 (Strategy

). Let G = (L, ℓ 0 , Act, X, E, Inv) be a TGA. A strategy f over G is a partial function from Runs(G) to Act c ∪ {λ} s.t. for every finite run ρ, if f (ρ) ∈ Act c then last (ρ) f (ρ) ---→ SG (ℓ ′ , v ′ ) for some (ℓ ′ , v ′ ). We denote Strat(G) the set of strategies over G. A strategy f is state-based whenever ∀ρ, ρ ′ ∈ Runs(G), last (ρ) = last (ρ ′ ) implies that f (ρ) = f (ρ ′ ).
Statebased strategies are also called memoryless strategies in game theory [START_REF] Alfaro | Symbolic Algorithms for Infinite-State Games[END_REF][START_REF] Thomas | On the Synthesis of Strategies in Infinite Games[END_REF].

The restricted behavior of a TGA G controlled with some strategy f is defined by the notion of outcome [START_REF] Alfaro | Symbolic Algorithms for Infinite-State Games[END_REF]. Definition 4 (Outcome). Let G = (L, ℓ 0 , Act, X, E, Inv) be a TGA and f a strategy over G. The outcome Outcome(q, f ) of f from q in S G is the subset of Runs(q, G) defined inductively by:

-q ∈ Outcome(q, f ), -if ρ ∈ Outcome(q, f ) then ρ ′ = ρ e --→ q ′ ∈ Outcome(q, f ) if ρ ′ ∈ Runs(q, G)
and one of the following three conditions hold: 1. e ∈ Act u , 2. e ∈ Act c and e = f (ρ),

3. e ∈ R ≥0 and ∀0 ≤ e ′ < e, ∃q ′′ ∈ Q s.t. last (ρ) e ′ --→ q ′′ ∧f (ρ e ′ --→ q ′′ ) = λ.
-for an infinite run ρ, ρ ∈ Outcome(q, f ) if all the finite prefixes of ρ are in Outcome(q, f ).

We assume that uncontrollable actions can only spoil the game and the controller has to do some controllable action to win [START_REF] Asarin | Controller Synthesis for Timed Automata[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF][START_REF] La Torre | Optimal-Reachability and Control for Acyclic Weighted Timed Automata[END_REF]. In other words, an uncontrollable action cannot be forced to happen in G. Thus, a run may end in a state where only uncontrollable actions can be taken. Moreover we focus on reachability games and assume K = {Goal} × R X ≥0 . A maximal run ρ is either an infinite run (supposing no infinite sequence of delay transitions of duration 0) or a finite run ρ that satisfies either i)

last (ρ) ∈ K or ii) if ρ a --→ then a ∈ Act u (i.e.
the only possible next discrete actions from last (ρ), if any, are uncontrollable actions). A strategy f is winning from q if all maximal runs in Outcome(q, f ) are in WinRuns(q, G). A state q in a TGA G is winning if there exists a winning strategy f from q in G. We denote by W(G) the set of winning states in G and WinStrat(q, G) the set of winning strategies from q over G.

Backwards Algorithms for Solving Timed Games

Let G = (L, ℓ 0 , Act, X, E, Inv) be a TGA. For reachability games, the computation of the winning states is based on the definition of a controllable predecessor operator [START_REF] Alfaro | Symbolic Algorithms for Infinite-State Games[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]. The controllable and uncontrollable discrete predecessors of X are defined by cPred(X) = c∈Actc Pred c (X) and uPred(X) = u∈Actu Pred u (X). A notion of safe timed predecessors of a set X w.r.t. a set Y is also needed. Intuitively a state q is in Pred t (X, Y ) if from q we can reach q ′ ∈ X by time elapsing and along the path from q to q ′ we avoid Y . Formally this is defined by:

Pred t (X, Y ) = {q ∈ Q | ∃δ ∈ R ≥0 s.t. q δ -→ q ′ , q ′ ∈ X and Post [0,δ] (q) ⊆ Y } (1)
where

Post [0,δ] (q) = {q ′ ∈ Q | ∃t ∈ [0, δ] s.t. q t --→ q ′ } and Y = Q \ Y . The controllable predecessors operator π is defined as follows 4 : π(X) = Pred t X ∪ cPred(X), uPred(X) (2)
Let (G, K) be a reachability game, if S is a finite union of symbolic states, then π(S) is again a finite union of symbolic states. Moreover the iterative process given by W 0 = K and W n+1 = π(W n ) will converge after finitely many steps for TGA [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] and the least fixed point obtained is W * . It is also proved in [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] that W * = W(G). Note also that W * is the maximal set of winning states of G i.e. a state is winning iff it is in W * . Thus there is a winning strategy in G iff (ℓ 0 , 0) ∈ W * . Altogether this gives a symbolic algorithm for solving reachability games. Extracting strategies can be done using the winning set of states W * . For safety games (G, K), it suffices to swap the roles of the players leading to a game G and solve a reachability game (G, K). If the winning set of states for (G, K) is W then the winning set of states of (G, K) is W .

3 On-the-fly Algorithm for Untimed Games

For finite-state systems, on-the-fly model-checking algorithms has been an active and successful research area since the end of the 80's, with the algorithm proposed by Liu & Smolka [START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF] being particularly elegant (and optimal). We present here our instantiation of this algorithm to untimed reachability games. We consider untimed games as a restricted class of timed games with only finitely many states Q and with only discrete actions, i.e. the set of labels is Act. Hence (memoryless) strategies simplifies to a choice of controllable action given the current state, i.e. f : Q -→ Act c . For (untimed) reachability games we assume a designated set Goal of goal-states and the purpose of the analysis is to decide the existence of a strategy f where all runs contains at least one state from Goal. Now, our instantiation OTFUR of the local algorithm by Liu & Smolka to untimed reachability games is given in Fig. 3. This algorithm is based on a waiting-list, W aiting ⊆ E of edges waiting to be explored together with a passed-list P assed ⊆ Q containing the states that have been encountered so far. Information about the current winning status of a state is given by a function W in : P assed → {0, 1}, where W in[q] is initialized to 0 and later potentially upgraded to 1 when the winning status of successors to q change from 0 to 1. To activate the reevaluation of the winning status of states, each state q has an associated set of edges Depend[q] depending on it: at any stage Depend[q] contains all edges (q ′ , α, q) that was encountered at a moment when W in[q] = 0 and where the winning status of the source state q ′ must be scheduled for reevaluation at the movement W in[q] = 1 becomes true. We refer to [START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF] for the formal proof of correctness of this algorithm summarized by the following theorem:

Theorem 1 ( [START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF]). Upon termination of running the algorithm OTFUR on a given untimed game G the following holds:

1. If q ∈ P assed and W in[q] = 1 then q ∈ W(G); 2. If W aiting = ∅ and W in[q] = 0 then q ∈ W(G).

In fact, the first property is an invariant of the while-statement holding after each iteration. Also, the algorithm is optimal in that it has linear time complexity in the size of the underlying untimed game: it is easy to see that each edge e = (q, α, q ′ ) will be added to W aiting at most twice, the first time q is encountered (and added to P assed) and the second time when W in[q ′ ] changes winning status from 0 to 1 5 . 5 To obtain an algorithm running in linear time in the size of G (i.e. |Q| + |E|) it is important that the reevaluation of the winning status of a state q does not directly involve (repeated and expensive) evaluation of the large boolean expression for W in * .

In a practice, this may be avoided by adding a boolean bq and a counter cq recording the existence of a winning, controllable successor of q, and the number of winning, uncontrollable successor of q.

Initialization:

P assed ← {q0}; W aiting ← {(q0, α, q ′ ) | α ∈ Act q α -→ q ′ }; W in[q0] ← (q0 ∈ Goal ? 1 : 0); Depend[q0] ← ∅; Main: while ((W aiting = ∅) ∧ W in[q0] = 1)
) do e = (q, α, q ′ ) ← pop(W aiting); if q ′ ∈ P assed then P assed ← P assed ∪ {q ′ }; Now let us turn our attention to the timed case and present our symbolic extension of the algorithm of Liu & Smolka providing a zone-based forward and onthe-fly algorithm for solving timed reachability games. The algorithm, SOTFTR, is given in Fig. 4 and may be viewed as an interleaved combination of forward computation of the simulation graph of the timed game automaton together with back-propagation of information of winning states. As in the untimed case the algorithm is based on a waiting-list, W aiting, of edges in the simulation-graph to be explored, and a passed-list, P assed, containing all the symbolic states of the simulation-graph encountered so far by the algorithm.

Depend[q ′ ] ← {(q, α, q ′ )}; W in[q ′ ] ← (q ′ ∈ Goal ? 1 : 0); W aiting ← W aiting ∪ {(q ′ , α, q ′′ ) | q ′ α -→ q ′′ }; if W in[q ′ ] then W aiting ← W aiting ∪ {e}; else (* reevaluate *) W in * ← V q u -→u W in[u] ∧ W q c - →w W in[w]; if W in * then W aiting ← W aiting ∪ Depend[q]; W in[q] ← 1; if W in[q ′ ] = 0 then Depend[q ′ ] ← Depend[q ′ ] ∪ {e}; endif endwhile
The crucial point of our symbolic extension is that the winning status W in[q] of an individual state q is replaced by a set W in[S] ⊆ S identifying the subset of the symbolic state S which is currently known to be winning. The set Depend[S] indicates the set of edges (or predecessors of S) which must be reevaluated (i.e. added to W aiting) when new information about W in[S] is obtained (i.e. when W in [S] W in * ). Whenever an edge e = (S, α, S ′ ) is considered with S ′ ∈ P assed, the edge e is added to the dependency set of S ′ in order that possible future information about additional winning states within S ′ may also be back-propagated to S. In Table 1, we illustrate the forward exploration and backwards propagation steps of the algorithm. The correctness of the symbolic on-the-fly algorithm SOTFTR is given by the following lemma and theorem, the rigorous proofs of which can be found in the appendix.

Initialization: P assed ← {S0} where S0 = {(ℓ0, 0)} ր ; W aiting ← {(S0, α, S ′ ) | S ′ = Postα(S0) ր }; W in[S0] ← S0 ∩ ({Goal} × R X ≥0 ); Depend[S0] ← ∅; Main: while ((W aiting = ∅) ∧ (s0 ∈ W in[S0])) do e = (S, α, S ′ ) ← pop(W aiting); if S ′ ∈ P assed then P assed ← P assed ∪ {S ′ }; Depend[S ′ ] ← {(S, α, S ′ )}; W in[S ′ ] ← S ′ ∩ ({Goal} × R X ≥0 ); W aiting ← W aiting ∪ {(S ′ , α, S ′′ ) | S ′′ = Postα(S ′ ) ր }; if W in[S ′ ] = ∅ then W aiting ← W aiting ∪ {e}; else (* reevaluate *) a W in * ← Predt(W in[S]∪ S S c - →T Predc(W in[T ]), S S u -→T Predu(T \ W in[T ])) ∩ S; if (W in[S] W in * ) then W aiting ← W aiting ∪ Depend[S]; W in[S] ← W in * ; Depend[S ′ ] ← Depend[S ′ ] ∪ {e}; endif endwhile a When T ∈ P assed,W in[T ] = ∅
Table 1. Running SOTFTG Lemma 1. The while-loop of algorithm SOTFTR has the following invariance properties when running on a timed game automaton G:

1. For any S ∈ P assed if S α -→ S ′ then either (S, α, S ′ ) ∈ W aiting or S ′ ∈ P assed and (S, α, S ′ ) ∈ Depend[S ′ ] 2. If q ∈ W in[S] for some S ∈ P assed then q ∈ W(G) 3. If q ∈ S \ W in[S] for some S ∈ P assed then either e ∈ W aiting for some e = (S, α, S ′ ) with S ′ ∈ P assed,

or -q ∈ Pred t W in[S] ∪ S c -→T Pred c (W in[T ]), S u -→T Pred u (T \ W in[T ]) .
Theorem 2. Upon termination of running the algorithm SOTFTR on a given timed game automaton G the following holds:

1. If q ∈ W in[S] for some S ∈ P assed then q ∈ W(G); 2. If W aiting = ∅, q ∈ S \ W in[S] for some S ∈ P assed then q ∈ W(G).

Termination of the algorithm SOTFTR is guaranteed by the finiteness of symbolic states 6 and the fact that each edge (S, α, T ) will be present in the W aiting-list at most 1 + |T | times, where |T | is the number of regions of T : (S, α, T ) will be in W aiting the first time that S is encountered and subsequently each time the value of W in[T ] increases. Now, any given region may be contained in several symbolic states of the simulation graph (due to overlap). Thus the SOTFTR algorithm is not linear in the region-graph and hence not theoretically optimal, as an algorithm with linear worst-case time-complexity could be obtained by applying the untimed algorithm directly to the regiongraph. However, this is only a theoretical result and, as we shall see, the use of zones yields very encouraging performance results in practice, as is the case for reachability analysis of timed automata.

Implementation, Optimizations and Extensions

Implementation of the Pred t Operator with Zones

In order to be efficient, the algorithm SOTFTR manipulates zones. However, while a forward step always gives a single zone as a result, the Pred t operator does not. So, given a symbolic state S, W in[S] is, in general, an union of zones (and so is S \ W in[S]). As a consequence, we now give two results, which allow us to handle unions of zones (Theorem 3) and to define the computation of Pred t in terms of basic operations on zones (Theorem 4). Theorem 3. The following distribution law holds:

Pred t ( i G i , j B j ) = i j Pred t (G i , B) (3)
Theorem 4. If B is a convex set, then the Pred t operator defined in equation ( 1) can be expressed as:

Pred t (G, B) = (G ւ \ B ւ ) ∪ ((G ∩ B ւ ) \ B) ւ (4)

Optimizations

Zone Inclusion. When we explore forward the automaton, we check if any newly generated symbolic state S ′ belongs to the passed list: S ′ ∈ P assed. As an optimization we may instead use the classical inclusion check: ∃S ′′ ∈ P assed s.t. S ′ ⊆ S ′′ , in which case, S ′ is discarded and we update the dependency graph as well. Indeed, new information learned from the successors of S ′′ can be new information on S ′ but not necessarily. This introduces an overhead in the sense that we may back-propagate information for nothing. On the other hand, back-propagating only the relevant information would be unnecessarily complex and would void most of the memory gain introduced by the use of inclusion. In practice, the reduction of the number of forward steps obtained by the inclusion check pays off for large systems and is a little overhead otherwise, as shown in our experiments.

Losing states. In the case of reachability games we can sometimes decide at an early stage that a state q is losing (i.e. q ∈ W(S G )), either because it is given as a part of the model in the same way as goal states, or because it is deadlock state, which is not in the set of goal states.

The detection of such losing states has a two-fold benefit. First, we can stop the forward exploration on these states, since we know that we have lost (in the case of a user-defined non-deadlock losing state). Second, we can back-propagate these losing states in the same way as we do for winning states and stop the algorithm if we have the initial state s 0 ∈ Lose[S 0 ], where Lose[S] is the subset of the symbolic state S currently known to be losing. In some cases, this can bring a big benefit, illustrated by Fig. 1, if the guard x < 1 is changed to true in the edge from ℓ 1 to ℓ 5 .

Pruning. In the basic algorithm early termination takes place when the initial state is known to be winning (i.e. s 0 ∈ W in[S 0 ]). However, we may extend this principle to other parts of the algorithm. In particular, we can add the condition that whenever an edge e = (S, α, S ′ ) is selected and it turns out that W in[S] = S then we may safely skip the rest of the while loop as we know that no further knowledge on the winning states of S can be gained. In doing so, we prune unnecessary continued forward exploration and/or expensive reevaluation. When we back-propagate losing states as described previously, the condition naturally extends to W in[S] ∪ Lose[S] = S.

Time Optimal Strategy Synthesis

Time-optimality for reachability games consists in computing the best (optimal) time the controller can guarantee to reach the Goal location: if t * is the optimaltime, the controller has a strategy that guarantees to reach location Goal within t * time units whatever the opponent is doing, and moreover, the controller has no strategy to guarantee this for any t < t * .

First consider the following problem: decide whether z 5 the controller has a strategy to reach location Goal within B time units. To solve this problem, we just add a fresh clock z to the TGA G and the invariant Inv(ℓ) ≡ z ≤ B for all locations ℓ with z being unconstrained in the initial state. Then we compute the set of winning states of this game and check that (ℓ 0 , 0, z = 0) is actually a winning state. If not, try with some B ′ > B. Otherwise we know that the controller can guarantee to reach Goal within B time units . . . but in addition we have the optimal-time to reach Goal 7 . Indeed, when computing the winning set of states W * on the TGA G augmented with the z clock (being initially unconstrained), we have the maximal set of winning states. This means that we obtain some (ℓ 0 , Z 0 ) ∈ W * and (ℓ 0 , 0, z = 0) ∈ (ℓ 0 , Z 0 ). But Z 0 ∩{(ℓ 0 , 0)} gives us for free the optimal-time to reach Goal. Assume I = Z 0 ∩ {(ℓ 0 , 0)}, then 0 ∈ I and the upper bound of I is less than B. This means that starting in (ℓ 0 , 0) with z ∈ I the controller can guarantee to reach Goal within B time units. And as W * is the maximal set of winning states, starting with z ∈ I cannot guarantee this any more. Assume I = [0, b]. The optimal-time is then t * = Bb. If it turns out that I is right open [0, b[, we even know more: that this optimal time t * cannot be achieved by any strategy, but we can reach Goal in a time arbitrarily close to t * . On the example of Fig. 1, if we choose B = 5 we obtain a closed interval I = [0, 3] giving the optimal time t * = 2 to reach Goal (Fig. 5). Moreover we know that there is a strategy that guarantees this optimal.

Experiments

Several versions of the described timed game reachability algorithm have been implemented: with or without inclusion checking between zones, with or without back-propagation of the losing states, and with or without pruning. To benchmark the implementations we used the Production Cell [START_REF] Lewerentz | Production Cell: A Comparative Study in Formal Specification and Verification[END_REF][START_REF] Melcher | Controller Synthesis for the "Production Cell" Case Study[END_REF] case study (Fig. 6). Unprocessed plates arrive on a feeding belt, are taken by a robot to a press, are processed, and are taken away to a departure belt. The robot has two arms (A and B) to take and release the plates and its actions are controllable, except for the time needed to rotate. The arrival of the plates and the press are uncontrollable.

We run experiments on a dual- 2 shows the obtained results. The tests are done with varying number of plates from 2 to 7, and with controllable (win) and uncontrollable (lose) configurations. The models contain from 4 to 10 clocks.

0 0 0 0 0 1 1
The inclusion checking of zones is shown to be an important optimization. Furthermore, activating pruning, which really exploits that the algorithm is on-the-fly, is useful in practice: the algorithm really terminates earlier. The results for time optimal reachability confirm that the algorithm is exploring the whole state-space and is comparable to exploring without pruning. We stress in the tables the best result obtained for every configuration: it turns out that propagating back the losing states has a significant overhead that pays off for large systems, i.e. it is clearly better from 6 plates.

The state-space grows exponentially with respect to the number of plates but the algorithm keeps up linearly with it, which is shown on Fig. 7 pre + post8 . These results show that the algorithm based on zones behaves well despite the fact that zones are (in theory) worse than regions.

Conclusion and Future Work

In this paper we have introduced what we believe is the first completely on-thefly algorithm for solving timed games. For its efficient implementation we have used zones as the main datastructure, and we have applied decisive optimizations to take full advantage of the on-the-fly nature of our algorithm and its zone representation. Experiments have shown that an implementation based on zones is feasible and with encouraging performances w.r.t. the complexity of the problem. Finally, we have exhibited how to obtain the time optimal strategies with minor additions to our algorithm (essentially book-keeping).

We are working on an improved version of the implementation to distribute it and use the Uppaal GUI augmented with (un)controllable transitions. We are investigating more aggressive abstractions for the underlying simulation graph computed by our algorithm and efficient guiding of the search, in particular for optimal strategies. Our algorithm is well suited for distributed implementation by its use of unordered waiting-list and there are plans to pursue this directions as has been done for Uppaal [START_REF] Behrmann | Distributed reachability analysis in timed automata[END_REF]. We are also investigating how to extract strategies and represent them compactly with CDDs (Clock Decision Diagrams).

A Proofs of Theorems

Lemma 1. The while-loop of algorithm SOTFTR has the following invariance properties when running on a timed game automaton G:

1. For any S ∈ P assed if S α -→ S ′ then either (S, α, S ′ ) ∈ W aiting or S ′ ∈ P assed and (S, α, S ′ ) ∈ Depend[S ′ ]. 2. If q ∈ W in[S] for some S ∈ P assed then q ∈ W(G) 3. If q ∈ S \ W in[S] for some S ∈ P assed then either e ∈ W aiting for some e = (S, α, S ′ ) with S ′ ∈ P assed,

or -q ∈ Pred t W in[S] ∪ S c -→T Pred c (W in[T ]), S u -→T Pred u (T \ W in[T ]) .
Proof. Consider the first loop invariant. Upon entry at the while-loop the invariant is true as (S, α, S ′ ) ∈ W aiting for all symbolic successors of S 0 . Assume that the invariant property holds after n iterations the loop and let ( * S, α, S ′ ) be the edge from W aiting dealt with during the the next ((n + 1)'th) iteration. If S ′ ∈ P assed before the iteration then S ′ ∈ P assed and (S, α, S ′ ) ∈ Depend[S ′ ] after the iteration. Also all successors of S ′ are added to W aiting ensuring that the invariant holds after the iteration. If S ′ ∈ P assed before the iteration then obviously S ′ ∈ Depend[S ′ ] after the iteration due to last statement of the reevaluate-branch. Consider the third loop invariant. First, in any given state of the program and for S a symbolic state φ(S) will denote the value of q

∈ Pred t W in[S] ∪ S c -→T Pred c (W in[T ]), S u -→T Pred u (T \W in[T ]
) . Upon entry of the while-loop only S 0 ∈ P assed and the property trivially holds as either S 0 is fully winning, as our goal set is based on locations (and hence q ∈ S 0 \ W in[S 0 ] is impossible), or S 0 has symbolic successors which are then in the waiting list or S 0 has no symbolic successor in which case q ∈ φ(S 0 ) obviously holds. Now assume that the property holds after n iterations (we will add n as a superscript to indicate the value at a particular variable after the n'th iteration) and let us prove that it holds after iteration n + 1. During this last iteration an edge (S, α, S ′ ) from W aiting n is processed. There are two cases to be considered depending on which branch of the while-body has been taken, i.e. either S ′ ∈ P assed n or S ′ ∈ P assed n .

Let us first consider the latter, i.e. S ′ ∈ P assed n . Let q ∈ T \ W in n+1 [T ] for some T ∈ P assed n+1 . If S ′ is not a symbolic successor of T then, as φ(T ) and the contents of W aiting and Depend w.r.t. T are unchanged, the desired property holds after the iteration due to the induction hypothesis. If T β -→ S ′ and T = S then by invariance property 1. (T, β, S ′ ) ∈ W aiting n (as S ′ ∈ P assed n the second options of 1. is not an option) and hence (T, β, S ′ ) ∈ W aiting n+1 . For the case T = S and S ′ ∩ {Goal} × R X ≥0 = ∅, the value of φ(T ) is the same before and after the iteration. Thus the induction hypothesis ensures that either f ∈ W aiting for some edge f = (T, γ, T ′ ) both before and after the iteration or q ∈ φ(T ) both before and after the iteration. In case T = S and S ′ ∩ {Goal} × R X ≥0 = ∅, the edge (S, α, S ′ ) = (T, α, S ′ ) is being put back into the W aiting-list ensuring that the property holds.

Let us now consider the case when the processed edge (S, α, S ′ ) is of the type S ′ ∈ P assed n . Let q ∈ T \ W in n+1 [T ] for some T ∈ P assed n+1 : Assume that T = S and that S is not a symbolic successor of T . Then by induction hypothesis the property trivially holds after the iteration. If T = S and T β -→ S then by the invariance property 1. either (T, β, S) ∈ W aiting n or (T, β, S) ∈ Depend n [S]. In the first case we satisfy the invariant property as also (T, β, S) ∈ W aiting n+1 . In the second case the program ensures that (T, β, S) ∈ W aiting n+1 in case W in n+1 [S] W in n [S]. Otherwise, φ(T ) is unchanged by the iteration, and hence by the induction hypothesis either (T, γ, T ′ ) ∈ W aiting for some T ′ ∈ P assed or q ∈ φ(T ) both before and after the iteration. If T = S then our assumption is that q ∈ S \ W in n+1 [S]. Obviously by the update of W in[S] to φ(S) which has taken place during the iteration it is clear that then q ∈ φ(S) = φ(T ).

⊓ ⊔ Theorem 2. Upon termination of running the algorithm SOTFTR on a given timed game automaton G the following holds:

1. If q ∈ W in[S] for some S ∈ P assed then q ∈ W(G); 2. If W aiting = ∅, q ∈ S \ W in[S] for some S ∈ P assed then q ∈ W(G).

Proof. By 1. of Lemma 1 it certainly holds that if q ∈ W in[S] for some S ∈ P assed then q ∈ W(G).

To show that q ∈ W(G) in case q ∈ S \ W in[S] for some S ∈ P assed when W aiting = ∅, we consider the following set L of states based on P assed and W in upon termination: L = {q | ∃S ∈ P assed. q ∈ S \ W in[S]} and let M = Q \ L, where Q is the state-set of the timed transition system G9 . Note that M ∩ S ⊆ W in[S] for all S ∈ P assed. In fact q ∈ M just in case whenever q ∈ S for some S ∈ P assed then also q ∈ W in [S].

Let K = {Goal} × R X ≥0 . We will show that M is a post-fixed point to λX.π(X) ∪ K and hence that W(G) ⊆ M . In particular, if q ∈ S \ W in[S] for some S ∈ P assed then q ∈ M and hence q ∈ W(G). Now let q ∈ π(M ) ∪ K. We must prove that q ∈ M : In case q ∈ K clearly q ∈ M as S ∩K ⊆ W in[S] for all S ∈ P assed due to the way we initialize W in[S] the first time the symbolic state S is encountered. Assume that q ∈ π(M ) and q ′ ∈ G and let q ′ * be such that q δ * -→ q ′ * . From ii) we know that δ * < δ ′ * . So, q ′ * ∈ B and since we have q ′ δ ′ * -δ * ----→ q ′′ * with q ′′ * ∈ B, q ′ * ∈ B ւ . Therefore, q ′ * ∈ G ∩ B ∩ B ւ and q ∈ (G ∩ B ∩ B ւ ) ւ , which concludes the proof of the claimed inclusion. Now we show that (G ւ ∩ B ւ ) ∪ (G ∩ B ւ ∩ B) ւ ⊆ Pred t (G, B).

Assume that q ∈ (G ւ ∩ B ւ ) ∪ (G ∩ B ւ ∩ B) ւ . First, if q ∈ G ւ ∩ B ւ . We have q ∈ G ւ and by definition of the down operator, this means that ∃δ ∈ R ≥0 s.t. q δ -→ q ′ and q ′ ∈ G. Furthermore, q ∈ B ւ so we are done since this means that there does not exist any δ ′ ∈ R ≥0 s.t. q δ ′ -→∈ B or, equivalently, ∀δ ′ ∈ R ≥0 , q δ ′ -→∈ B, which implies that Post [0,δ] (q) ⊆ B. If q ∈ (G ∩ B ւ ∩ B) ւ , then by definition of the down operator, we know that ∃δ ′ ∈ R ≥0 such that q δ ′ -→ q ′′ and q ′′ ∈ G ∩ B ∩ B ւ . Let δ ′ * be the smallest such δ ′ and q ′′ * be such that q δ ′ * --→ q ′′ * . q ′′ * ∈ G so, to conclude the proof, we need only to prove that Post [0,δ ′ * ] (q) ⊆ B.

Assume this is not the case, then there exists δ ∈ [0, δ ′ * ] s.t. q δ -→∈ B. Now, on the one hand, we know that q ′′ * ∈ B ւ , so there exists δ ′′ ∈ R ≥0 s.t. q δ ′′ -→∈ B. On the other hand, q ′′ * ∈ B and δ ≤ δ ′ * ≤ δ ′′ . But this is not possible since B is convex. So Post [0,δ ′ * ] (q) ⊆ B.

⊓ ⊔

B Production Cell Case Study

Fig. 2 .

 2 Fig. 2. Simulation and time-abstracted quotient graph of Fig. 1 (λ is for time elapsing)

Fig. 3 .

 3 Fig. 3. OTFUR: On-The-Fly Algorithm for Untimed Reachability Games

Fig. 4 .

 4 Fig. 4. SOTFTR: Symbolic On-The-Fly Algorithm for Timed Reachability Games

3 x 0 1 Fig. 5 .

 315 Winning subset of the initial zone of the TGA of Fig.1with clock z added.

Fig. 6 .

 6 Fig.6. The production cell Xeon 2.8GHz equipped with 3GB of RAM running Linux 2.4.21. Table2shows the obtained results. The tests are done with varying number of plates from 2 to 7, and with controllable (win) and uncontrollable (lose) configurations. The models contain from 4 to 10 clocks.The inclusion checking of zones is shown to be an important optimization. Furthermore, activating pruning, which really exploits that the algorithm is on-the-fly, is useful in practice: the algorithm really terminates earlier. The results for time optimal reachability confirm that the algorithm is exploring the whole state-space and is comparable to exploring without pruning. We stress in the tables the best result obtained for every configuration: it turns out that propagating back the losing states has a significant overhead that pays off for large systems, i.e. it is clearly better from 6 plates.The state-space grows exponentially with respect to the number of plates but the algorithm keeps up linearly with it, which is shown on Fig.7that depicts

Fig. 7 .

 7 Fig. 7. Scalability of the algorithm. The scale is logarithmic.

  Consider the second loop invariant. That is W in[S] ⊆ W(G). Upon entering the while-loop this condition holds trivially. The only place at which W in[S] can change is in the reevaluate-branch. Now by the induction hypothesis we may assume that W in[T ] ⊆ W(G) whenever S α -→ T . Then, by monotonicity of Pred t it follows that W in * ⊆ π(W(G)) ⊆ W(G). Thus if the property holds before the update W in[S] ← W in * then it also holds after.

Fig. 8 .

 8 Fig. 8. Uppaal models of the plates and the robot.

Table 2 .

 2 that depicts Results for the different implementations: basic algorithm, then with inclusion checking (inc), pruning (pruning), back propagation of losing states (lose) and time optimal strategy generation (topt, only for "win", and pruning has little effect). Time (user process) is given in seconds (s) rounded to 0.1s and memory in megabytes (M). '-' denotes a failed run (not enough memory). Results in bold font are the best ones.

	Plates	Basic	Basic +inc	Basic +inc Basic+lose +inc Basic+lose +inc
						+pruning	+pruning	+topt
		time mem time mem	time mem	time	mem	time	mem
	win 0.0s 2 lose 0.0s	1M 1M	0.0s 0.0s	1M 1M	0.0s 0.0s	1M 1M	0.0s 0.0s	1M 1M	0.04s n/a	1M n/a
	win 0.5s 19M 3 lose 1.1s 45M	0.0s 0.1s	1M 1M	0.0s 0.0s	1M 1M	0.1s 0.2s	1M 3M	0.27s n/a	4M n/a
	win 33.9s 1395M 0.2s 4 lose --0.5s 11M 8M	0.1s 0.4s	6M 10M	0.4s 0.9s	5M 9M	1.88s n/a	13M n/a
	win 5 lose	--	--	3.0s 31M 11.1s 61M	1.5s 5.9s	22M 46M	2.0s 7.0s	16M 41M	13.35s n/a	59M n/a
	win 6 lose	--	--	89.1s 179M 38.9s 121M 12.0s 699s 480M 317s 346M 135.1s 273M 63M	220.3s 369M n/a n/a
	win 7 lose	--	--	3256s 1183M 1181s 786M 124s 319M 6188s 2457M --16791s 2981M 4075s 2090M n/a n/a

A winning strategy would consist in taking c1 immediately in all states (ℓ1, x) with x ≤ 1; taking c2 immediately in all states (ℓ2, x) with x ≥ 2; taking c3 immediately in all state (ℓ3, x) and delaying in all states (ℓ4, x) with x < 1 until the value of x is 1 at which point the edge c4 is taken.

A time-abstracted bisimulation is a binary relation on states preserving discrete states and abstracted delay-transitions.

Note that π is defined here such that uncontrollable actions cannot be used to win.

Strictly speaking, this requires that we either transforms the given TGA into an equivalent one in which all location-invariants insist on an upper bound on all clocks or, alternatively, that we apply standard extrapolation w.r.t. maximal constant occurring in the TGA (which is correct up to time-abstracted bisimulation).

To get an optimum, the condition of the while-loop must be W aiting = ∅ alone in the algorithm, disabling early termination.

pre + post represents the number of iterations of the algorithm and is therefore an abstraction in both time and space of the implementation.

i.e. Q = L × R X ≥0 .

Acknowledgments. The authors want to thank Patricia Bouyer and Gerd Behrmann for inspiring discussions on the topic of timed games.

Steps

Waiting

Passed Depend Win # S S ′ 0 --(S0, u1, S1), (S0, u2, S2), (S0, c1, S3) S0 -(S0, ∅)

1 S0 S3 (S0, u1, S1), (S0, u2, S2) + (S3, c1, S4), (S3, u3, S2) S3 S3 → (S0, c1, S3) (S3, ∅)

2 S3 S4 (S0, u1, S1), (S0, u2, S2), (S3, u3, S2) + (S3, c2, S4) S4 S4 → (S3, c2, S4) (S4, S4)

3 S3 S4 (S0, u1, S1), (S0, u2, S2), (S3, u3, S2)

At step n, (S, α, S ′ ) is the transition popped at step n + 1; At step n, +(S, α, S ′ ) the transition added to Waiting at step n;

that q ∈ S for some S ∈ P assed. We have to prove that q ∈ W in[S] in order to conclude that q ∈ M . Assume not, i.e. q ∈ W in [S]. But then according to 2. Lemma 1 -as W aiting = ∅ -we have that:

for S ∈ P assed it follows by monotonicity that:

The following distribution law holds:

⊓ ⊔ Assume q ∈ Pred t (G, j B j ). Equivalently, by definition of Pred t , i)∃δ ∈ R ≥0 s.t. q δ -→ q ′ , q ′ ∈ G and ii)Post [0,δ] (q) ⊆ j B j . ii) can be written as

-→ ∈ B j . This is equivalent to ∀j, Post [0,δ] (q) ⊆ B j and together with i), ∀j, q ∈ Pred t (G, B j ). Finally this is equivalent q ∈ j Pred t (G, B j ).

⊓ ⊔ Theorem 4. If B is a convex set, then the Pred t operator defined in equation ( 1) can be expressed as:

Proof. Let us first transform the claimed expression of Pred t . It can equivalently be written as:

From i), we can deduce that q ∈ G ւ . Now if q ∈ B ւ , then q ∈ G ւ ∩ B ւ and we have the claimed result. If q ∈ B ւ , then by definition of the down operator, ∃δ ′ ∈ R ≥0 s.t. q δ ′ -→ q ′′ and q ′′ ∈ B. Let δ ′ * be the smallest such δ ′ . Similarly, let δ * be the smallest δ such that q δ -→ q ′ , with


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

Franck Cassez
email: cassez@irccyn.ec-nantes.fr

Emmanuel Fleury
email: fleury@cs.auc.dk

Kim G Larsen

GDV 2004 Preliminary Version

Keywords: optimal control, timed systems, strategy synthesis

. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.

Introduction

In recent years the application of model-checking techniques to scheduling problems has become an established line of research. Static scheduling problems with timing constraints may often be formulated as reachability problems on timed automata, viz. as the possibility of reaching a given goal state. Realtime model checking tools such as Kronos and Uppaal have been applied on a number of industrial and benchmark scheduling problems [START_REF] Abdeddaim | Modélisation et résolution de problèmes d'ordonnancement à l'aide d'automates temporisés[END_REF][START_REF] Brinksma | Verification and optimization of a PLC control schedule[END_REF][START_REF] Fehnker | Scheduling a steel plant with timed automata[END_REF][START_REF] Hune | Guided synthesis of control programs using uppaal[END_REF][START_REF] Larsen | Resource-efficient scheduling for real time systems[END_REF][START_REF] Niebert | Computing efficient operations schemes for chemical plants in multi-batch mode[END_REF].

Often the scheduling strategy needs to take into account uncertainty with respect to the behavior of an environmental context. In such situations the scheduling problem becomes a dynamic (timed) game between the controller and the environment, where the objective for the controller is to find a dynamic strategy that will guarantee the game to end in a goal state [START_REF] Asarin | Controller synthesis for timed automata[END_REF][START_REF] De Alfaro | Symbolic algorithms for infinite-state games[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF].

A few years ago, the ability to consider quite general performance measures has been given. Priced extensions of timed automata have been introduced [START_REF] Behrmann | Minimum-cost reachability for priced timed automata[END_REF][START_REF] Alur | Optimal paths in weighted timed automata[END_REF] where a cost c is associated with each location ℓ giving the cost of a unit of time spent in ℓ. Within this framework, it is possible to measure performance of runs and to give optimality criteria for reaching a given set of states.

In [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF], we have combined the notions of games and prices and we have proved that, under some hypotheses, the optimal cost in priced timed game automata is computable and that optimal strategies can then be synthetized.

In this paper, we present an algorithm for extracting optimal strategies in priced timed game automata. We also provide an implementation of the algorithm using the tool HyTech [START_REF] Henzinger | HyTech: A model-checker for hybrid systems[END_REF]. The outline of the paper is as follows: in section 2 we recall the definition of Priced Timed Game Automata and present an example; in section 3 we unveil an optimal cost computation method; in section 4 we detail the algorithm to synthesize the optimal strategies and we give some conclusions in section 6.

The HyTech files given in Fig. 5 and Fig. 7 are available on the web page http://www.lsv.ens-cachan.fr/aci-cortos/ptga/. The detailed proofs of the theorems we refer to, as well as complementary definitions and explanations can be found in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF].

2 Priced Timed Games

Preliminaries

Let X be a finite set of real-valued variables called clocks. We denote B(X) the set of constraints ϕ generated by the grammar: ϕ ::= x ∼ k | ϕ ∧ ϕ where k ∈ Z, x, y ∈ X and ∼∈ {<, ≤, =, >, ≥}. A valuation of the variables in X is a mapping from X to R ≥0 (thus an element of R X ≥0 ). For a valuation v and a set R ⊆ X we denote v[R] the valuation that agrees with v on X \ R and is zero on R. We denote v + δ for δ ∈ R ≥0 the valuation s.t. for all x ∈ X, (v + δ)(x) = v(x) + δ.

The (R)PTGA Model

Definition 2.1 [RPTGA] A Priced Timed Game Automaton (PTGA) G is a tuple (L, ℓ 0 , Act, X, E, inv, cost) where: L is a finite set of locations; ℓ 0 ∈ L is the initial location; Act = Act c ∪ Act u is the set of actions (partitioned into controllable and uncontrollable actions); X is a finite set of real-valued clocks; E ⊆ L × B(X) × Act × 2 X × L is a finite set of transitions; inv : L -→ B(X) associates to each location its invariant; cost : L ∪ E -→ N associates to each location a cost rate and to each discrete transition a cost value. We assume that PTGA are deterministic w.r.t. controllable actions (renaming). A reachability PTGA (RPTGA) is a PTGA with a distinguished set of locations Goal ⊆ L.

Runs, Costs of Runs

Let G = (L, ℓ 0 , Act, X, E, inv, cost) be a RPTGA. A configuration of G is a pair (ℓ, v) in L × R X ≥0 . A run ρ = (ℓ 0 , v 0 ) δ 0 --→ (ℓ ′ 0 , v ′ 0 ) e 0 --→ (ℓ 1 , v 1 ) δ 1 --→ (ℓ ′ 1 , v ′ 1 ) e 1 --→ • • • (ℓ n , v n ) δn --→ (ℓ ′ n , v ′ n ) en --→ (ℓ n+1 , v n+1 ) . . . in G is a finite or infinite sequence of alternating time (δ i ∈ R ≥0 ) and discrete (e i ∈ Act) steps such that for every i ≥ 0: (ℓ i , v i ) and (ℓ ′ i , v ′ i ) are configurations of G; for each e i ∈ Act there exists a transition (ℓ ′ i , g, e i , Y, ℓ i+1 ) ∈ E such that v ′ i |= g and v i+1 = v ′ i [Y ]; for each δ i ∈ R ≥0 ℓ i = ℓ ′ i and v ′ i = v i + δ i . The cost of a discrete or time step t = (ℓ, v) α --→ (ℓ ′ , v ′ ) is given by Cost(t) = α.cost(ℓ) if α ∈ R ≥0 and Cost(t) = cost((ℓ, g, α, Y, ℓ)) if α ∈ Act. A run ρ of G is winning if at least
one of the states along ρ is in the set Goal. We note Runs(G) (resp. WinRuns(G)) the set of (resp. winning) runs in G and Runs((ℓ, v), G) (resp. WinRuns((ℓ, v), G)) the set of (resp. winning) runs in G starting in configuration (ℓ, v). If ρ is a finite run with n = 2k steps we note last(ρ) = (ℓ k , v k ) and the cost of the run ρ is defined by: Cost(ρ) = 0≤i≤n-1 Cost(t i ).

Example 2.2 Consider the RPTGA in Fig. 1. Plain arrows represent controllable actions (Act c = {c 1 , c 2 }) whereas dashed arrows represent uncontrollable actions (Act u = {u}). Cost rates in locations ℓ 0 , ℓ 2 and ℓ 3 are 5, 10 and 1 respectively. In ℓ 1 the environment may choose to move to either ℓ 2 or ℓ 3 . However, due to the invariant y = 0 this choice must be made instantaneously.

Strategies, Costs of Strategies

Definition 2.3 [Strategy] Let G be a (R)PTGA. A strategy f over G is a partial function from Runs(G) to Act c ∪ {λ}. Definition 2.4 [Outcome] Let G = (L, ℓ 0 , Act, X, E, inv, cost) be a (R)PTGA and f a strategy over G. The outcome Outcome((ℓ, v), f ) of f from configu- ration (ℓ, v) in G is the subset of Runs((ℓ, v), G) defined inductively by: ℓ 0 cost(ℓ 0 ) = 5 ℓ 1 [y = 0] ℓ 2 cost(ℓ 2 ) = 10 ℓ 3 cost(ℓ 3 ) = 1 Goal x ≤ 2; c 1 ; y := 0 u u x ≥ 2; c 2 ; cost = 1 x ≥ 2; c 2 ; cost = 7 Fig. 1. A Reachability Priced Time Game Automaton A • (ℓ, v) ∈ Outcome((ℓ, v), f ), • if ρ ∈ Outcome((ℓ, v), f ) then ρ ′ = ρ e -→ (ℓ ′ , v ′ ) ∈ Outcome((ℓ, v), f ) if ρ ′ ∈ Runs((ℓ, v), G
) and one of the following three conditions hold: (i) e ∈ Act u , (ii) e ∈ Act c and e = f (ρ),

(iii) e ∈ R ≥0 and ∀0 ≤ e ′ < e, ∃(ℓ ′′ , v ′′ ) ∈ (L × R X ≥0 ) s.t. last(ρ) e ′ --→ (ℓ ′′ , v ′′ ) ∧ f (ρ e ′ --→ (ℓ ′′ , v ′′ )) = λ.
• an infinite run ρ is in ∈ Outcome((ℓ, v), f ) if all the finite prefixes of ρ are in Outcome((ℓ, v), f ).

A strategy f over a RPTGA G is winning from (ℓ, v) whenever all maximal 1 runs in Outcome((ℓ, v), f ) are winning. We denote WinStrat((ℓ, v), G) the set of winning strategies from (ℓ, v) in G. Let f be a winning strategy from configuration (ℓ, v). The cost of f from (ℓ, v) is defined by:

Cost((ℓ, v), f ) = sup{Cost(ρ) | ρ ∈ Outcome((ℓ, v), f )}

Optimal Control Problems

Let (ℓ 0 , 0) denote the initial configuration of a RPTGA G. The three main problems we address in this paper are:

Optimal Cost Computation Problem: we want to compute the optimal cost one can expect in a RPTGA G from (ℓ 0 , 0), i.e. to compute

OptCost((ℓ 0 , 0), G) = inf{Cost((ℓ 0 , 0), f ) | f ∈ WinStrat((ℓ 0 , 0), G)}
Optimal Strategy Existence Problem: we want to determine whether the optimal cost can actually be reached i.e. if there is an optimal strategy f ∈ WinStrat((ℓ 0 , 0), G) such that:

Cost((ℓ 0 , 0), f ) = OptCost((ℓ 0 , 0), G)
1 Roughly speaking a run is maximal if it can not be extended in the future by a controllable action (see [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] page 6, section 2.2); this point is discussed in the sequel in section 3.2.

Optimal Strategy Synthesis Problem: in case an optimal strategy exists we want to compute a witness.

As the example below shows there are PTGA with no optimal winning strategies. In this case there is a family of strategies f ε such that

|Cost((ℓ 0 , 0), f ε ) -OptCost((ℓ 0 , 0), G)| < ε
Thus another problem is, given ε, to compute such an f ε strategy. This latter synthesis problem is not dealt with in this paper.

Example 2.5 [No optimal strategy] For the PTGA of Fig. 2 there is no optimal strategy. c is a controllable action. Nevertheless we can define a family of strategies f ε with 0 < ε ≤ 1 by:

f (ℓ 0 , x < 1 -ε) = λ, f (ℓ 0 , x = 1 -ε) = c and f (ℓ 1 , x ≤ 1) = c.
The cost of such a strategy is 1 + ε. So we can get as close as we want to 1 but there is no optimal winning strategy.

ℓ 0 cost(ℓ 0 ) = 1 ℓ 1 cost(ℓ 1 ) = 2 Goal x < 1; c x = 1; c [x < 1] [x ≤ 1]
Fig. 2. A PTGA with no reachable optimal cost.

Example 2.6 We consider again Fig. 1. We want to compute an optimal strategy for the controller from the initial configuration. Obviously, once ℓ 2 or ℓ 3 has been reached the optimal strategy for the controller is to move to Goal asap (taking a c 2 action). The crucial (and only remaining) question is how long the controller should wait in ℓ 0 before taking the transition to ℓ 1 (doing c 1 ). Obviously, in order for the controller to win this duration must be no more than two time units. However, what is the optimal choice for the duration in the sense that the overall cost of reaching Goal is minimal? Denote by t the chosen delay in ℓ 0 . Then 5t + 10(2t) + 1 is the minimal cost through ℓ 2 and 5t + (2t) + 7 is the minimal cost through ℓ 3 . As the environment chooses between these two paths the best choice for the controller is to delay t ≤ 2 such that max(21 -5t, 9 + 4t) is minimum, which is t = 4 3 giving a minimal cost of 14 1 3 . In Fig. 3 we illustrate the optimal strategy for all states reachable from the initial state provided by our HyTech implementation that will be described in section 3.4.

Optimal Cost Computation

In this section we show that computing the optimal cost for a RPTGA amounts to solving a simple2 control problem on a linear hybrid game automaton [START_REF] Wong-Toi | The synthesis of controllers for linear hybrid automata[END_REF]. As a consequence well-known algorithms [START_REF] Wong-Toi | The synthesis of controllers for linear hybrid automata[END_REF][START_REF] De Alfaro | Symbolic algorithms for infinite-state games[END_REF] for computing winning states of reachability hybrid games enable us to compute the optimal cost of a RPTGA.

We then show how to use the HyTech tool to implement the computation of the optimal cost for RPTGA.

From Priced Timed Games to Linear Hybrid Games

Assume we want to compute the optimal cost of the RPTGA A given in Fig. 1.

We translate this automaton into a linear hybrid game automaton (LHGA for short) H (see Fig. 4) where the cost function is encoded into a variable Cost of the LHGA. In H the variable Cost decreases with rate k in a location ℓ (i.e. Let CompWin be a semi-algorithm (e.g. [START_REF] Wong-Toi | The synthesis of controllers for linear hybrid automata[END_REF][START_REF] De Alfaro | Symbolic algorithms for infinite-state games[END_REF]) that computes the largest set of winning states for a reachability hybrid game. Using CompWin we can compute the largest set of winning states for H with the goal states given by Goal∧Cost ≥ 0. The meaning of this new reachability game is that we want to win without having spent all the resources (Cost) we started with. Assume the corresponding (largest) set of winning states is denoted CompWin(H, Goal ∧ Cost ≥ 0). The meaning of the set W = CompWin(H, Goal ∧ Cost ≥ 0) is that in order to win one has to start in the region given by W and if one starts outside W the opponent has a strategy to win i.e. we lose. We can prove (see [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF], Theorem 5 and Lemma 6) that the (largest) set of winning states W is a union of zones of the form (ℓ, R ∧ Cost ≻ h) where ℓ is a location, R ⊆ R X ≥0 , h is a piece-wise affine function on R and ≻∈ {>, ≥}. Hence we have the answer to the optimal reachability game: we intersect the set of initial states with the set of winning states W , and in case it is not empty, the projection on the Cost axis yields a constraint on the cost like Cost ≻ k with k ∈ Q ≥0 and ≻∈ {>, ≥}. By definition of the winning set of states in reachability games, this is the largest set from which we can win, no cost lower than or equal to k is winning and we can deduce that k is the optimal cost. Also we can decide whether there is an optimal strategy or not: if ≻ is equal to > there is no optimal strategy and if ≻ is ≥ there is one.

dCost dt = -k in ℓ) if Cost(ℓ) = k in A. As for discrete transitions the variable Cost is updated by Cost ′ = Cost -k in H if the corresponding transition's cost in A is k. ℓ 0 dCost dt = -5 ℓ 1 [y = 0] ℓ 2 dCost dt = -10 ℓ 3 dCost dt = -1 Goal x ≤ 2; c 1 ; y := 0 u u x ≥ 2; c 2 Cost ′ = Cost -1 x ≥ 2; c 2 Cost ′ = Cost -7
Thus computing CompWin(H, Goal ∧ Cost ≥ 0) is a semi-algorithm for computing the optimal cost of the RPTGA A. Moreover we can decide (if CompWin terminates) whether there exists an optimal strategy or not: in case the initial winning cost set is of the form Cost > k there is no optimal strategy but a family of strategies f ε (for ε > 0) with cost lower than k + ε. When this set if of the form Cost ≥ k (and assuming CompWin terminates) we can compute an optimal strategy (this point is dealt with in the next section 4).

The formal definitions and proofs of this reduction are given in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] (Definition 12, Lemma 5, Theorems 4 and 5, Corollaries 1 and 2).

The π Operator

The computation of the winning states (with CompWin) is based on the definition of a controllable predecessor operator [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF][START_REF] De Alfaro | Symbolic algorithms for infinite-state games[END_REF]. Let G = (L, ℓ 0 , Act, X, E, inv, cost) be a RPTGA and Q its set of configurations. For a set X ⊆ Q and a ∈ Act we define Pred a (X) = {q ∈ Q | q a --→ q ′ , q ′ ∈ X}. The controllable and uncontrollable discrete predecessors of X are defined by cPred(X) = c∈Actc Pred c (X), respectively uPred(X) = u∈Actu Pred u (X). We also need a notion of safe timed predecessors of a set X w.r.t. a set Y . Intuitively a state q is in Pred t (X, Y ) if from q we can reach q ′ ∈ X by time elapsing and along the path from q to q ′ we avoid Y . Formally this is defined by:

Pred t (X, Y ) = {q ∈ Q | ∃δ ∈ R ≥0 s.t. q δ -→ q ′ , q ′ ∈ X ∧ Post [0,δ] (q) ⊆ Y } (1)
where

Post [0,δ] (q) = {q ′ ∈ Q | ∃t ∈ [0, δ] | q t -→ q ′ }.
We are then able to define a controllable predecessor operator π as follows:

π(X) = Pred t X ∪ cPred(X), uPred(X) (2)
This definition of π captures the choice that uncontrollable actions cannot be used to win (this choice is made in [START_REF] La Torre | Optimal-reachability and control for acyclic weighted timed automata[END_REF] and in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]). As a matter of fact there is no way to win in the RPTGA of Fig. 1 with this definition of π: ℓ 1 cannot be a winning state if we start iterating the computation of π from Goal as π only adds predecessors that can reach a winning state by a controllable transition.

Another choice is possible: uncontrollable actions may be used to win if they are forced to happen. This second choice is rather involved when one wants to give a new definition of π in the general case. We adopt a position which is half-way between the previous two extremes: if an uncontrollable action is enabled from a state q where time cannot elapse and leads to a winning state q ′ , and no uncontrollable transitions enabled at q can lead to a nonwinning state, we declare q as winning. Assume the set of configurations of G where time cannot elapse is denoted STOP . Then a new definition of π where uncontrollable actions can be used to win is given by:

π ′ (X) = Pred t X ∪ cPred(X) ∪ (uPred(X) ∩ STOP ), uPred(X) (3)
Note that this choice does not change the results presented in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]. In the example of Fig. 1, from location ℓ 1 only uncontrollable transitions are enabled, but they are bound to happen within a bounded amount of time (in this case as soon as we reach ℓ 1 because of the invariant y = 0). π ′ will add configuration (ℓ 1 , x ≥ 0 ∧ y = 0) to the set of winning states. The semi-algorithm CompWin computes the least fixed point W of the functional λX.{X 0 } ∪ π ′ (X) as the limit of an increasing sequence of sets of states W i (starting from set W 0 = X 0 ) where

W i+1 = π ′ (W i )). If G is a RPTGA, the result of the computation of CompWin on the associated LHGA H starting from Goal ∧ Cost ≥ 0 is W = µX.{Goal ∧ Cost ≥ 0} ∪ π ′ (X)
. This result is also denoted CompWin(H, Goal ∧ Cost ≥ 0) and gives the largest set of winning states.

Termination Issues

An important issue about the previous semi-algorithm CompWin is whether it terminates or not. We have identified a class of RPTGA for which CompWin terminates on the associated hybrid game.

Let G be a RPTGA satisfying:

• G is bounded, i.e. all clocks in G are bounded3 ;

• the cost function of G is strictly non-zeno, i.e. there exists some κ > 0 such that the accumulated cost of every cycle in the region automaton associated with G is at least κ. Note that this condition can be checked. For more complete explanations, see [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF].

Then the semi-algorithm CompWin(H, Goal ∧ Cost ≥ 0) terminates (H is the hybrid game defined from G in the previous section). The formal statement and proof of this claim is given by Theorem 6 in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]. We thus get:

Theorem 3.1 Let G be a RPTGA satisfying the above-mentionned hypotheses (boundedness and strict non-zenoness of the cost). Then the optimal cost is computable for G.

Implementation of CompWin in HyTech

HyTech [START_REF] Henzinger | A user guide to hytech[END_REF][START_REF] Henzinger | HyTech: A model-checker for hybrid systems[END_REF] is a tool that implements "pre" and "post" operators for linear hybrid automata. Moreover it is possible to write programs that use these operators (and many others) on polyhedra in order to compute sets of states.

The specification in HyTech of our LHGA H of Fig. 4 is given in Fig. 5, lines 7-20. We detail this specification in the sequel.

Controllable and Uncontrollable Predecessors. HyTech provides the pre operator that computes at once the time predecessors and the discrete predecessors of a set of states. As we need to distinguish between time predecessors, discrete controllable predecessors and discrete uncontrollable predecessors, we use the following trick: in the HyTech source code of the LHA H we add two boolean variables u and c (Fig. 5, line 4) that are negated on each discrete uncontrollable (resp. controllable) transitions (Fig. 5, lines 10-19). In HyTech one can existentially quantify over a variable t by using the hide operator. Then the controllable predecessors can be computed by existentially quantifying over c and over a variable t that has rate4 -1. We can express the cPred (and uPred) operator with existential quantifiers and two variables t and c as follows:

cPred(X) = {q | ∃c ∈ Act c s.t. q c -→ q ′ , q ′ ∈ X} = {q | ∃t s.t. ∃c s.t. t = 0 ∧ c = 0 ∧ (q, t, c) ∈ pre(X ∧ t = 0 ∧ c = 1
)} where pre is the predecessor operator of HyTech.

We impose that the value of t stays unchanged to ensure that we just take discrete predecessors (Fig. 5, line 39). For uncontrollable predecessors we replace c by u (Fig. 5, line 41). Note that the computation of STOP states (Fig. 5, line 32) can also be done using our extra variables t, c, u.

Safe Time Predecessors. The other operator Pred t (Z, Y ) is a bit more complicated. We just need to express it with existential quantification so that it is easy to compute it with HyTech. Also we assume we have time deterministic automata as in this case Pred t (Z, Y ) is rather simple (if we do not have time determinism a more complicated encoding must be done and we refer the reader to [START_REF] Wong-Toi | The synthesis of controllers for linear hybrid automata[END_REF] for a detailed explanation.) From equation (1) we get:

Pred t (Z, Y ) = {q | ∃t ≥ 0 s.t. q t -→ q ′ , q ′ ∈ Z and ∀0 ≤ t 1 ≤ t, q t -→ q ′′ =⇒ q ′′ ∈ Y } = {q | ∃t ≥ 0 s.t. q t -→ q ′ , q ′ ∈ Z and ¬(∃0 ≤ t 1 ≤ t, q t -→ q ′′ ∧ q ′′ ∈ Y )}
The latter formula can be encoded in HyTech using the hide operator (Fig. 5, lines 47-55) and two auxiliary variables t and t 1 that evolves at rate -1 (note -time predecessors of Z from which we can reach Z -and avoid uPred(X) all along; X := Predt(Z, uPred(X))

X := hide t in (hide c,u in t>=0 & c=0 & u=0 & pre(Z & t=0 & c=0 & u=0) endhide) & 50: ~(hide t1 in (hide c,u in t1>=0 & t1<=t & c=0 & u=0 & pre(uPrebarX & t1=0 & c=0 & u=0) endhide) endhide) 55:
endhide; -add the newly computed regions to the set of already -computed region fix := fix | X ; } ; 60:

-print the result print omit all locations hide x,y in fix & init_reg endhide; that those variables are not part of the model but only used in existentially quantified formulas and they do not constrain the behavior of H.) Finally if the computation of π ′ terminates (Fig. 5, lines 35-59) the set fix contains all the winning states. It then suffices to compute the projection on cost in the initial state to obtain the optimal cost (Fig. 5, line 61).

Doing this we have solved the first two problems: computing the optimal cost and deciding whether there exists an optimal strategy.

Optimal Strategies Computation

In this section we show how to compute an optimal strategy when one exists. Then we give the HyTech implementation of this computation and discuss some properties of those strategies.

Strategy Synthesis For RPTGA

First we recall some basic properties of strategies for (unpriced) Timed Game Automata (TGA).

A strategy f is

• state-based whenever ∀ρ, ρ ′ ∈ Runs(G), last(ρ) = last(ρ ′ ) implies that f (ρ) = f (ρ ′ ).
State-based strategies are also called memoryless strategies in game theory [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF][START_REF] De Alfaro | Symbolic algorithms for infinite-state games[END_REF];

• polyhedral if for all a ∈ Act c ∪ {λ}, f -1 (a) is a finite union of convex polyhedra for each location of the game;

• realizable, whenever the following holds: for all ρ ∈ Outcome(q, f ) s.t. f is defined on ρ and f (ρ) = λ, there exists some δ > 0 such that for all 0 ≤ t < δ, there exists q ′ with ρ t -→ q ′ ∈ Outcome(q, f ) and f (ρ

t -→ q ′ ) = λ.
Strategies which are not realizable are not interesting because they generate empty sets of outcomes. Nevertheless it is not clear from [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF][START_REF] Asarin | Controller synthesis for timed automata[END_REF] how to extract strategies for RPTGA and ensure their realizability as shown by the following example. 6 where c is a controllable action. The game is to enforce state Goal. The most natural strategy f would be to do a c when x > 1 and to wait until x reaches a value greater than 1. Formally this yields f (ℓ 0 , x ≤ 1) = λ and f (ℓ 0 , x > 1) = c. This strategy is not realizable. In the sequel, we build a strategy which is f (ℓ 0 , x < 2) = λ and f (ℓ 0 , x ≥ 2) = c. Now assume the constraint on the transition is 1 < x ≤ 2. In this case we start with the following strategy (not realizable): f (ℓ 0 , x ≤ 1) = λ and f (ℓ 0 , 1 < x ≤ 2) = c. To make it realizable we will take the first half of 1 < x ≤ 2 and have a delay action on it i.e. f (ℓ 0 , x < 3 2 ) = λ and f (ℓ 0 , 3 2 ≤ x ≤ 2) = c. In the following, we will restrict our attention to realizable strategies and simply refer to them as strategies.

ℓ 0 Goal x > 1; c
A secondary result is provided in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] for Linear Hybrid Games (Theorem 2 page 7) that can be rephrased in the context of RPTGA as: Theorem 4.2 (Adapted from Theorem 2 of [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]) Let G be a RPTGA. If the semi-algorithm CompWin terminates for the hybrid game associated with G (see section 3.1), then we can compute a winning strategy which is: polyhedral, realizable and stated-based.

Let H be the LHGA associated to the RPTGA G = (L, ℓ 0 , Act, X, E, inv, cost). A state of H is a triple (ℓ, v, c) where ℓ ∈ L, v ∈ R X ≥0 and c ≥ 0 (c is the value of the variable Cost of H). Thus if we synthetize a realizable winning state-based strategy f for H, we obtain a strategy that depends on the cost value. In case there is a winning strategy for H (see section 3.1) we can synthetize realizable state-based winning strategies for G (see [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF], Corollary 2). This result is already satisfying but we would like to build strategies that are independent of the cost value i.e. in which there is no need for extra information to play the strategy on the original RPTGA G (this means we want to build a statebased strategy for the original RPTGA G.) To this extent we introduce the notion of cost-independent strategies.

Let W = CompWin(H, Goal ∧ Cost ≥ 0) be the set of winning states of

H. A state-based strategy f for H is cost-independent if (ℓ, v, c) ∈ W and (ℓ, v, c ′ ) ∈ W implies f (ℓ, v, c) = f (ℓ, v, c ′ ).
Cost-independent strategies in H will then be used for having state-based strategies in G. Theorem 7 of [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] gives then sufficient conditions for the existence of a state-based, optimal, realizable strategy in G and, when back to the automaton reads as follows:

Theorem 4.3 (Adapted from Theorem 7 of [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]) Let G be a RPTGA. H is the associated LHGA. If CompWin terminates for H and the set of winning states is W = CompWin(H, Goal ∧ Cost ≥ 0) is a union of sets of the form (ℓ, R ∧ Cost ≥ h) where ℓ is a location, R ⊆ R X ≥0 and h is a piece-wise affine function on R, then there exists a winning realizable state-based strategy f defined over

W G = ∃Cost.W s.t. for each q ∈ W G , f ∈ WinStrat(q, W G ) and Cost(q, f ) = OptCost(q).
Note that under the previous conditions we build a strategy f which is uniformly optimal i.e. optimal for all states of W G . A syntactical criterion to enforce the condition of theorem 4.3 is that the constraints (guards) on controllable actions are non-strict and constraints on uncontrollable actions are strict. We now give an algorithm to extract such an optimal, state-based, realizable and winning strategy for a RPTGA G.

The example of Fig. 1 satisfies the assumptions of Theorem 4.3 and thus we can compute an optimal strategy for this model. Moreover, the strategy we obtain using HyTech is precisely the one we described in Fig. 3.

Synthesis of Optimal Strategies

The set of winning states of H is computed iteratively using the functional π ′ defined by equation ( 3). In the sequel we need to compute the states that can let a strict positive delay elapse to define the strategy for the delay action.

For a set X we denote NonStop(X) the set of states in X from which a strict positive delay can elapse and all the intermediary states lie in X i.e.

NonStop(X) = {q ∈ X | ∃t > 0 | q + t ∈ X ∧ ∀0 ≤ t ′ ≤ t, q + t ′ ∈ X} (4)
Tagged Sets. To synthetize strategies we compute iteratively a set of extended "tagged" states W + during the course of the computation of W (this follows from Theorem 2 and Lemma 6 of [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]). The tags will contain information about how a new set of winning states W i+1 = π ′ (W i ) has been obtained. We start with W + 0 = ∅ and W 0 = Goal ∧ Cost ≥ 0. Assuming W i and W + i are the sets obtained after i iterations of π ′ we define W + i+1 as follows:

(i) let Y = W i+1 \ W i where W i+1 = π ′ (W i ); (ii) for each c ∈ Act c , we define the tagged set Y ∩ cPred c (W i ) [c]
with the intended meaning: "Y ∩ cPred c (W i ) has been added to the set of winning states by a Pred c and doing a c from this set leads to W i ";

(iii) define another tagged set NonStop(Y ) [λ] with the intended meaning: "NonStop(Y ) has been added to the set of winning states by the (strictly positive) time predecessors operator and letting time elapse will lead to either W i or cPred(W i ) or uPred(W i ) ∩ STOP ";

(iv) define W + i+1 by :

W + i+1 = W + i ∪ NonStop(Y ) [λ] ∪ c∈Actc Y ∩ cPred c (W i ) [c]
Computation of an Optimal Strategy. If CompWin terminates in j iterations we end up with W + = W + j . Note that by construction a state q of W may belong to several tagged sets

X [λ] 0 , X [c 1 ] 1 , . . . , X [cn] n (where c i ∈ Act c for each i ∈ [1, n]) of W + . If the assumptions of theorem 4.3 are satisfied all the X i 's are of the form X ′ i ∧ Cost ≥ h i where X ′ i ⊆ {ℓ i } × R X ≥0
for some location ℓ i and h i : X ′ i → R ≥0 is a piecewise affine function. Thus the infimum of h i over X ′ i is reachable and equal to the minimum of h i . Theorem 7 of [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] states that in this case an optimal state-based strategy f * for q a winning state of G (no cost) will be obtained by taking the local optimal choice: let m = min i∈[0,n] h i (q); then defining f * (q) = c i if h i (q) = m gives an optimal strategy.

As it can be the case that h i (q) = h j (q) = m with i = j, we impose a total order ⊏ on the set of events in Act c and define f * (q) = c i where i = max{j | h j (q) = m}. To avoid realizability problems (see proof of Lemma 6 in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]) on the boundary of a set X i if h 0 (q) = m (which means that the optimal cost can be achieved by time elapsing) and h i (q) = m for some i ∈ [1, n] we define f * (q) = c i . This can be easily defined in our setting by extending ⊏ to Act c ∪ {λ} and making λ the smallest element.

After these algorithmics explanations, we can summarize how we can synthesize an optimal, cost-independent strategy. We denote W + [c] the set defined by:

W + [c] = S [c] i ∈W + S i (5)
For each c ∈ Act c ∪ {λ}, W + [c] is a set of the form X c ∧ Cost ≥ h c where h c is a piecewise affine function on X c (X c is a union of convex polyhedra). Note that the constraint Cost ≥ h c is a polyhedron which constrains the Cost variable and the clocks. In what follows, a pair (q, α) will represent a state of H (α is the value of the Cost variable). For each winning state q of G, we want to compute the minimal cost for winning and which action we should do if we want to win with the optimal cost. Let us consider two actions c 1 , c 2 ∈ Act c ∪ {λ}. We denote [c 1 ≤ c 2 ] the set of winning states of G where it is better to do action c 1 than action c 2 (h c 1 (q) ≤ h c 2 (q)). This set is defined by:

[c 1 ≤ c 2 ] = {q ∈ X c 1 | ∃α 1 | (q, α 1 ) ∈ W + [c 1 ] and ∀α 2 | (q, α 2 ) ∈ W + [c 2 ] , α 1 ≤ α 2 } (6) = q ∈ X c 1 | ∃α 1 | (q, α 1 ) ∈ W + [c 1 ] ∧ ¬ ∃α 2 | (q, α 2 ) ∈ W + [c 2 ] and α 2 < α 1 (7) Each set [c 1 ≤ c 2 ] is a polyhedral set. For each c ∈ Act c ∪ {λ} define Opt(c) = c ′ =c [c ≤ c ′ ] (8)
Opt(c) is the set of states for which c is an action that gives the optimal cost. W * = c∈Actc∪{λ} Opt(c) is thus equal to the set of states on which we need to define the optimal strategy. Given the total order ⊏ on Act c ∪ {λ} with λ ⊏ c 1 ⊏ • • • ⊏ c n , we can define an optimal strategy f * as follows: for

i ∈ [0, n -1], let B i = W * \ (∪ k>i B k ) ∩ Opt(c i ) and B n = W * ∩ Opt(c n ); define then f * (q) = c i if q ∈ B i .
f * is an optimal strategy that is (winning), state-based, realizable and polyhedral.

Implementation in HyTech

Controllable Tagged Sets. We first show how to compute tagged sets of states. Our HyTech encoding consists in adding a discrete variable a to the HyTech model of Fig. 5 and use it in the guards of controllable transitions: controllable action c k of Fig. 4 corresponds to the guard a = k in the HyTech model. The HyTech model of Fig. 5 is enriched as follows: we add the guard a = 1 to line 11, a = 2 to lines 16 and 18. In this way we achieve the tagging of controllable predecessors as now the computation of cPred (line 39 of Fig. 7) will compute a tagged region that will be a union of polyhedra with some a = k constraints. Note that we also modify line 44 of Fig. 5 and replace it by line 20 in Fig. 7 where a is hidden from the new cPreX as a is not needed to compute the winning set of states.

New NonStop States. To compute NonStop(Y ) we use again our extra variables t, c, u and add the tag a = 0 to the result set. Lines 35-36 of Fig. 7 achieves this.

W + is stored in the region fix_strat in the HyTech code. To compute W + i+1 we update fix_strat as described by line 38 in Fig. 7. Computation of the Optimal Strategy. To compare the costs for each action and determine the optimal one we use the trick described in the previous subsection. Each tagged set gives the function h c i by the means of a constraint between the Cost variable and the rest of the state variables. To compute h c i we need to split the state space according to each action c i : this is achieved by lines 44-46 where the state space that corresponds to h c i is stored in ri.

It remains to compute for each pair of actions (c 1 , c 2 ) (c i can be λ), the set [c 1 ≤ c 2 ] states. The encoding in HyTech of the formula given by equation ( 7) is quite straightforward using the hide operator that corresponds to existential quantification. The strategy is then computed as described at the end of the previous subsection by lines 54-63.

Experiments

Using a HyTech-code as described in this paper, we have done some more experiments. The most important example we have treated is a model of a mobile phone with two antennas trying to connect to a base station with an environment which can possibly jam some transmissions.

Description of the Mobile Phone Example. We consider a mobile phone with two antennas emitting on different channels. Making the initial connection with the base station takes 10 time units whatever antenna is in use. Statistically, a jam of the transmission (e.g. collision with another phone) may appear every 6 time units in the worst case. When a collision is observed, the antenna tries to transmit with a higher level of energy for a while (at least 5 time units for Antenna 1 and at least 2 time units for Antenna 2) and then can switch back to the lower consumption mode. Unfortunately, switching back to the low consumption mode requires more resources and forces to interrupt the other transmission (Antenna 1 resets variable y of Antenna 2 and vice-versa). The overall cost rate (consumption per time unit) for the mobile phone in a product state s = (low x , high y , Y) is the sum of the rates of Antenna 1 and Antenna 2 (both are working) i.e. 1 + 20 = 21 and Cost(s) = 21 in our model. Once the connection with the base station is established (either x ≥ 10 or y ≥ 10) the message is delivered with an energy consumption depending on the antenna (Cost = 7 for Antenna 1 and Cost = 1 for Antenna 2). The aim is to connect the mobile phone with an energy consumption (cost) as low as possible whatever happens in the network (jam). This system can be represented by a network of PTGAs (see Fig. 8 where plain arrows represent controllable actions whereas dsahed arrows represent uncontrollable actions) and the problem reduces to finding an optimal strategy for reaching one of the goal states Goal x or Goal y . Note that our original model is a single PTGA and not a network of PTGAs, but networks of PTGA can be used as well because it does not add expressive power and it is simple to define the composed PTGA: in a global location (being a tuple of locations of simple PTGAs), the cost is simply the sum of the costs of all single locations composing it. Idem for a composed transition resulting from a synchronization: the cost of the synchronized transition is the sum of the costs of the two initial transitions. Of course, one has to pay attention that no controllable action can synchronize with an uncontrollable action in order that we can define properly the nature, controllable or not, of the synchronization. In this example, see Fig. 8, jam x ? (resp. jam y ?) synchronizes with jam x ! (resp. jam y !). The HyTech code of this example can be found in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] and on the web page http://www.lsv.ens-cachan.fr/aci-cortos/ptga/. Results of our Experiments. We got that the optimal cost (lowest energy consumption) that can be ensured is 109. The optimal strategy is graphically represented on Fig. 9. The strategy is non-trivial and the actions to take depend on a complex partitioning of the clock space. The computation took 828s on a 12" PowerBook G4 running Mac OS X.

In this paper we have described an algorithm to synthesize optimal strategies for a sub-class of priced timed game automata. The algorithm is based on the work described in [START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF] where we proved this problem was decidable (under some hypotheses we recall in this paper). Morever, we also provide an implementation of our algorithm in HyTech and demonstrate it on small case-studies. In a recent paper [START_REF] Alur | Optimal reachability in weighted timed games[END_REF] Alur et al. addressed a related problem i.e. "compute the optimal cost within k steps". They give a complexity bound for this restricted "bounded" problem and prove that the splitting incurred by the computation of the optimal cost within k steps only yields an exponential number (in k and the size of the automaton) of subregions. They do not consider the problem of strategy synthesis.

Our future work consists in extending the class of systems for which the algorithm we provided terminates. The synthesis of sub-optimal strategies (when no optimal strategy exists) is currently being investigated. We would also like to extend this work to more general winning conditions (like safety conditions) and with other performance criteria (as for example the price per unit of time along infinite schedules).

Fig. 3 .

 3 Fig.3. Optimal strategy for the RPTGA of Fig.1. Optimal cost is 141 3 .

Fig. 4 .

 4 Fig. 4. The Linear Hybrid Game Automaton H.

10 : 15 :

 1015 loc l0: while x>=0 & y>=0 wait {dcost=-5,dt=-1,dt1=-1} when x>=0 & x<=2 do {u'=u,c'=1-c,y'=0} goto l1; loc l1: while y=0 wait {dcost=0,dt=-1,dt1=-1} when True do {u'=1-u,c'=c} goto l2; when True do {u'=1-u,c'=c} goto l3; loc l3: while x>=0 & y>=0 wait {dcost=-10,dt=-1,dt1=-1} when x>=2 do {c'=1-c,u'=u,cost'=cost-1} goto Win; loc l4: while x>=0 & y>=0 wait {dcost=-1,dt=-1,dt1=-1} when x>=2 do {c'=1-c,u'=u,cost'=cost-7} goto Win; loc Win: while True wait {dcost=0,dt=-1,dt1=-1} 20: end var init_reg,winning,fix, -sets of states STOP, -set of STOP states from which time cannot elapse uPreX,uPrebarX,cPreX,X,Y,Z : region ; 25: -first define the initial and winning regions init_reg := loc[H]=l0 & x=0 ; winning := loc[H]=Win & cost>=0; -fix is the fixpoint we want to compute i.e. the set of winning states W 30: fix := winning; -stopped states STOP := ~(hide t,c,u in t>0 & c=0 & u=0 & pre(True & t=0 & c=0 & u=0) endhide) ; -compute the fixpoint of π ′ 35: X := iterate X from winning using { -uncontrollable predecessors of X: uPred(X) uPrebarX := hide t,u in t=0 & u=0 & pre(~X & u=1 & t=0) endhide; -controllable predecessors of X: cPred(X) cPreX := hide t,c in t=0 & c=0 & pre(X & t=0 & c=1) endhide ; 40: -uncontrollable predecessors leading to winning states: uPred(X) uPreX := hide t,u in t=0 & u=0 & pre(X & u=1 & t=0) endhide; --Z is the the first argument of π ′ in the paper; --Z = X ∪ cPred(X) ∪ (uPred(X) ∩ STOP ) Z := (X | cPreX | (uPreX & STOP)) ; 45:

Fig. 5 .

 5 Fig. 5. Computation of the Optimal Cost.

Fig. 6 .

 6 Fig. 6. A timed game automaton Example 4.1 Consider the PTGA of Fig.6where c is a controllable action. The game is to enforce state Goal. The most natural strategy f would be to do a c when x > 1 and to wait until x reaches a value greater than 1. Formally this yields f (ℓ 0 , x ≤ 1) = λ and f (ℓ 0 , x > 1) = c. This strategy is not realizable. In the sequel, we build a strategy which is f (ℓ 0 , x < 2) = λ and f (ℓ 0 , x ≥ 2) = c. Now assume the constraint on the transition is 1 < x ≤ 2. In

GoalxFig. 8 .

 8 Fig. 8. Mobile Phone Example.

Delay high x →low x high y →low y low x →Goal x low y →Goal yFig. 9 .

 9 Fig. 9. Optimal Strategy for the Mobile Phone Example

Without cost.

P. Bouyer et al.

This hypothesis is not a restriction, see[START_REF] Larsen | As cheap as possible: Efficient cost-optimal reachability for priced timed automata[END_REF].

any rate different from 0 would also do but we need another variable t with rate -1 later on and use this one.

 [START_REF] Abdeddaim | Modélisation et résolution de problèmes d'ordonnancement à l'aide d'automates temporisés[END_REF]Work supported by the ACI Cortos, a program of the French government.

var

-same set of variables here as lines 22-24 in Fig. 5 plus some new vars: a: discrete; cost0,cost1,cost2: analog;

5:

fix_strat,nonstop,Y, r0,r1,r2, B0,B1,B2, inf_0_1,inf_0_2,inf_1_0,inf_1_2,inf_2_0,inf_2_1: region; X := iterate X from winning using { uPrebarX : -compute the state space inf_i_j where h c i (q) ≤ h c j (q) inf_0_1 := hide cost0 in r0 & ~(hide cost1 in r1 & cost1<cost0 endhide) endhide ;