Control of Timed Systems

In this Chapter we address the problem of controller synthesis for timed systems. By timed systems we refer to systems which are subject to quantitative (hard) real-time constraints. We assume the reader is familiar with the basics of Timed Automata theory, or has read Chapter 1 and Chapter 2 in this book.

Introduction

It is not always possible to use discrete time to specify and model timing constraints. This is why dense-time specification formalisms, like timed automata [ALU 94] or time Petri nets [MER 74] have been introduced some years ago. Once a system is modelled by a timed automaton or a time Petri net, it can checked (Chapter 2) for quantitative properties. If a property is not satisfied, we still might be able to act on the system and control some of its behaviours: for instance by adding a component, a controller. How to compute such a timed controller is the purpose of this Chapter in which we review some algorithms for controller synthesis for timed automata.

Verification of Timed Systems

A standard approach to the verification of real-time systems, called model checking [SCH 99], consists in 3 phases: (1) build a complete model S for the system (e.g. a finite automaton); (2) specify the qualitative correctness property to be satisfied in a non ambiguous logical language (e.g. temporal logics) as a formula ψ and (3) check Chapter written by Franck CASSEZ and Nicolas MARKEY.

algorithmically that S is a model of ψ, denoted S |= ψ: this is the model checking algorithm. Model cheking techniques for discrete event systems and qualitative properties, have been studied for quite a long time and are mature enough to have spread in industry. Nevertheless, for certain types of systems, the correctness property is formulated in terms of quantitative requirements that cannot be captured in a discrete time or logical time model. A typical example of such system is the scheduling of tasks where the durations of the tasks must be taken into account. It is sometimes possible to use discrete time as an abstraction for dense time but it may turn out to be of limited applicability: if the timing parameters of the system range from 1 to 10 000, using a discrete clock that ticks every time unit produces a prohibitive number of states, and model checking algorithms (even if symbolic) will not be able to handle such state spaces. Another disadvantage of using discrete time is that it is not easy to compose two systems specified with different time scales. Finally, we may have some limited knowledge of the durations of the tasks in the system. To take into account this uncertainty (durations of the tasks, of the communications), we can use dense time formalisms, for instance timed automata (TA) [ALU 94] which are finite automata extended with real-time clocks. Model checking algorithms for discrete event systems (finite automata, temporal logics like CTL or LTL) have been extended to timed automata and timed logics and these algorithms are implemented in a variety of tools like UPPAAL [AMN 01], KRONOS [YOV 97], CMC [LAR 98, LAR 05], PHAVER [FRE 05] (see Chapter 7 in this book) and HYTECH [HEN 97].

The Controller Synthesis Problem

To use a model checking algorithm, we must have a complete model describing all the behaviours of the system: thus we assume we have a model consisting of the environment of the system, the sensors and the controller. Such systems are called closed systems. On the contrary, in the framework of controller synthesis, we assume we have a model of the system which is open: if S is a model the system to be controlled, we have to find a controller C to build a closed system C(S) "S controlled or supervised by C" which represents the complete model.

If the correctness property is φ, the model checking approach answers to questions of the form "Does C(S) satisfy φ?". Hence the model checking problem can be formally defined by: given S, C and φ, does C(S) |= φ hold ?

[MCP]

The model checking approach thus requires to first build (maybe by "hand") a controller C to be able to obtain a closed system C(S). This can be a very difficult task for complex systems or when the correctness property involves timing constraints. Moreover, if using our handmade controller C, φ does not hold on C(S), we have to iterate and modify C until we finally end up with a satisfactory controller1 . An ideal solution would be to compute (we say synthesize in the sequel) a controller (if there is one) such that the correctness property is satisfied. This is the controller synthesis problem (CSP) for open systems. Before building a controller we still have to check if one exists, and this is the control problem (CP) formally defined by: given S and φ, is there any C such that C(S) |= φ ?

[CP]

To solve problem [CP], we often have to narrow the class of controllers we will consider. For instance, we can look for finite state controllers (with bounded memory) or timed controllers (that can be represented by timed automata). In any case, once we have checked that a controller exists, another task is to build a witness, which is the controller synthesis problem (CSP):

if the answer to [CP] is "yes", build a witness controller C.

[CSP]

These problems have been introduced and solved for finite state systems (discrete event systems) in the pioneering work of Ramadge and Wonham [RAM 87,RAM 89]. An alternative framework to study the control problem is the framework of game theory which we introduce in the next section.

From Control to Game

A control problem can be formulated as a two-player game problem (see [ ARN 03,MCN 93, RIE 03, THO 95]): the model of the system is a transition system in which one of two players, controller or environment, is responsible for state change. In this framework, the controller has to find a strategy to ensure a particular property, and this, whatever the environment does.

An example of a two-player game is given in Fig. 3.1. In this game, round shaped states are Player 1' states in which Player 1 chooses the next move, and the square shaped states are Player 2' states.

Assume Player 1 plays the following strategy: when the game is in state 0 , he chooses to go to 2 , and when the game is in 3 , he chooses to go to FINAL. If Player 1 plays this strategy, for any strategy of Player 2, the game is bound to end in FINAL. Player 1's strategy is said to be winning if the objective of the game (for Player 1) is to reach FINAL (this is called a reachability objective).

On the contrary, if the objective of the game for Player 1 is to avoid FINAL (this is called a safety objective), he still has a winning strategy: always choose to go to state 1 .

Finally, if Player 1's objective is to visit 3 infinitely often (repeated reachability objective or Büchi objective), Player 1 has no winning strategy (he has to play a move and cannot refuse to play): if from 0 he chooses to go to 2 , Player 2 can choose to go to FINAL; if he chooses to got to 1 , Player 2 chooses to go back to 0 .

The type of strategies Player 1 has to follow is also an important parameter for a game. If Player 1 wants to play one of the strategies we have defined previously, he just has to observe the current state of the game. Such strategies are called memoryless or positional strategies. Player 1 could also consider waiting a bit before enforcing state FINAL and for instance choose to go to 3 the first time the game reaches 2 and the second time go to FINAL. He will then have to remember that 2 has been reached once which can be done using one bit of memory. More generally, Player 1 could choose to delay the winning moves n times (choosing to go to 3 for the first n times the game enters 2 ) and at the n + 1-th times the game enters 2 , he can choose to go to FINAL. All these strategies, when n is fixed are bounded memory strategies. There are also games and objectives that cannot be won with bounded memory strategies and in this case Player 1 needs to record the entire history of the game from the beginning, to be able to choose a correct move. To solve a control problem using a game theory approach, it suffices to let Player 1 be the controller and Player 2 be the system to be controlled (the environment). The control problem is then: is there a winning strategy for Player 1 ? A winning strategy is an actual controller to supervise the system.

Game Objectives

Given a game G, a control objective φ, solving (G, φ) stands for the following control problem: "Is there a strategy C for Player 1 in G to ensure C(G) |= φ?". If φ is a safety objective, and in this case we assume it is given as a set of states to stay in or to avoid, we have a safety control problem (SafCP). If φ is a reachability objective, we have a reachability control problem (RCP). We can define more complex objectives (repeated reachability, Büchi or co-Büchi) or even formulate them as (timed) temporal logic formulas.

Varieties of Untimed Games

A game as the one in Fig. 3.1 is a turn-based game. As for Chess or Draughts board games, players' moves alternate. A generalization of turn-based games can be obtained by tagging the states of the game with a shape either circle or square: in circle shaped states, Player 1 moves, and in square shaped states, Player 2 moves. In this case, the type of the state determines whose turn it is, but the turn does not always change in each round. This games are called state-based games and can be transformed in "equivalent" turn-based games. If the two players can play at the same time as in "Scissors Paper Stone", we have a concurrent game. We will briefly mention timed concurrent games in section 3.10.

Turn-based (finite) games enjoy nice properties. For instance they are determined for a large class, say B (that includes Büchi objectives), of control objectives [MAR 75]. Being determined means that in each state of the game, either Player 1 can win (G, φ) (φ taken in B), or Player 2 can win (G, ¬φ) where ¬φ is the complement of φ (this implies that B is closed under complement). Concurrent games do not have this determinacy property.

Moreover, for the types of control objectives we have mentioned earlier (safety, reachability, repeated reachability, . . . ), turn-based and concurrent (untimed) games satisfy the following properties [THO 95]:

-it is decidable in polynomial time whether Player 1 has a winning strategy for (G, φ); -if Player 1 has a winning strategy for (G, φ), he has a memoryless or positional winning strategy; -if Player 1 has a winning strategy for (G, φ), there is a "most permissive" strategy which is memoryless as well.

The remainder of this chapter is organised as follows. Section 3.2 introduces the basic notions of timed games and their formal definitions, together with strategies. In Section 3.3, we give algorithms to solve the safety control problem for timed automata. The following sections consider more advanced topics related to the control of timed systems. Section 3.4 points out one limitation (related to the practical implementation of controllers) of the previous algorithms, and in Section 3.5, we focus on the notion of implementable controllers. In the following Section 3.6, we review some results on more complex control objectives. Section 3.7 addresses the problem of optimal control for reachability timed games. Efficient on-the-fly algorithms for controller synthesis are described in Section 3.8; a good complement to this section can be found at the end of Chapter 6. Finally, Section 3.10 considers an extended model of timed games introduced in Section 3.2.

Timed Games

The aim of this first section is to define the formal framework of timed games and related notions. The definition of timed games used in the sequel has been introduced in [ASA 98, MAL 95]: it is an extension of timed automata in which the set of actions is split between both players. Besides these discrete actions, each player can also decide to wait in the current location: in this case, time will elapse until one of the player possibly decides to perform an action.

Timed Game Automata

DEFINITION 3.1 (TIMED GAME AUTOMATON, TGA).-A timed game automaton (or simply timed game) is a 7-tuple G = (L, 0 , X, Σ 1 , Σ 2 , E, Inv ) satisfying the following conditions:

-Σ 1 and Σ 2 are disjoint alphabets; -(L, 0 , X, Σ 1 ∪ Σ 2 , E, Inv) is a timed automaton (following Definition 2.2 of Chapter 2).

A timed game is thus a timed automaton the actions of which are associated with players: transitions that belong to the controller are called controllable, and the other ones belong to the environment and are called uncontrollable.

Informally, a play in a timed game proceeds as follows: it starts in an initial location 0 with all clocks set to 0, and is made of a sequence of action and delay transitions. Delay transitions are the "default" transitions, and occur as long as no player decides (or can) play an action transition. In the special case of turn-based games, the delay in each location is decided by the player controlling that location. EXAMPLE 3.1 .-An example of a timed game is depicted on Fig. 3.2 [CAS 05]. Dashed transitions are uncontrollable (labelled with Σ 2 ), and solid transitions are controllable ones (labelled with Σ 1 ). This rule will be used all along this chapter.

In this example, all invariants are true, so that it is always possible to let time elapse. Assume that the controller decides to play action c 1 when x = 1. If the environment does not play action u 2 in the meantime, then the transition corresponding to action c 1 will be fired, and the game will end up in location 1 with x = 1. The controller will then have the opportunity to wait for an extra time unit, and then play action c 2 , leading to his GOAL state. Notice that, when in location 1 with x ≥ 1, the environment cannot play any action. He has to wait until the controller decides to play an action.

Of course, given the strategy "play action c 1 when x = 1" of the controller in the initial location, the environment could also have decided to play an action at an earlier time instant, for instance by playing u 2 when x = 0.5 (notice that u 1 is only available when x > 1). The play would then have moved to ( 2 , x = 0) (since the transition from 0 to 2 resets clock x). Those examples informally illustrate the intuition behind timed games. We now define the corresponding mathematical framework, which will allow us to formally check properties of those games.

In the sequel, we fix a game G = (L, 0 , X, Σ 1 , Σ 2 , E, Inv ).

Strategies and Course of the Game

Several different semantics have been proposed for timed games: time indeed requires to fix the "rules of the game". We begin here with a natural definition of the semantics of timed games as proposed in [MAL 95]. Section 3.10 will stress the drawbacks of this semantics (especially regarding strategies consisting in "stopping time") and propose another approach to remedy this problem [ALF 03].

The Course of a Timed Game

The definition of a run of a timed game is that of the underlying timed automaton; following Definition 3.1, a timed game is a timed automaton whose actions are partitioned between controllable and uncontrollable actions. Given a timed game G = (L, 0 , X, Σ 1 , Σ 2 , E, Inv), we write T G for the timed transition system which gives the semantics of G (see Chapter 2). A run of the timed game G is a run of the timed transition system T G : it is a sequence

ρ = s 0 d1 -→ s 0 a1 -→ s 1 d2 -→ s 1 a2 -→ • • • dn-1 ---→ s n an --→ s n • • • where a i ∈ Σ 1 ∪ Σ 2 , d i ∈ R ≥0
, and in which configurations s i and s i are pairs ( , v) with ∈ L and v is a clock valuation. Delay and action transitions thus alternate (two consecutive delay transitions can be merged, and the last delay transition of a finite run can have infinite duration).

The set of runs of the timed game G is written Exec G . We also define the subset of maximal runs as being the set fo runs that cannot be extended. This includes several kinds of runs:

-runs having infinitely many action transitions; -finite runs with infinite duration; -finite runs with finite duration from which no delay nor action transition is possible.

We write Exec m

G for the set of maximal runs of G, and Exec f G for the set of its finite runs. The length of a finite run is the number of its transitions (both delay and action transitions) along that run.

Strategies

Strategies are the central concept in game theory. A strategy tells the player how to play, depending on the history of the game. In the case of timed games, players are allowed to wait and stay idle (this is the λ transition in the definition below). As will be seen in the sequel, both players have to agree on playing that special action in order to let time elapse. As soon as one of the players decides to play one of his available actions, time will stop elapsing and the action will be played. DEFINITION 3.2 (STRATEGY).-Let j ∈ {1, 2} be a player of G. A strategy for Player j is a mapping s : Exec f G → Σ j ∪ {λ} satisfying the following conditions: given a finite run ρ ending in state q = ( , v),

-if s(ρ) = a ∈ Σ j , then there must exist a transition q a --→ q in T G ; -if s(ρ) = λ, then there must exist a positive delay d > 0 such that q d -→ q in T G .
These conditions encode the fact that any action (including the λ action) proposed by a strategy must be allowed in the game G. The set of strategies of Player j in G is denoted by Strat j (G).

When a player plays according to a given strategy, he narrows the set of possible runs of the game to runs that comply with that strategy. DEFINITION 3.3 (CONTROLLED GAME).-Let q = ( , v) be a state of G, and s be a strategy for Player 1 (the case of Player 2 would be symmetric). The set of finite outcomes of s from q, denoted by Out f (q, s), is defined inductively as follows:

q is the only zero-length run in Out f (q, s);

-any finite run of G of the form ρ = ρ σ -→ q (hence having positive length) belongs to Out f (q, s) if, and only if, ρ belongs to Out f (q, s) and one of the following three conditions holds:

σ ∈ Σ 2 ; σ ∈ Σ 1 and σ = s(ρ);

-σ ∈ R >0 and for any d such that 0 ≤ d < σ, it holds s(ρ d -→ q ) = λ.
The set of maximal outcomes of s from q, denoted with Out m (q, s), is the union of the following two set of outcomes:

-the set of maximal finite runs in Out f (q, s); -the set of infinite runs all of whose prefixes are in Out f (q, s).

It is understood in this definition that a player can remember the whole history of the play for applying his strategy. However, some strategies have the special feature of being independent of the history and only depending on the current state of the system. Those strategies are called positional or memoryless strategies. In those special cases, in order to alleviate notations, we will see those strategies as mapping from the set of states to the set of actions of the corresponding player. Below is an example of a positional strategy. EXAMPLE 3.2 .-We stick to the example of Fig. 3.2, and consider the following memoryless strategy s:

-from states of the form ( 0 , v) with v(x) < 1, Player 1 (the controller) plays action λ. When v(x) = 1, he plays c 1 . If ever v(x) > 1, he again decides to play λ (as this is his only allowed action). Formally, s(

0 , x < 1 ∨ x > 1) = λ and s( 0 , x = 1) = c 1 ; -from ( 1 , v), he plays λ as long as v(x) < 2, and c 2 when v(x) ≥ 2, i.e., s( 1 , x < 2) = λ and s( 1 , x ≥ 2) = c 2 ; -from ( 2 , v), he plays c 3 , hence s( 2 , v) = c 3 ; -from ( 3 , v), if v(x) < 1, he plays λ, and plays c 4 when v(x) = 1. When v(x) > 1, he has to play λ. Hence s( 3 , x < 1 ∨ x > 1) = λ and s( 3 , x = 1) = c 4 ;
-from 4 and GOAL, Player 1 has no choice and only has to wait:

s( 4 , v) = s(GOAL, v) = λ.
Among the outcomes of this strategy from ( 0 , 0), some directly go to 1 , some others go via 2 and 3 (in case Player 2 plays u 2 ), but one is easily convinced that no outcome can ever reach 4 , and that actually all the outcomes eventually reach GOAL.

Let Ω be a set of runs (intended to represent the set of winning plays) defining the control objective. In the sequel, we write (G, Ω) for the game G under the winning objective Ω (for Player 1).

DEFINITION 3.4 (WINNING STATE, WINNING STRATEGY

).-Let s ∈ Strat j (G) be a strategy for Player 1. We say that s is winning from state q for Ω if Out m (q, s) ⊆ Ω, i.e., , if all the maximal outcomes meet the objective.

A state q is winning for Player 1 if he has a winning strategy from q. We write WinState 1 (G, Ω) for the set of states of G that are winning for Player 1.

Finally, a strategy s is said to be winning in (G, Ω) if it is winning from the initial state: Out m (( 0 , v 0 ), s) ⊆ Ω. We write WinStrat j (G, Ω) for the set of winning strategies of Player j. In the sequel, we focus on winning strategies for Player 1 (the controller). We thus write WinStrat(G, Ω), being understood that it refers to player 1. We also sometimes omit to mention Ω when it is clear from the context. EXAMPLE 3.3 .-Back to the example of Fig. 3.2, location GOAL is the reachability objective of the controller. The set Ω is then the set of (maximal) runs visiting that location. The strategy s defined above is then winning from the initial state.

Computation of Winning States and Strategies

Controller synthesis algorithms for timed automata are given in [ALF 01, ALF 03, ASA 98, MAL 95]. They compute fix-points (as for untimed games): the set of states which are winning in n steps is computed inductively. When n tends to infinity, all the winning states are collected. These algorithms terminate because the region equivalence relation on clock valuations introduced in Chapter 2 is also a good equivalence relation for timed games.

In this section, we use a running example depicted in Fig. 3.3 where the control objective is to avoid location BAD. The results of the synthesis algorithms for this example are given at the end of this section.

Controllable Predecessors

In order to implement our inductive fix-point algorithm, we define the controllable predecessors of a set of states: indeed, to win a game in at most n + 1 steps, the controller must have a strategy to force in one step, a state from which it can win in at most n steps.

Let G be a timed game, and T G the timed transition system which is the semantics of G. For a given subset X of S (set of states of T G ), we define the sets CPre(X) and UPre(X) by:

CPre(X) = {q ∈ S | ∃c ∈ Σ c such that q c -→ q et q ∈ X}; UPre(X) = {q ∈ S | ∃u ∈ Σ u such that q u --→ q et q ∈ X}.
These two sets are respectively the set from which the controller can force, with a controllable transition, the game into the set X, and the set from which the environment can force, with an uncontrollable transition, the game into the set X. To complete the definition we have to take into account the time elapsing action λ. Fig. 3.4 depicts the conditions for a state q to be a controllable predecessor of a set of states X: the controller must be able to force the game into a state of X, first by time elapsing (λ) and then by firing a controllable transition c; and from each state q t encountered during the time elapsing phase, the environment must not be able to fire an uncontrollable transition leading outside of X (denoted X).

In Fig. 3.4, state q is not a controllable predecessor of X, because during the time elapsing phase, the game reaches a state in UPre(X), from where the environment can force the game in X. On the contrary q is a controllable predecessor of X.

DEFINITION 3.5 (CONTROLLABLE PREDECESSOR)

.-A state q is a controllable predecessor of X iff: X CPre(X) UPre(X) q q Figure 3.4. Controllable Predecessors
1) there is some δ ≥ 0, such that q δ -→ q and q ∈ CPre(X);

2) for all 0 ≤ t ≤ δ such that q t -→ q t , we have q t ∈ UPre(X).

The set of controllable predecessors of X is denoted π(X).

In Fig. 3.4, the black lined polygon corresponds to the controllable predecessors of the set X. In the example of Figure 3.3, the state ( 1 , x = 1) is a controllable predecessor of ( 2 , x = 2): a controller can let time elapse (1 time unit) until ( 1 , x = 2) and then fire c 2 from 1 to 2 . During the time elapsing phase no uncontrollable transition can be fired. REMARK 3.1 .-This definition of controllable predecessors is an extension of the one given for discrete games. It does not take into account the special features of timed games, like liveness enforced by invariants. For instance, for a reachability game with control objective GOAL, and one uncontrolable transition (0, x ≤ 1, u, ∅, GOAL) with Inv(0) ≡ x ≤ 1, the environment must play action u before the time point 1. Thus if we would take this into account, a controller could win just by waiting.

It is possible to take into account the cases where the environment is bound to play by modifying the previous definitions. The results we give in this section are still valid in this case.

Symbolic Operators

The semantics of a timed game automaton is a timed transition system, and as for model checking of timed automata, the set of states is infinite. Thus we must develop symbolic techniques, gathering states in "families" which have the same properties.

We will use the notion of equivalence, regions, between states introduced in paragraph 2.4.2 of Chapter 2. To prove the correctness of this approach, we must show that two states in the same region have the same properties regarding their winning status. If this holds, we can can compute the controllable predecessors of a region. The following Lemma summarizes these two claims: LEMMA 3.1 .-If Z is a (finite) union of regions (we say a zone), then: P 1 : CPre(Z), UPre(Z) and π(Z) are unions of regions (thus zones), P 2 : CPre(Z), UPre(Z) et π(Z) can be effectively computed.

Proving the previous Lemma requires the introduction of an intermediate symbolic operator which computes the states from which a set of states A can be reached by time elapsing without encountering a state in a set B. This operator is given by:

Pre t (A, B) = {s ∈ S | ∃δ ≥ 0. s δ -→ s ∧ s ∈ A ∧ ∀0 ≤ t ≤ δ. [(s t -→ s ) ⇒ (s / ∈ B)]}.
Taking A = CPre(X) and B = UPre(X) allows us to define a symbolic version of the controllable predecessors operator π using Pre t : π(X) = Pre t (CPre(X), UPre(X)).

EXAMPLE 3.4 .-For the automaton of Fig. 3.3, we have CPre(

1 , x ≤ 3) = ( 0 , x ≤ 3) and if Z = ( 0 , x ≤ 4) ∪ ( 1 , x ≥ 0) ∪ ( 2 , x ≥ 0) then π(Z) = Z avec Z = ( 0 , x ≤ 3) ∪ ( 1 , 0 ≤ x ≤ 3) ∪ ( 2 , x ≥ 2).

Symbolic Computation of Winning States

We can now proceed to the symbolic computation of winning states of a timed game. A symbolic state of a TGA is given as a finite union of pairs ( , Z) where is a location of the TGA and Z a zone. We assume we have to solve a safety game, and the set of bad states to avoid, is given by BAD which is a symbolic state. The set of winning states of such games is the greatest fix-point of the mapping h : X → BAD ∩ π(X). As h is a monotonic (decreasing) mapping, this is well defined. To compute this fix-point, we start by computing h(S) (where S is the set of states of the game), then h(h(S)), and so on. This algorithm produces a decreasing sequence of symbolic As we can effectively decide whether the initial state of a TGA belongs to the symbolic representation h * we can decide whether there is a winning strategy using h * and moreover: THEOREM 3.1 ([ASA 98, HEN 99B]).-The control problems SafCP and RCP are decidable for TGA and EXPTIME-complete.

X i 0 1 2 0 0 ≤ x ≤ 4 0 ≤ x ≤ 5 0 ≤ x ≤ 5 1 0 ≤ x ≤ 4 0 ≤ x ≤ 3 2 ≤ x ≤ 5 2 0 ≤ x ≤ 3 - - (a) Winning States 0 1 2 λ x < 3 x < 3 x < 5 c x ≤ 3 2 ≤ x x ≤ 5 (b) Most Permissive Strategy f *

Synthesis of Winning Strategies

To solve the Control Synthesis Problem for a safety game, we can define a most liberal or most permissive strategy. Actually, this strategy is not a strategy in the sense of section 3.2.2.2 as it maps states to sets of controllable actions and not to a single controllable action. The most permissive strategy f * associates with each run ρ a set of actions from Σ c ∪ {λ} which are safe: every non-blocking strategy f (in the sense of section 3.2.2.2) such that f (ρ) ∈ f * (ρ) is winning and conversely a strategy f is winning only if f (ρ) ∈ f * (ρ). This is why f * is called the most permissive strategy. For the synthesis problem we have the following result: THEOREM 3.2 ([ASA 98]).-If G is a timed game automaton such that the initial state of G is winning for a safety objective, then there is a positional winning most permissive strategy f * .

To compute this most permissive strategy, we begin by strengthening the guards of the controllable transitions such that, from a winning state s, firing the transition with the strengthened guard leads to a winning state. This amounts to computing a most liberal pre-condition. In our case, we strengthen (the guard of) transition c 1 by x ≤ 3, c 2 by x ≥ 2 (which ensures that c 2 is not fired too early). The most permissive strategy is then defined by: wait in each winning state s such that there is some δ > 0 and s δ -→ s with s winning; fire a controllable transition c i if the strenghtened guard is satisfied. For the example of Figure 3.3 the most permissive strategy is given in Table 3.1(b). Notice that to obtain a non-Zeno strategy, one should not choose infinitely often λ in 0 (or 1 , 2 ), but at some point in time we should fire c 1 . Using the previous method we can compute a timed automaton C (given in Fig. 3.5) which is a representation of the most permissive strategy f * , and such that Reach(C(G)) ⊆ φ with φ = Reach(G) \ {BAD}. For reachability games, computing a winning strategy may be a bit more complicated. A correct algorithm is given in [BOU 04b] for this case.

K 0 [z≤3] K 1 [z≤3] K 2 [2≤z≤5] z := 0 u u u z ≤ 3; c 1 z ≥ 2 c 2 c 3 z := 0

Zeno Strategies

Fix-point algorithms presented in Section 3.3 compute the set of winning states, and the corresponding winning strategies. However, we did not take into account the so-called "Zenoness" problem: it could be the case -and is the case in the example of Fig. 3.6 where the aim is to always avoid the BADstate-that a state is winning thanks to non-realistic strategies. In the example of Fig. 3.6, the strategy of the controller consists in firing transition c infinitely many times during the first time unit, thus preventing clock x to reach value 1. Such a controller is called a Zeno controller and is not realistic because physical time cannot be stopped. Symmetrically, there is no strategy for the environment to reach the BAD state in this game, since any strategy of the environment has to "wait" as long as x ≤ 1. Hence the controller can fire transition c at dates 1 -1/n, which yields an infinite run never reaching BAD.

As will be seen in Section 3.10, a (rather technical) solution exists to rule out those non-realistic strategies. More generally, control problems (in particular for safety games) have been extended to generate implementable controllers (thus in particular non-Zeno). This extension is presented in the following section.

Implementability

Variants of the safety control problem SafCP have been proposed in many papers [HEN 99a, HEN 99b, ASA 98, MAL 95].

In the paper [CAS 02], we can find a classification of these problems according to the following criteria:

-discrete time control: can we control the system with a controller that reacts every β time units? This is the Known Sampling Rate (KSR) control problem. A more general question is ask for the computation of a value β such that the system is controllable. This is the Unknown Sampling Rate (USR) control problem.

-dense time control: in this setting the controller can either (i) control time elapsing, which is the setting of the seminal papers [MAL 95, ASA 98]; in this case this is the Unknown Switch Condition (USC) control problem; or (ii) cannot control time elapsing and in this case this is the Known Switch Condition (KSC) control problem.

The decidability status of the standard safety control problem SafCP also depends on the expressive power of the formalism used to specify timed games. Before giving the decidability status of the previous problems we review some well-known classes of extensions of timed automata.

Hybrid Automata

The more general class that is usually considered for the control problem SafCP is the class of Linear Hybrid Automata (LHA) [HEN 96]. The reader is refered to Chapter 7 for a detailed presentation of LHA. This class extends timed automata in the following manner: (i) the evolution rate of the variables2 are given by intervals of the form 1 ≤ ẋ ≤ 3; (ii) guards and resets are linear functions like 2x + 3y ≤ 4 et x := 3y -7z.

An interesting subclass of LHA is the class of Rectangular Automata (RA) introduced in [HEN 99b]. For RA, the guards and resets cannot involve two distinct variables: they are of the form x ≥ 1 ∧ y < 2 and for resets x :=]2, 3] to assign a value v with 2 < v ≤ 3 to x. This class has interesting and surprising decidability results: the reachability problem is decidable for RA [HEN 99b]. A subclass of RA is the class of Initialised Rectangular Automata (IRA): if a derivative of a variable changes on a transition from to , then the variable must be reset on this transition.

The reachability problem is decidable for RA but for any subclass if becomes undecidable [HEN 98]. Another interesting class of hybrid systems with good decidability properties, is the class of O-minimal Automata, (OminA) [LAF 00]: in this model, the dynamics can be non-linear (exponential or any o-minimal theory) but all the variables must be reset when firing a discrete transition.

Decidability results for the safety control problem on LHA are summarised in Table 3.

On the Existence of Non-Implementable Continuous Controllers

In [CAS 02] it is proved that the USR-CP is undecidable, even for the class of timed automata. Another result of the paper is that, there are systems that can be controlled with a dense time controller (USC), but by no sampling controller (USR). We System Given by: KSC USC KSR USR Timed Auto.

√ have given an example of such a system, given by the timed automaton of Figure 3.7. This timed automaton can be controlled with a non-Zeno controller. In this example, all the transitions are controllable. To avoid location BAD, it suffices to avoid firing a d-transition. This can be achieved by computing a most permissive controller: this controller C only requires to leave 2 when x < 1, and thus we add the invariant [x < 1] to location 2 . The controller C has to do the sequence of actions (a.b.c) ω , but the time elapsed between the n + 1-th a and the n + 1-th b must be smaller than for the previous round n. More precisely, if the time elapsed between the n-th a and the n-th b is δ n , the controller has to ensure that +∞ i=1 δ i ≤ K where K ≤ 1. Because of this, no sampling controller can control the system: given a sampling rate β, after a finite number of rounds m, the sum m i=1 δ i is beyond 1. The controller C is non-zeno (and non-blocking) because the n-th a action occurs at time n. This shows dense time controllability does not imply sampling controllability. In other words, if the answer to the USC-CP is "yes", the most permissive controller is not always implementable on a digital controller.

x := [0, 1[ y := 0 [x≤2] l 0 l 1 l 2 BAD x = 1 x := 0 a y = 1 z := 0 b z > 0 y := 0 c d x ≥ 1 d x ≥ 1 ∧ z > 0 d x ≥ 1 Figure 3.7.
A system that cannot be controlled with a sampling controller

Recent Results and Open Problems

The main undecidability result of [CAS 02] can be extended to intervals of the form [α, β] i.e., we impose that a controllable action occurs within [α, β] after the preceeding controllable action. The proof of this result is given in [DOY 07].

The previous result show that the notion of implementable controllers is important and must be addressed in the control problem. This aspects of the control problem have been extensively studied by Jean-François Raskin and his group in [DEW 05a, DEW 05b, DEW 04a, DEW 04b] and a synthesis of this work (in French) is given in [ALT 05].

An open problem is the direct synthesis of implementable or robust controllers which woudl extend the corresponding results on robust model checking [BOU 06f, BOU 08b].

Specification of Control Objectives

In the previous section, we have considered safety (or reachability) control objectives. In this section, we model the systems by timed automata and focus on more general types of control objectives.

In [ALF 01] the authors give an algorithm to deal with general ω-regular control objectives. They consider ω-regular objectives on TGA with a "surprise" semantics (see section 3.10 in this Chapter). They show that the CP with this "surprise" semantics is EXPTIME-complete. It is to be noticed that those control objectives are often called internal in the sense that they refer to the state properties (and clocks) of the system to be controlled. The safety and reachability properties that we have considered previously are examples of internal property. In the case of timed systems they only refer to the untimed sequences of states of the system and thus have a restrictive expressiveness: it is possible to specify a property like "from a state satisfying p we must reach a state satisfying q" but nothing like "from a state satisfying p we must reach a state satistying q within d time units" (bounded liveness). In [FAE 02a], the authors show that the control problem is 2EXPTIME-complete for specifications given by LTL formulae3 .

A control objective is a property of a closed system, and it is natural to write properties using temporal logics or automata, i.e., , to give the set of timed words the controlled system has to generate. The language 4 L(A) accepted by a timed automaton is a set of behaviours (timed words) and this can be considered to be a control objective: in this sense this is an external control objective. Notice that it can either specify good or bad behaviours. Assume we have two timed automata: A d which defines the desired (permitted) behaviours of the system, and A u which defines the undesired behaviours. Let S be the system we want to control. The External Specification Control Problem, (ESCP) is the following:

is there any C s.t. (1) L(C(S)) ∩ L(A u ) = ∅ et (2) L(C(S)) ⊆ L(A d ) ? [ESCP]
In the paper [DSO 02], the authors prove that: 1) the sub-problems ESCP.(1) and ESCP.(2) are undecidable when A d and A u are non-deterministic timed automata;

2) these problems become decidable if A d and A u are deterministic; deterministic timed automata can be complemented and in this case the ESCP can be reduced to a (internal) safety control problem;

3) the control problem ESCP.( 2) is decidable and 2EXPTIME-complete if the resources (number of clocks, granularity and constants used in the specification) of the controller are bounded, and this even if A u is non-deterministic. ESCP.(1) remains undecidable even for bounded resources.

Expressing control objectives using timed automata is a very powerful tool and there is a gap between the control objectives we considered previously (safety or reachability) and these very general class of ω-regular properties. Temporal logics are a less powerful yet often sufficient specification formalism for most properties needed in practise.

In [BOU 06a], the authors consider a timed extension of LTL namely MTL [KOY 90].

The control problem is undecidable for MTL specifications but become decidable if the resources of the controller are bounded (it is still non primitive recursive). In [FAE 02b], the authors consider TCTL specifications without equality and prove that the control problem (for timed automata) can be decided in exponential time for this type of specifications.

In [BOU 05b], control objectives are specified using the (timed) temporal logic L ν (more precisely a fragment L det ν of L ν ) which is a fragment of the timed µ-calculus: it allows to specify bounded safety properties.

What is interesting is that the CP for L det ν control objectives can be reducec to model checking problem and this later problem is EXPTIME-complete.

Finally, there is a nice logic which was specifically designed to specify properties of open (discrete) systems: Alternating-time Temporal Logic (ATL) [ALU 02]. This logic is an extension of CTL where the path quantifiers are replaced by "strategies quantifiers". It is possible to write a property like "Player 1 has a strategy to reach a state from which Player 2 will not be able to reach a winning state".

Several recent papers have extended the definitions of this logocs to timed systems. One can then write a property specifying that a winning state must be reached "within five time units". The extended logic has been studied for time automata operating in discrete time [LAR 06], and PTIME algorithms are proposed for model-cheking the extended logic. For timed automata in dense time, some results are available [BRI 07, HEN 06a] but the semantics iof TGA s a bit different from the one we have introduced so far (see section 3.10).

Optimal Control

If we consider the reachability Reachability Control Problem (RCP)" we want to synthesise a controller which enforces a particular state or location q. Once solved, we can ask for the controller to be optimal e.g. the state q is reached as soon as possible with the controller. This version of optimal control called time-optimal control was solved in [ASA 99].

Timed Automata with Costs

A few years later in 2001, timed automata were extended with costs or prices: this extension was called priced timed automata (PTA) in [BEH 01b, BEH 01a] and weighted timed automata (WTA) in [ALU 01] (both models are exactly the same thing but they were proposed independently at the same time by two different groups.)

The notion of cost or price generalises the notion of elapsed time: the cost is a linear function of the elapsed time in each location, and is an integer value on each discrete transition. In the example of Figure 3.8, the costs in the PTA A are given by the keyword cost.

When the cost is associated with a location, it stands for the cost per time unit when time elapses in this location. When it is associated with a discrete transition, it stands for the cost of firing the transition. Assume δ time units elapse in location 0 , and then c 1 is fired. The invariant on 1 prevents time from elapsing in 1 . This location is a choice location in which we immediately go either to 2 or 3 . Assume we choose 2 and let δ time units elapse before firing c 2 . In this case the total cost of this execution is 5 • δ + 10 • δ + 1. In PTA all the transitions are controllable.

The optimal-cost computation problem for PTA consists in computing the minimal cost to reach a particular location. The (smart) solutions to the optimal-cost computation problem for PTA were simultaneously proposed in [ALU 01, BEH 01b]. Notice

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 If we consider PTA and a dual problem i.e., keep the system in a set of states, we can define an optimal problem as well: here the model has costs and rewards, and the aim is to minimise the limit of the ration cost/reward on infinite runs. This latter problem was solved in [BOU 08a, BOU 04a].

A step further consists in defining a logic which can refer to cost values: such a logic, WCTL, has been defined in [BRI 04], and extends TCTL with cost variables. Inside this logic, it is possible to write a formula which which states "it is possible to reach a state q and this at a cost which is less than K." The model-checking problem for WCTL against timed automata was proved undecidable (even if the time domain is discrete). Nevertheless, for a subset of WCTL, there are some classes of timed automata for which model-checking is decidable. Recently in [BOU 07], the authors have proved that WCTL was decidable for o-minimal PTA. The formal definition of a priced timed game automaton is the follwoing: DEFINITION 3.6 (PRICED TIMED GAME AUTOMATON).-A priced timed game automaton (PTGA) is a pair (G, cost) where G = (L, 0 , X, Σ 1 , Σ 2 , E, Inv) is a timed game automaton and cost is a cost mapping such that: cost : L ∪ E → N, i.e., cost assocaites with each loation a cost per time unit and a firing cost with each discrete transition. Let

T G = (Q, Q 0 , Σ 1 , Σ 2 , Γ, δ) be the semantics of G. If ρ is the run of T G defined by: ρ = ( 0 , v 0 ) (δ1,e1) -----→ ( 1 , v 1 ) (δ2,e2) -----→ . . . (δn,en) -----→ ( n , v n )
we can define the cost of ρ by:

Cost(ρ) = n-1 i=0 cost( i ) × δ i+1 + cost( i ei --→ i+1 ) .
The cost of a run is thus the sum of the discrete costs and the delay costs.

Optimal Cost in Timed Games

We can now formulate the optimal-cost problem for timed games. In this case we start with a model which is a Priced Timed Game Automaton (PTGA) i.e., a TGA enriched with costs. We consider here reachability games: the aim is to reach a location at an optimal cost, and this optimal cost is the best the controller can ensure, whatever the adversary (environment) does. The automaton A of Figure . 3.8 is an example of a PTGA. Uncontrollable transitions are labelled by u. Notice that in this game, there is a controller which can enforce location GOAL: fire c 1 and then whatever the environment chooses in 1 , fire c 2 . In the sequel, we assume that the reachability control problem has been solved and the answer was "yes" i.e., there is a controller which can enforce GOAL. Our problem is now to compute the optimal cost. This optimal cost is defined as the minimum value the controller can guarantee whatever the environment does. For example, in the PTGA A of Figure 3.8, there are two families of runs: the runs in which the environment chooses to go from 1 to 2 and the runs in which it chooses to go from 1 to 3 . The only real decision the controller has to make is to choose how long to wait in 0 before firing c 1 (indeed when in 2 or 3 it chooses to fire c 2 as soon as x ≥ 2.) Let δ be the amount of time the controller chooses to wait for in 0 . The costs that can result from this choice depend on the choice of the environment: if it chooses i , i = 2, 3, the cost is respectively

α 2 (δ) = 5 • δ + 10 • (2 -δ) + 1 and α 3 (δ) = 5 • δ + 1 • (2 -δ) + 7.
Once the controller has fired c 1 , the environment will try to maximise the cost of the current run: it will choose i , i = 2, 3 such that α i (δ) is maximal. The aim of the controller is to minimise this maximum over all paths.

Thus the optimal cost for the PTGA A is defined by:

OptCost = inf 0≤δ≤2 max(5 • δ + 10 • (2 -δ) + 1, 5 • δ + 1 • (2 -δ) + 7).
For A, this value is 43 3 which means c 1 should be fired at the date 4 3 . The problem of computing automatically this optimal cost is the Optimal Cost Reachability Control Problem (OC-RCP).

Of course we can generalise the definition of the optimal cost given for A to PTGA. With the model of PTGA we have introduced, the time optimal control problem is a particular version: in each location, the cost rate is 1 and each discrete transition has a null cost.

Let WinStrat(q, G) be the set of winning strategies from q in G. Given a strategy s for the contrller, we can define the cost of s from a state q of T G by:

Cost(q, s) = sup {Cost(ρ) | ρ ∈ Out m (q, f )} .
DEFINITION 3.7 (OPTIMAL COST).-Let (G, cost) be a PTGA. We consider the RCP for G and the goal location is GOAL. The set of possible costs, Cost(q), from q in G when playing s is defined by:

Cost(q) = {Cost(q, s) | s ∈ WinStrat(q, G)}.
The optimal cost from q is OptCost(q) = inf Cost(q). The optimal cost for G, OptCost(G), is sup q∈Q0 OptCost(q). REMARK 3.3 .-Notice that we consider the supremum from the initial states of G and this means that we consider that the choice of the initial state is not controllable. If there is a single initial state (like in the following examples) we have OptCost(G) = OptCost(q 0 ).

The Cost Optimal Reachability Control Problem (CO-RCP) asks the following:

Given (G, cost), compute OptCost(G).

[CO-RCP]

Computation of the Optimal Cost

A first step towards a solution of the optimal cost reachability control problem was given for acyclic timed games in [LAT 02]. As the PTGA does not have any cycle, the computation of the optimal cost can be reduced to a linear optimisation problem.

If we consider PTGA which can contain cycles, it is not obvious that the algorithm proposed in [LAT 02] can be tuned to accommodate cycles. A solution to the OC-RCP was simultaneoulsy given by Alur et al. We detail here the algorithm of [BOU 04c] to solve the OC-RCP. The idea we propose to solve the optimal cost problem 5 for PTGA is the following: the OC-RCP 5. As emphasised earlier we assume there is a strategy to win the game i.e., to force GOAL. This ensures that the optimal cost exists and is an finite number. can be rephrased as: "What is the minimum amount of resources (time, petrol, . . . ) I should start with, to be able to enforce GOAL, and when GOAL is reached I have not run out of resources?" Thus to solve the OC-RCP we can proceed as follows:

1) we start with a PTGA A similar to the one given on Figure 3.8;

2) then we build a game H A , which is a timed game with a special variable rsrc: we end up with a timed game which is a special kind of linear hybrid automata (LHA). This variable stores the amount of resources which is left at each point in the game. Its value will then decrease in a location of H A with a rate which is the opposite of the rate of the cost in the corresponding location in A. Applied to A of Figure 3.8, this construction gives the automaton H A on Figure 3.9 (the notation ṙsrc stands for the first derivative of rsrc). The OC-RCP for PTGA can then be reduced to a (standard) Reachability Control Problem for a linear hybrid game 6 (LHA): the control objective is to enforce GOAL and a value of rsrc which is larger or equal than zero i.e., the control objective is (GOAL, rsrc ≥ 0). We know how to effectively compute the set of winning states for this type of (linear hybrid) games, and if the algorithm terminates we obtain a set of pairs of the form ( , Z) where is a location and Z a polyhedron. In particular we may obtain a set of pairs ( 0 , Z) giving the set of winning states (values of the variables) in the initial location. By definition of the algorithm to solve linear hybrid games, Z is the maximal winning zone i.e., if one starts outside Z, the game cannot be won.

0 ṙsrc = -5 1 [y = 0] 2 ṙsrc = -10 3 ṙsrc = -1 GOAL x ≤ 2; c 1 ; y := 0 u u x ≥ 2; c 2 rsrc := rsrc -1 x ≥ 2; c 2 rsrc := rsrc -7
The projection of the winning set Z in 0 on the variable rsrc gives the set of values of rsrc from which we can win the game i.e., enforce (GOAL, rsrc ≥ 0). We can prove that this set is of the form rsrc k with {>, ≥} and this means that the optimal cost is k. Decidability of the OC-RCP for PTGA is also reduced to the decidability of the RCP for the class of LHA that is obtained when we use our translation. Les résultats obtenus par cette démarche sont les suivants:

-for bounded PTGA (all the clocks are bounded) such that on each cycle, the cost is at least β > 0 (we call this class of PTGA, cost non-Zeno PTGA), the classical backward algorithm that computes the winning states of the associated linear hybrid game terminates; -the optimal cost can be obtained by computing the projection of the set of initial winning states on the variable rsrc. When the previous algorithm terminates, this set is always of the form rsrc k with {>, ≥} and k is the optimal cost. We can decide whether there is a strategy that guarantees the optimal cost, i.e., an optimal strategy: if the initial winning interval is of the form rsrc ≥ k the answer is "yes", otherwise it is of the form rsrc > k and there is a family of strategies that can ensure a cost k + ε for any ε > 0. Still there is no optimal strategy; -optimal strategies when they exist, may need cost information i.e., the accumulated amount of resources consumed since the game started. In this sense, the clocks of the PTGA are not always sufficient to decide what to do to ensure winning at optimal cost, and we may need the cost information.

Recent Results and Open Problems

Since these results were published, some new results about optimal cost for PTGA were obtained:

-in [BRI 05], the authors prove that the Cost non-Zeno the optimal cost computation problem is undecidable. This shows that the assumption we had made to prove termination of our algorithm is necessary. This proof was refined in [BOU 06c] and the most recent result is that for PTGA with 3 clocks the optimal cost computation problem is undecidable;

-in [BOU 06e], the authors prove that for turn-based PTGA with one clock, the optimal cost can be computed (3EXPTIME).

-finally, in [BOU 07], there is a proof that the optimal cost is computable for o-minimal automata.

An interesting open problem is the Cost Optimal Safety Control Problem where the goal is to minimize the cost over infinite runs. This can be viewed as the generalisation of the result in[BOU 08a, BOU 04a] (costs and rewards) to timed games with costs and rewards.

Efficient Algorithms for Controller Synthesis

In the last ten years, a lot of progress has been made in the design of efficient tools for the analysis (model-checking) of timed systems. Tools like KRONOS [YOV 97] or UPPAAL [AMN 07, AMN 01] have become very efficient and widely used to check properties of timed automata but still no real efficient counterpart had been designed for timed games.

One of the main reasons behind the efficiency of tools like UPPAAL is the on-thefly generation of the state space (this is also due to the use of efficient data structures in the implemtation of the algorithms). Notice that on-the-fly algorithms were already crucial for model-checkers for finite communicating systems like SPIN [HOL 07].

The algorithm for computing controllers for safety timed games described in section 3.3.3 is based on backwards fix-point computations of the set of winning states [MAL 95, ASA 98, ALF 01]. We call this algorithm a backward algorithm. A drawback of a backward algorithm is that it does not take into account the fact that a state is reachable from the initial state or not. Backward computation may thus yield an enormous set of winning (symbolic) states most of which could be non unreachable. Moreover, at each iteration, we compute the : pi operator for these unreachable states.

A more difficult problem is that for simple extensions of timed automata, it is very difficult and sometimes impossible to compute the controllable predecessor operator π. For instance, if transitions are of the form i := 2j + k (which is allowed in UPPAAL), computing the controllable predecessors of the symbolic state ( , j ≥ 0 ∧ k ≥ 0) means collecting all the values of i such that i = 2j + k. This computation can be very expensive. In practise, if we start from a given initial state and given j and k, there might be a few reachable (admissible) values for j and k and consequently a few for i. Or a least, for each new value of i which is reached, we know the values of j and k that were used to obtain i.

A first step towards a solution is to compute the set of reachable states R. Then for each step of the iterative algorithm using π for computing winning states, take the intersection on the winning states and R. Even if these sets are represented with efficient data structures this can be very expensive and imply the computation of the whole state space of the system which may be unncessary to check whether a winning strategy exists.

On-the-fly Algorithms

To obtain a real on-the-fly algorithm for computing winning states, we should not have to compute the set R of reachable states before we compute the winning set of states but rather explore the symbolic state space as needed.

Regarding timed games, in [ALT 99, ALT 02], Karine Altisen and Stavros Tripakis have proposed a (partially) on-the-fly method for solving timed games. This algorthm consists in first computing an abstraction of the region graph (which can be huge) and second use an on-the-fly algorithm on the abstraction. In this sense, this is not a real on-the-fly algorithm on the timed automaton as we first have to compute a finite abstraction of the set of reachable states.

To design a truly on-the-fly algorithm for the computation of winning states for reachability timed game automata we start from the on-the-fly algorithm suggested by Liu & Smolka in [LIU 98] for linear-time model-checking of finite-state systems.

To obtain an on-the-fly algorithm for TGA, we can first extend the algorithm suggested by Liu & Smolka in [LIU 98] to the RCP for finite automata.

The idea for this on-the-fly algorithm for a finite game A is the following. We assume that some variables store two sets of transitions: ToExplore store the transitions that have been explored and ToBackPropagate store the transitions the target states of which has been declared winning. Moreover, the set of explored states R of A is also stored. For each state s of A already explored we keep track of its statut which is either winning (this is te initial value for state s in GOAL) or unknown (this is the initial value for the other states).

To perform a step of the on-the-fly algorithm, we pick a transition (s, a, s ) in one of the two sets ToExplore or ToBackPropagate and we do step (A1) for a transition from ToExplore and (A2) for a transition from ToBackPropagate:

-(A1) we explore (s, a, s ):

-if s is encoutered for the first time, we add the outgoing transitions of s to ToExplore; if s is a winning state in GOAL, we update the status of s to winning and otherwise set it to unknown;

-if the status of s is winning, we add (s, a, s ) to the set ToBackPropagate; otherwise we just keep track of the fact that "the status of s depends on the status of s via transition (s, a, s )"; -(A2) we backpropagate some information for the transition (s, a, s ). Actually, if it is in ToBackPropagate, this must be because the status of s became winning recently and we have to update the status of s accordingly:

-either a is a controllable action, and in this case we update a counter c(s). The meaning of c(s) is "c(s) is the number of controllable transitions from s leading to a winning state"; -or a is uncontrollable and we increment a counter u(s). The meaning of u(s) is: "u(s) is the number of uncontrollable transitions from s leading to a winning state"; -Once c(s) or u(s) has been updated, the status of s may change. Let U (s) be the total number of uncontrollable transitions originating from s in A. If c(s) ≥ 1 and u(s) = U (s), s can be declared a winning state. The status of the states which depend on s has to be re-considered. Thus we add to ToBackPropagate all the transitions (s , a, s) such that the status of s depends on s via (s , a, s).

An on-the-fly algorithm for reachability games will process the sets ToExplore and ToBackPropagate in a random order. As soon as the status of the initial state of A is winning, we can stop the algorithm and the answer to the RCP is "yes" (moreover a winning strategy can be computed). This algorithm is linear in the size of A. Indeed, each transition is processed at most twice: once in ToExplore and once in ToBackPropagate. To design the on-the-fly version for timed games, we consider symbolic states or zones which are unions of regions. Given a TGA and a symbolic state ( , Z) we do a forward exploration of each transition from location to by computing the discret succesors of Z and the time successors (contrained by invariant). The status of the symbolic is then updated as for the untimed case. The on-the-fly algorithm for timed games together with the correctness proof are given in [CAS 05]. Actually, for timed games, the algorithm we give is not linear in the size of the region graph! We use zones to store symbolic states, and a region maybe included in several zones. Our algorithm is thus not optimal as there is an algorithm which is linear in the size of the region graph [ALT 99]. However, this algorithl is really on-the-fly, and in practise gives good results, as witnessed by the experiments carried out with the games version of UPPAAL called UPPAAL-TIGA [BEH 07a] which is presented in Chapter 6.

Recent Results and Open Problems

Using the previous algorothm, it is possible to compute time optimal controllers (cost associated with locations are all 1 and cost associated with discrete transitions are all 0). It suffices to give an upper bound on the maximum time to reach GOAL (see [CAS 05] for details). There is also a "safety games" version of the previous algorithm . In [CAS 07b], this on-the-fly algorithm has been adpated to games under partial observation (see next section 3.9). An ovserview of the on-the-fly algorithms for timed games us given in [CAS 07a].

Some open problems still remain:

-on-the-fly algorithm could be extended to more general control objectives like repeated reachability (Büchi objective). This is really useful for timed games as Büchi objectives allow to enforce a controller to be non-Zeno; -anotehr direction is to extend the previous algorithm and find good data structures to solve the optimal cost reachability control problem (see section 3.7).

Partial observation

In the previous sections, we (tacitly) assumed that the controller had perfect knowledge of the environment, and that it could observe all the actions and states of the system. In practice, it might not always be the case: in some cases, the controller can only observe some of the actions of the environment (which are said to be observable), and can only have partial informations about the current state of the environment. Still, we would like to be able, as much as possible, to control the environment: this problem is known as Control Under Partial Observation (referred to as PO in the sequel).

In this case, we keep assuming that the set of events is partitionned into two sets -controllable (Σ c ) and uncontrollable (Σ u )-but only a subset Σ o u of Σ u is observable. The controller is only able to observe a timed trace (a 0 , t

0 )(a 1 , t 1 ) • • • (a n , t n ) in ((Σ c ∪ Σ o u ) × R ≥0 ) *
, and based on this information, it must decide which actions to play.

As regards strategies, we say that a strategy f is trace-based if for any two runs ρ and ρ yielding the same observation 7 , we have f (ρ) = f (ρ ).

The control problem under partial observation (PO-CP) aims at deciding whether there exists a winning trace-based strategy f (i.e., a trace-based controller, TBC). The PO-CP problem is then the following: given a partially observable system S and an objective φ, does there exists a TBC C such that (S C) |= φ?

[PO-CP]

A survey on partial observation in timed systems is given in [BOU 05c]. In case the specification is given as a deterministic timed automaton, the PO-CP is undecidable [ BOU 03]. Even if we restrict to the safety fragment and if we are only interested in synthesizing non-Zeno controllers (Non-Zeno-PO-SCP), the problem remains undecidable [BOU 06d].

However, by fixing in advance the resources available to the controller, the proof of [DSO 02] on control with external specifications (see Sect. 3.6) can be extended to the partial observation setting. The result is then the following: if the resources available to the controller are fixed and if the control objective φ is given as a deterministic finite automaton, then the PO-CP is EXPTIME-complete [BOU 03].

Recent works [CHA 06, DEW 06] focus on partial observation of the states of a finite-state system. A timed extension of those works is given in [CAS 07b]. 3.10. Changing game rules . . .

As mentionned above when defining TGAs, several semantics have been defined for timed games. We present below an alternative semantics, based on [ALF 03], and whose main advantage is that it can handle Zeno strategies.

Informally 8 , the main difference in the rules is the following: instead of choosing between waiting and performing an action, each player concurrently choose an action and how long they want to wait before performing that action. The rest is identical: the player with the shortest delay is selected, and his action is performed after delaying for the amount of time this player had chosen.

Though this might look like a minor change, this semantics has one important advantage: at each step, we know which player has chosen the shortest delay. That way, along Zeno runs, we are able to detect which player has been unfair by choosing converging delays. The other player is declared the winner in this case 9 Let us go back to our example of Section 3.4, depicted on Fig. 3.10. Consider the following strategy: in state ( 0 , x) with x < 1, the controller proposes a positive delay δ such that, after this delay, the value of x is of the form 1 -1/n (this is always possible when x < 1). Together with this value, the controller decides to perform action c. With our new semantics, this strategy is not winning: it suffices for the environment to play the strategy "wait until x = 1 and perform action u" to win, since the controller will be disqualified. This setting has drawbacks unfortunately. For instance, even for simple reachability objectives, winning strategies might need memory: from state ( 0 , 0) of the game depicted on Fig. 3.11(a), the controller has to play c 1 at date 0 (in order to satisfy the reachability condition). The play will then come back to the same state ( 0 , 0) after the second move. If the controller is memoryless, he will keep applying this strategy, which results in a Zeno run.

8. We won't give the precise definition of those games in this chapter, and refer the eager reader to [ALF 03, BRI 07, HEN 06b], where the details can be found. 9. It could be the case that both players are disqualified. There is no winner in this case.

Even though the players cannot rely on Zeno behaviours to win, there are examples where it is necessary to apply a "Zeno strategy" for a finite number of steps. Figure 3.11(b) depicts such an example: the objective in this game being to reach state 1 , the controller will play action c at dates 1/2, 3/4, 7/8, etc., always letting 1/2 n+1 time units elapse between the n-th and n + 1-st step. This strategy is Zeno, but it is intended to be applied only a finite number of times. Plays that are winning for the environment under that strategy are plays in which the environment itself always plays smaller delays. In that case, the environment loses. Under such rules, most of the results presented in this chapter still hold. In particular, the notion of controllable predecessors can be extended to this setting, and zone-based arguments are still valid; that way, fixpoint techniques can be developped, still resulting in exponential time algorithms.

Recent extensions of those models have been proposed, where all the players can act upon the action to be performed even if they don't choose the smallest delay. Those games extend classical concurrent games [ALU 02] with clocks: in this setting, each player will not only tell his preferred delay and action, but also the actions he would like to perform is a smaller delay were to be chosen by some other player. The resulting action would then depend on all the choices of all the players, even if their preferred delays were too large. In [BRI 07], the techniques and results presented above have been adapted to this framework.

Bibliography

Figure 3

 3 Figure 3.1. A game example

Figure 3 . 2 .

 32 Figure 3.2. An example of a timed game

Figure 3

 3 Figure 3.3. A Timed Game Automaton S

Figure 3 . 5 .

 35 Figure 3.5. Most Permissive Controller C

Figure 3

 3 Figure 3.6. A safety game having a winning Zeno strategy

  5.1: The meaning of abbreviations are: KSC = Known Switch Conditions controller, USC = Unknown Switch Conditions controller, KSR = Known Sampling Rate controller, and USR = Unknown Sampling Rate controller. √ = decidable, × = undecidable. A recent result by Patricia Bouyer, Thomas Brihaye et Fabrice Chevalier [BOU 06b] is the decidability of the Reachability control problem, USC variant, for o-minimal automata.

Figure 3 .

 3 Figure 3.8. A PTGA A

  [ALU 04] and Bouyer et al. [BOU 04c, BOU 05a]. [ALU 04] gives some complexity results (lower bound) and in [BOU 04c] gives decidability results for PTGA as well as structural properties of the class of strategies (or controllers) that can win this type of games. The algorithm of [BOU 04c] was implemented in HYTECH [HEN 97] and this is described in [BOU 05a].

Figure 3 . 9 .

 39 Figure 3.9. The LHA HA built from A.

6.

  See 3.5.1 in Chapter 7.

  7. I.e., having the same projection on ((Σc∪ Σ o u ) × R ≥0 ) * .

Figure 3 .

 3 Figure 3.10. A (safety) game in which winning requires Zenoness

Figure 3 . 11 .

 311 Figure 3.11. Examples of timed games

Table 3 .

 3 1. Iterative Computation of h * for the Example of Figure 3.3state and as there is a finite number of such states, this computation terminates in a finite number of steps. When it stabilizes, the greatest fix-point h

* of h is computed: it is a subset of BAD, and from each state in h * the controller has a strategy to stay within h * by time elapsing and then firing a discrete transition. The set h * is also the largest subset of BAD that the controller can enforce. EXAMPLE 3.5 .-For the example of Fig.

3

.3, the iterative computation of h * is given in Table

3

.1(a): the winning zone for each location i appears in the corresponding column.

REMARK 3.2 .-For reachability games, the goal is to enforce a symbolic state GOAL. Thus the set of winning states is the least fix-point of the mapping h : X → GOAL ∪ π(X). Again, this least fix-point can computed iteratively by computing h(∅), h(h(∅)) and so on. Termination is ensured because the sequence of symbolic states which is computed is monotonic. For more complex control objectives (repeated reachability, . . . ), nested fix-points are required (see [MAL 95, ASA 98, ALF 01, ALF 03]).

Table 3 .

 3

2. Safety Control Problem: Decidability Results.

  [ALF 01] DE ALFARO L., HENZINGER T.A., MAJUMDAR R., "Symbolic Algorithms for Infinite-State Games", Proc. 12th International Conference on Concurrency Theory (CON-CUR'01), vol. 2154 of Lecture Notes in Computer Science, p. 536-550, Springer, 2001. [ALF 03] DE ALFARO L., FAËLLA M., HENZINGER T.A., MAJUMDAR R., STOELINGA M., "The Element of Surprise in Timed Games", Proc. 14th International Conference on Concurrency Theory (CONCUR'03), vol. 2761 of Lecture Notes in Computer Science, p. 142-156, Springer, 2003.

This may take a while in the case no such controller exists . . .

We note ẋ the derivative of x.

This result does not contradict the complexity result of [ALF 03] because the specification is given as an LTL formula and not by the automaton that recognises the valid sequences.

We consider languages over infinite words e.g. ω-regular languages.


Franck Cassez
email: franck.cassez@cnrs.irccyn.fr

The Dark Side of Timed Opacity

In this paper we extend the notion of opacity, defined for discrete-event systems, to dense-time systems. We define the timed opacity problem for timed automata and study its algorithmic status. We show that for the very restrictive class of Event Recording Timed Automata, the opacity problem is already undecidable leaving no hope for an algorithmic solution to the opacity problem in dense-time.

Introduction

Security issues have become increasingly important in the last decade with the development of the Internet. Various notions and theories have emerged to model, design and check that a given system is secure. These theories provide sound foundations for the analysis of security policies. For instance, many security policies like access control, channel-control can be formulated within the framework of transitive or intransitive non-interference (see [START_REF] Rushby | Noninterference, Transitivity and Channel-Control Security Policies[END_REF] for an excellent introduction to the subject).

Opacity. Non-interference cannot capture every type of security policies. Thus extension and generalization have been proposed to address relevant practical problems. Opacity was introduced in [START_REF] Mazaré | Using unification for opacity properties[END_REF][START_REF] Bryans | Opacity generalised to transition systems[END_REF] to model leaks of information from a system to an attacker. The framework of opacity is the following: a (model of the) system A is given which generates sequences of actions over an alphabet Σ. A secret S is a subset of the sequences of actions generated by A. An attacker can only see the generated sequences through an interface which prevents the observation of some of the events: he has only a partial knowledge of the events generated by A and sees the projection of a sequence over an alphabet Σ o ⊆ Σ. The secret S is opaque w.r.t. A and Σ o , if for every observation w the attacker can make, he can never infer that this observation was produced by a secret sequence in S.

Assume the system A can generate the sequences of events {ab, cb} and the attacker can only see Σ o = {b}. Let S = {ab} be the secret. Then S is opaque w.r.t. A and Σ o . Indeed the only observation the attacker can make is the sequence "b", but then, he cannot know whether this observation is the projection of ab or cb and thus cannot know the secret.

The opacity problem consists in checking whether a secret is opaque for a model of a system. Anonymity and non-interference can be reduced to opacity using a proper encoding [START_REF] Mazaré | Using unification for opacity properties[END_REF]. If the system A is given by a finite transition system over an alphabet Σ, the secret S is a regular language included in Σ * and the observation of an attacker is defined by a projection over Σ o ⊆ Σ, the opacity problem can decided [START_REF] Mazaré | Using unification for opacity properties[END_REF]. The previous introductory example can be modeled by the finite automaton A of Figure 1.

Taking Time into Account. In the above mentioned framework, the attacker can only observe sequences of events but not the point in time at which they occur. But time could be an important information for an attacker. Indeed, assume the system generates {ab, cb} as before, but when it generates ab, then "b" occurs at (global) time 1, and when it generates cb then "b" occurs at (global) time 2 (for instance, the system is slower when doing the "c" action than doing the "b"). Using this timing information, and yet observing only "b", an attacker can know whether an "a" or a "c" has occurred: if "b" occurs at time 1, the system generated ab, otherwise if "b" occurs at time 2, it generated cb. If the secret is ab as before, then it is no more opaque for an attacker who has a clock. Taking into account the ability of the attacker to measure time gives a more accurate and realistic model of the system. Whether it is dense-time of discretetime is important as it has been shown that the expressiveness of dense-time models (timed automata) is strictly larger than discrete-time ones [START_REF] Alur | A theory of timed automata[END_REF]. In this paper we use timed automata [START_REF] Alur | A theory of timed automata[END_REF] to model dense-time systems and study the opacity problem in this setting.

Related Work. Formalizing security policies is an important issue and has been investigated a lot in the recent years. In these frameworks, a finite or discrete state model of the system is known, and the security policy is specified as a property of this model: see [START_REF] Rushby | Noninterference, Transitivity and Channel-Control Security Policies[END_REF][START_REF] Focardi | Classification of security properties (part I: Information flow)[END_REF] for non-interference and [START_REF] Mazaré | Using unification for opacity properties[END_REF][START_REF] Bryans | Opacity generalised to transition systems[END_REF] for opacity.

Taking into account timing aspects in the model has been investigated for (strong non-deterministic) non-interference (SNNI) in [START_REF] Gardey | Non-interference control synthesis for security timed automata[END_REF][START_REF] Benattar | Synthesis of Non-Interferent Timed Systems[END_REF] where it is shown that checking SNNI is decidable for deterministic timed automata. To our knowledge, the opacity problem for timed systems has not been studied and this is the contribution of this paper.

We show that, although it is important to take into account in the model of the system the capability of an attacker to measure time, the problem of checking whether such a model is opaque is undecidable for a very restricted class of timed systems (Event Recording Automata). This leaves no hope for an algorithmic solution to this problem.

Organisation of the Paper. Section 2 recalls the basics of timed languages and timed automata. Section 3 contains a formal definition of the opacity problem for dense-time systems. Section 4 is the main part of the paper and we prove that opacity is undecidable for timed automata. Finally, Section 5 gives a summary of the contribution of the paper.

Preliminaries

Notations

In the sequel Σ is a finite alphabet. We let τ be the unobservable action, and let Σ τ = Σ ∪ {τ }. R is the set of real numbers and R ≥0 is the set of nonnegative reals numbers. N the set of natural numbers, Z the set of integers and B = {true, false} is the set of boolean values.

Let X be a finite set of clocks. We let C(X) be the set of convex constraints on X, i.e., the set of conjunctions of constraints of the form x ⊲⊳ c with c ∈ Z and ⊲⊳∈ {≤, <, =, >, ≥}. A clock valuation is a mapping v : X → R ≥0 . We let R X ≥0 be the set of clock valuations over X. We let 0 X be the zero valuation where all the clocks in X are set to 0 (we use 0 when X is clear from the context). Given

δ ∈ R, we let v + δ denote the valuation (v + δ)(x) = v(x) + δ. Given a constraint g ∈ C(X) and a valuation v, we write v |= g if g is satisfied by the valuation v. Given a set R ⊆ X and a valuation v of the clocks in X, v[R] is the valuation v[R](x) = v(x) if x ∈ R and v[R](x) = 0 otherwise.
The set of finite words over an alphabet Σ is Σ * which contains the empty word ε.

If w = a 1 • • • a n , |w| = n
is the length of w, and we write w[i], 1 ≤ i ≤ |w| to denote the ith letter a i of w. A language L is any subset of Σ * . A finite timed word over Σ is a word in (Σ × R ≥0 ) * i.e., over the (infinite) alphabet Σ × R ≥0 . Thus a timed word is a pair w = (σ, t) with σ ∈ Σ * , t ∈ R * ≥0 with |σ| = |t| and with the convention that event σ[i] occurs at global time t[i]. Hence we require the t[i]'s to form an increasing sequence.

TW * (Σ) is the set of finite timed words over Σ and again ε is the empty timed word. A timed language is any subset of TW * (Σ). Given a timed language K, we let

Unt(K) = {σ ∈ Σ * | ∃t ∈ (R ≥0 ) * : (σ, t) ∈ K}. Given Σ ′ ⊆ Σ, the projection of (σ 1 , t 1 )(σ 2 , t 2 ) • • • (σ n , t n ) is the timed word that comprises of the letters σ i ∈ Σ ′ . For example π {a,b} ((a, 1)(c, 2.34)(τ, 2.986)(b, 3.146)(c, 4.16)) is (a, 1)(b, 3.146). π Σ ′ (K) = {π Σ ′ (w) | w ∈ K}. Let K ⊆ (Σ ′ ) * . The inverse projection π -1 Σ (K) is defined by: π -1 Σ (K) = {w ∈ TW * (Σ) | π Σ ′ (w) ∈ K}.

Timed Automata

Timed Automata (TA) were introduced in [START_REF] Alur | Automata for modeling real-time systems[END_REF] to model real-time systems using dense-time. The fundamental results about timed automata can be found in [START_REF] Alur | A theory of timed automata[END_REF].

Definition 1 (Timed Automaton). A Timed Automaton A is a tuple (L, l 0 , X, Σ τ , E, F ) where:

-L is a finite set of locations; -l 0 is the initial location; -X is a finite set of clocks; -Σ is a finite set of actions;

-E ⊆ L × C(X) × Σ τ × 2 X
× L is a finite set of edges; in an edge (ℓ, g, a, r, ℓ ′ ), g is the guard, and r the reset set; -F ⊆ L is the set of final locations.

A state of A is a pair (ℓ, v) ∈ L × R X ≥0 . A run ̺ of A from (ℓ 0 , v 0 ) is a sequence of the form: ̺ = (ℓ 0 , v 0 ) δ0 -→ (ℓ 0 , v 0 + δ 0 ) a0 -→ (ℓ 1 , v 1 ) • • • • • • an-1 ---→ (ℓ n , v n ) δn -→ (ℓ n , v n + δ n ) s.t. for every i ≥ 0 there is some edge (ℓ i , g i , a i , r i , ℓ i+1 ) ∈ E and: (i) v i + δ i |= g i , (ii) v i+1 = (v i + δ i )[r i ].
The set of finite runs from s = (ℓ, v) is denoted Runs(s, A) and we let Runs(A) = Runs((l 0 , 0), A). We let last(̺) = (ℓ n , v n + δ n ). The trace, tr(̺), of the finite run ̺ the timed word (σ

1 , t 1 )(σ 2 , t 2 ) • • • (σ n , t n ) with σ i = a i-1 , 1 ≤ i ≤ n and t i = i-1 k=0 δ k , 1 ≤ i ≤ n. For V ⊆ Runs(A), we let Tr(V ) = {tr(̺) | ̺ ∈ V },
which is the set of traces of the runs in V . Let Tr(A) = Tr(Runs(A)) be the set of traces generated by A (note that this language is prefix-closed).

A finite timed word w is accepted by A if it is the trace of a run ̺ of A that ends in an F -location i.e., last(̺) ∈ F × R X ≥0 . L(A) is the set of traces of finite timed words accepted by A. timed automaton with one clock x. It indicates that an "a" or a "c" can occur at time 0 and be followed either by a "b" at time 1 or a "b" at time 2. In this example we do not use strict constraints like 1 < x < 2. Thus automaton B can generate the following runs:

(0, x = 0) a --→ (1, x = 0) 1 -→ (1, x = 1) b --→ (2, x = 1) δ --→ (2, x = 1 + δ) or (0, x = 0) c --→ (3, x = 0) 2 -→ (3, x = 2) b --→ (4, x = 2) δ --→ (4, x = 2 + δ)
with δ ≥ 0. The set of timed words generated by automaton B consists of two timed words and L(B) = Tr(B) = {(a, 0)(b, 1), (c, 0)(b, 2)}. ♦

A τ -edge in a timed automaton is an edge (ℓ, g, a, r, ℓ ′ ) with a = τ . A timed automaton (L, l 0 , X, Σ τ , E, F ) is deterministic if: (i) it does not contain any τedge and (ii) whenever two edges (ℓ, g 1 , a, r 1 , ℓ 1 ) and (ℓ, g 1 , a, r 2 , ℓ 2 ) are in E, then g 1 ∧ g 2 is equivalent to false. A is an Event Recording Automaton if: it is deterministic1 and (iii) each clock x a ∈ X is paired with an event a ∈ Σ, and (iv) if (ℓ, g, a, r, ℓ ′ ) ∈ E, then r = {x a }.

We use the following classes of TA in the sequel:

the most general class [START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF] of TA with τ -edges given by Definition 1 is denoted τ NTA; -NTA is the sub-class of τ NTA which consists of non-deterministic TA with no τ -edges; -DTA is the sub-class of NTA which consists of deterministic TA; -ERA is the sub-class of DTA which consists of Event Recording Automata (ERA, see [START_REF] Alur | Event clock automata: A determinizable class of timed automata[END_REF]); ERA are TA where each clock is associated with an event and when this event occurs the corresponding clock is reset.

These classes of TA can be ordered according to the class of timed languages they accept. A class C is more expressive than C ′ if every timed language accepted by a TA of C ′ can be accepted by a TA of C. This defines a pre-order C ′ ⊑ C (reads "C is more expressive than C ′ ") on classes of TA. The expressive power of the different classes is strictly increasing in the following order (see [START_REF] Alur | Event clock automata: A determinizable class of timed automata[END_REF][START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF]):

ERA ⊏ DTA ⊏ NTA ⊏ τ NTA (1)
One of the key result in the seminal paper of Alur and Dill [START_REF] Alur | A theory of timed automata[END_REF] is that the universality problem for NTA, i.e., checking whether a NTA A accepts all timed words, is undecidable (notice that it is decidable for DTA [START_REF] Alur | A theory of timed automata[END_REF]).

Product of Timed Automata

In the sequel we need to use the product of two TA to reduce the opacity problem to the L-opacity problem (section 4.2).

Definition 2 (Product of TA). Let A i = (L i , l i 0 , X i , Σ i τ , E i , F i ), i ∈ {1, 2}, be two TA such that X 1 ∩ X 2 = ∅. The product of A 1 and A 2 is the timed automaton A 1 × A 2 = (L, l 0 , X, Σ τ , E, F ) given by:

-L = L 1 × L 2 , -l 0 = (l 1 0 , l 2 0 ), -Σ = Σ 1 ∪ Σ 2 , -X = X 1 ∪ X 2 , -E ⊆ L × C(X) × Σ × 2 X × L and ((ℓ 1 , ℓ 2 ), g 1,2 , σ, r, (ℓ ′ 1 , ℓ ′ 2 )) ∈ E if: • either σ ∈ Σ 1 ∩ Σ 2 , and (i) (ℓ k , g k , σ, r k , ℓ ′ k ) ∈ E k for k = 1 and k = 2; (ii) g 1,2 = g 1 ∧ g 2 and (iii) r = r 1 ∪ r 2 ; • or for k = 1 or k = 2, σ ∈ (Σ k \ Σ 3-k ) ∪ {τ }, and (i) (ℓ k , g k , σ, r k , ℓ ′ k ) ∈ E k ; (ii) g 1,2 = g k et (iii) r = r k ; -F = F 1 × F 2 .
A 1 and A 2 have no clocks in common, ans it is a well-known fact that:

Lemma 1. L(A 1 × A 2 ) = L(A 1 ) ∩ L(A 2 ).
Thus given two automata A 1 and A 2 that have no clocks in common, it is possible to construct the product A 1 × A 2 which accepts exactly the intersection of the two timed languages L(A 1 ) ∩ L(A 2 ).

Timed Opacity

In this section we give a formal definition of opacity for timed automata along with a small example.

Assume we are given a timed automaton (L, l 0 , X, Σ τ , E, F ) and a secret S ⊆ TW * (Σ). Let Σ o ⊆ Σ be a set of observable events. Opacity is a property which ensures that, if the system generates a timed word w, and an external observer, the attacker, can only see π Σo (w), he can never infer whether the original timed word w generated by A is in S or not. Let π be the projection over The timed automaton in Figure 2, page 4, generates the timed language L(B) = {(a, 0)(b, 1), (c, 0)(b, 2)}. Notice also that Unt(L(B)) = L(A). Define the secret by the timed language S ′ = {(a, t 1 )(b, t 2 )}, 0 ≤ t 1 ≤ t 2 . Assume now that an attacker can measure time with his own clock but can only observe Σ o = {b}. Then S ′ is not opaque any more w.r.t. B and Σ o : indeed, if the attacker sees "b" at time 1 he knows an "a" has occurred. Thus there is a timed word w = (a, 0)(b, 1) ∈ Tr(B) s.t. π Σo (w) = (b, 1) ∈ π Σo (Tr(B)) and

π -1
Σo ((b, 1)) = {w} ⊆ S ′ which contradicts the requirement of Definition 3. ♦

In this sense timed opacity is an interesting generalisation of opacity as it takes into account the time-measuring capabilities of an external attacker which gives him additional observational power. Nevertheless, from an algorithmic viewpoint, timed opacity is hopeless as we will show in the next section.

Checking Timed Opacity

In this section we will prove that the simplest versions of the timed opacity problem are undecidable for timed automata.

We first define a version of timed opacity where the secret is a set of states an automaton can be in. Let A = (L, l 0 , X, Σ τ , E, F ) be a timed automaton where F is a set of secret locations. Let Σ o ⊆ Σ and π be the associated projection. Given a word w ∈ TW * (Σ), we let last(w) = {last(̺) |̺ ∈ Runs(A)∧tr(̺) = w}; last(w) is the set of states A can be in after reading the timed word w. This extends trivially to sets of traces.

Checking Location-Based Opacity

We can now define a location-based version of timed opacity: Let A = (L, l 0 , X, Σ τ , E, F ) be a timed automaton with secret locations F . A first negative result is easy to prove for L-opacity: Theorem 1. The L-opacity problem is undecidable for NTA.

Proof. We reduce the universality problem for NTA, which is known to be undecidable [START_REF] Alur | A theory of timed automata[END_REF], to the L-opacity problem for NTA.

Let A = (L, l 0 , X, Σ, E, F ) be a non-deterministic TA, with accepting locations F . The universality problem consists in deciding whether L(A) = TW * (Σ).

First thing we do is to complete by adding edges from each location, with guard true, and fresh target location Bad which is not in F . Then we can assume that Tr(A) = TW * (Σ). Note that it does not change L(A) as Bad is not accepting. L(A) is universal is equivalent to:

∀w ∈ TW * (Σ), last(w) ⊆ L \ F (2)
Let Σ o = Σ. L \ F is L-opaque w.r.t. A and Σ amounts to:

∀w ∈ π(Tr(A)), last([w]) ⊆ L \ F (3)
but as π(Tr(A)) = Tr(A) = TW * (Σ) and [w] = w (no τ -edges), equation ( 2) is equivalent to equation (3). As universality is undecidable for NTA, the result follows.

⊓ ⊔

Because τ NTA includes NTA, it follows that the L-opacity problem is also undecidable for τ NTA. To prove the previous result we did not need to take any particular strict subset of Σ. It turns out that, using this possibility to make the observable alphabet vary, we can prove that the L-opacity problem is also undecidable for DTA.

Theorem 2. The L-opacity problem is undecidable for DTA.

Proof. Let A = (L, l 0 , X, Σ τ , E, F ) be a τ NTA. We show that F is L-opaque w.r. We now restrict our attention to ERA. It turns out that the L-opacity problem is also undecidable for ERA:

Theorem 3. The L-opacity problem is undecidable for ERA.

Proof. We reduce the L-opacity problem for DTA to an opacity problem on ERA. Let A = (L, l 0 , X, Σ, E, F ) be a DTA. We let Σ(X) = {r x , x ∈ X} be a set of actions corresponding to each clock x in X. Also we define X a = {x a , a ∈ Σ} to be a new set of clocks associated with actions in Σ.

Let (ℓ, g, a, R, ℓ ′ ) be an edge from E with R = {x 1 , • • • , x k }. Consider the sequence of edges given in Figure 3. In this sequence, we reset the first clock (x a does not appear in any guard of A) x a and then use it to enforce the reset of the clocks in R within 0 time units. The set R i is given by {x i , • • • , x k }. The sequence of transition given on Figure 3 fires only if g is satisfied (and the new clocks in X a are not constraining g) and then resets the clocks in R without any elapsing. Thus when ℓ ′ is reached, the values of the clocks in X have the same values as the ones they would have if firing (ℓ, g, a, R, ℓ ′ ).

For an edge e ∈ E, denote κ(e) the associated set of edges as given in Figure 3.

Let A ′ = (L ∪ L ′ , l 0 , X ∪ X a , Σ ∪ Σ(X), E ′ , F ) be the TA with L ′ = L × 2 X and E ′ comprises of all the edges κ(e), e ∈ E.
First A ′ is an ERA. Second F is opaque w.r.t. A and Σ if and only if F is opaque w.r.t. A ′ and Σ. This completes the proof.

⊓ ⊔ ℓ (ℓ ′ , R1) (ℓ ′ , R2) (ℓ ′ , R k-1 ) (ℓ ′ , R k ) ℓ ′ (g, a, {xa}) (xa = 0, rx 1 , {x1}) (xa = 0, rx k , {x k-1 }) (xa = 0, rx 1 , {x k }) ℓ ℓ ′ (g, a, R)

Checking Opacity

The initial version of opacity of Definition 3 can be reduced to L-opacity for secret languages S generated by deterministic timed automata, even ERA. This opacity problem has two parameters: the model of the system and the secret language. It follows that:

Theorem 4. The opacity problem is undecidable for systems given by ERA and secrets given by ERA.

Proof. We reduce opacity to L-opacity. Let A = (L, l 0 , X, Σ, E, L) be an ERA and Σ o ⊆ Σ. Assume the secret language S ⊆ L(A) is given by an ERA A S = (L S , l S 0 , X S , Σ, E S , F S ). Define the product A × A S and remind that the final locations are F × F S . Notice that the product of two ERAs is an ERA. By definition of A × A S , and Lemma 1, L(A × A S ) = L(A) ∩ L(A S ) = L(A) ∩ S.

Consequently w ∈ L(A × A S ) if and only if w ∈ Tr(A) ∩ S. Thus last([w]) ⊆ F × F S if and only if [w] ⊆ S. This completes the proof.

⊓ ⊔ Remark 1. In the untimed case, for finite transition system, non-interference can be reduced to an opacity problem [START_REF] Mazaré | Using unification for opacity properties[END_REF]. It should not be difficult to extend the reduction to timed automata. Thus it is not so surprising that opacity is undecidable for NTA because checking non-interference for NTA is undecidable [START_REF] Gardey | Non-interference control synthesis for security timed automata[END_REF].

What is surprising is that this result holds for very restrictive classes of timed automata like ERA, which usually have very nice closure and decidability properties [START_REF] Alur | Event clock automata: A determinizable class of timed automata[END_REF]. ♦

Conclusion

In this paper we have addressed the opacity problem for timed systems. It turns out that the opacity problem is undecidable for the very restrictive class of ERA. Notice that our result carries over to other reasonable models of dense-time systems like Time Petri Nets (TPN), because TPN and τ NTA are equivalent w.r.t. timed language acceptance [START_REF] Cassez | Structural translation from time petri nets to timed automata[END_REF].

Our result is based on the undecidability of universality for NTA operating in dense-time. Considering a time domain like N (not dense) may render the opacity problem tractable.

Fig. 1 .

 1 Fig. 1. The Automaton A

Example 1 . 2 Fig. 2 .

 122 Fig. 2. The Automaton B

  Σ o . Two words w, w ′ ∈ TW * (Σ) are π-equivalent, denoted w ≡ w ′ if π(w) = π(w ′ ). Given w ∈ π(Tr(A)), we let [w] be the set of timed words of A the projection of which is w.Thus [w] = π -1 (w) ∩ Tr(A) i.e.,[w] is the set of timed words generated by A which give the same trace when projected on Σ o . We can define formally what is opacity for timed automata. The relational operator ⊆ is used to denote non inclusion: for two sets A and B, A ⊆ B stands for "A is not included in B". Definition 3 (Opacity). The secret S is opaque w.r.t. A and Σ o ⊆ Σ iff for each w ∈ π(Tr(A)), [w] ⊆ S. The opacity problem is the following: Given a TA A, a secret S and Σ o ⊆ Σ, is S opaque w.r.t. A and Σ o ? Definition 3 defines opacity as a non-inclusion property. If [w] ⊆ S for w ∈ π(Tr(A)), it simply means that the observation w can be produced by at least two timed words w 1 and w 2 in A and at least one of them is not in S. Thus we cannot conclude by observing w that a word of S generated the observation w. Example 2. Assume Σ = {a, b, c} and Σ o = {b}. Let S = {ab} be the secret and A be the finite automaton 2 given in Figure 1 (all locations are accepting) in the introduction. S is opaque w.r.t. the automaton A and Σ o because, if an attacker sees a "b", he cannot infer what the preceding letter was and cannot know the secret ab: π -1 (b) ∩ Tr(A) = {ab, cb} ⊆ S.

Definition 4 (

 4 L-Opacity). F is L-opaque with respect to A and Σ o ⊆ Σ iff for each w ∈ π(Tr(A)), last([w]) ⊆ F . The L-opacity problem asks the following: Given a TA A, a set of secret states F and Σ o ⊆ Σ, is F L-opaque w.r.t. A and Σ o ?

Fig. 3 .

 3 Fig. 3. Widget κ(e) for Encoding DTA L-Opacity into ERA L-Opacity

  t. A and Σ if and only if F is L-opaque w.r.t. A ′ and Σ, where A ′ is a DTA. Assume the only non-determinism in A is on the τ -edges, i.e., A is deterministic for all the other actions in Σ. Then A has a finite number, say n, of τ -edges. Let {a 1 , a 2 , • • • , a n } be fresh letters not in Σ. Order the τ -edges and replace the τ action in τ -edge k by a k . This gives a DTA A ′ on the alphabetΣ ∪ {a 1 , • • • , a n }.It is easy to see that F is L-opaque w.r.t. A and Σ if and only if F is L-opaque w.r.t. A ′ and Σ.⊓ ⊔

In their original paper[START_REF] Alur | Event clock automata: A determinizable class of timed automata[END_REF], Alur et al. do not require that ERA be deterministic. Considering deterministic ERA is not a restriction since (non-deterministic ERA) are determinizable[START_REF] Alur | Event clock automata: A determinizable class of timed automata[END_REF].

A finite automaton is a timed automaton with no clocks.

Acknowledgements. The author would like to thank J. Dubreil and H. Marchand for introducing the opacity problem to him.

⋆ Author supported by a Marie Curie International Outgoing Fellowship within the 7th European Community Framework Programme.