François Laroussinie

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

Ghassan Oreiby
email: oreiby@lsv.ens-cachan.fr

Model Checking Timed ATL for Durational Concurrent Game Structures

HAL is

Introduction

Verification and model-checking. The development of embedded reactive systems is impressive (both in terms of their number and of their complexity), and their formal verification can't be ignored. Model-checking [START_REF] Clarke | Model Checking[END_REF][START_REF] Bérard | Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools[END_REF] is a well-established technique for verifying that (an automaton representing) such a system satisfies a given property. Following [START_REF] Pnueli | The temporal logic of programs[END_REF][START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF], temporal logics have been used for specifying those properties: Linear time temporal logics (e.g. LTL) expresses properties on each single execution of the model, while branching time temporal logics (e.g. CTL) deal with the computation tree of the model.

The model-checking technique has been extended to also handle quantitative measurement of time. In that framework, automata are equipped with realvalued clocks [START_REF] Alur | A theory of timed automata[END_REF], and temporal logics are extended to also express quantitative constraints on the flow of time [START_REF] Alur | Model-checking in dense real-time[END_REF]. Again, this framework is now well understood, but the algorithms are noticeably more complex.

In order to lower the complexity of those algorithms, less expressive models and logics have been developed [START_REF] Emerson | Quantitative temporal reasoning[END_REF][START_REF] Campos | Real-time symbolic model checking for discrete time models[END_REF][START_REF] Laroussinie | Efficient timed model checking for discrete-time systems[END_REF]. Those models are less expressive, but can be handled very efficiently, especially through symbolic model-checking algorithms using BDD techniques [START_REF] Bryant | Symbolic boolean manipulation with ordered binary-decision diagrams[END_REF][START_REF] Mcmillan | Symbolic Model Checking: An Approach to the State Explosion Problem[END_REF][START_REF] Campos | Real-time symbolic model checking for discrete time models[END_REF][START_REF] Markey | Symbolic model checking of simply-timed systems[END_REF].

Verification and control. In the late 80's, a new framework has been developed in the field of verification: control (and controller synthesis) [START_REF] Ramadge | The control of discrete event systems[END_REF]. The goal is now to build a controller that should prevent the (model of the) system from having unwanted behaviors.

This problem is closely related to (multi-player) games: solving such a game amounts to compute a strategy (if it exists) for a player so that he surely reaches a state where he is declared the winner. In that case, the underlying model is not a simple automaton, but rather a "concurrent game structure" (CGSs) [START_REF] Alur | Alternating-time temporal logic[END_REF], in which several agents concurrently decide on the behavior of the system. In order to reason with strategies, a new flavor of temporal logics has been defined: alternating time temporal logics (ATL) [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF]. This logic allows to express, for instance, that a coalition of agents has a strategy in order to always reach a winning location, or to always avoid reaching a bad locations. When the concurrent game structure is defined explicitly, ATL enjoys polynomial-time model-checking algorithms.

Our contribution. The goal of this paper is to extend the framework of ATL to (simply) timed systems. To that aim, we introduce durational CGSs (DCGSs), in which each transition is labeled with an interval of possible (integer) durations. Those durations are assumed to be atomic, i.e., there are no intermediate state, and the complete duration elapses in one step.

We propose a semantics for DCGSs where we assume that each transition is associated with an extra agent, who is in charge of selecting the duration of that transition within the interval it is labeled with. We believe that this semantics is really interesting, as it allows to finely select which durations can be controlled by a coalition. Moreover, we show that it still enjoys polynomial-time quantitative model-checking algorithms in the case when no equality constraint is involved.

Related work. Our discrete-time extension of CGSs to DCGSs is inspired by that of [START_REF] Laroussinie | Efficient timed model checking for discrete-time systems[END_REF], where efficient quantitative model-checking algorithms are proposed. Several other extensions of games with time have been proposed in the recent literature, e.g. [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF][START_REF] Alur | Modularity for timed and hybrid systems[END_REF][START_REF] Asarin | Controller synthesis for timed automata[END_REF][START_REF] Cassez | Efficient on-thefly algorithms for the analysis of timed games[END_REF]. The semantics assumed there uses dense-time where players choose either to wait for a delay or to fire an action-transition. In [START_REF] De Alfaro | The element of surprise in timed games[END_REF], another dense-time semantics is proposed, working (roughly) as follows: each player chooses a (strictly positive) delay and a transition, and the game follows the player with the shortest delay. With this semantics, each player can take the others by surprise.

Those papers only deal with qualitative control objectives. In [START_REF] Schobbens | Real-time concurrent game structures[END_REF], Schobbens proposes a quantitative extension of ATL over timed CGSs (with a semantics of time similar to that of [START_REF] De Alfaro | The element of surprise in timed games[END_REF]). The resulting logic, ARTL * , a mixture of ATL and MITL, is shown decidable.

Definitions

Tight Durational CGS (TDCGS)

We extend the model of CGSs, see [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Laroussinie | Expressiveness and complexity of ATL[END_REF]. Definition 1. A TDCGS is a 6-tuple A = Loc, Agt, AP, Lab, Mv, Edg where:

• Loc is the (finite) set of locations;

• Agt = {a 1 , . . . , a k } is a (finite) set of agents (or players); • AP the set of atomic propositions; • Lab : Loc → 2 AP the labelling function;

• Mv : Loc × Agt → P(N) {∅} gives the set of possible moves at a given location for a given agent;

• Edg : Loc × N k → Loc × N >0
is the transition table, that is a partial function assigning a successor location and a duration for a move of all agents.

The difference with classical CGSs is that each transition of a TDCGS carries a positive1 integer, representing the duration (or cost) of that transition. Given a transition Edg(q, c 1 , . . . , c k ) = (q , t), we use Edg (q, c 1 , . . . , c k ) (resp. Edg τ (q, c 1 , . . . , c k )) to denote the location q (resp. the duration t).

The semantics of a TDCGS is similar to that of classical CGSs: a move of agent a in location q is an integer c such that c ∈ Mv(q, a). Once each agent a i has selected a move c i ∈ Mv(q, a i ), the transition table Edg indicates the transition to be fired, namely Edg(q, c 1 , . . . , c k ). Definition 2. An execution of a TDCGS A = Loc, Agt, AP, Lab, Mv, Edg from a location q 0 ∈ Loc is an infinite sequence ρ = (q 0 , d 0 ) . . . (q i , d i ) . . . such that:

• d 0 = 0;
• for each i, there exists a set of moves c i 1 , . . . , c i k such that (q i+1 , d i+1 -d i ) = Edg(q i , c i 1 , . . . , c i k ). For an execution ρ = (q 0 , d 0 ) . . . (q i , d i ) . . ., the integer d i is the date when arriving in q i . The interesting point with ATL, compared to standard temporal logics, is that it allows quantifications on strategies of (coalitions of) agents. A coalition is a subset of the set of agents. Now we introduce the notions of strategy and outcome: Definition 3. Let A = Loc, Agt, AP, Lab, Mv, Edg be a TDCGS.

• Let a ∈ Agt. A strategy σ a for a is a mapping that associates, with any finite prefix (q 0 , d 0 ) . . . (q i , d i ) of any execution, a possible move for agent a in q i , i.e. σ a ((q 0 , d 0 ) . . . (q i , d i )) ∈ Mv(q i , a). • Let A ⊆ Agt be a coalition. A move for A from a location q is a family (c a ) a∈A : one move for each agent in A. We write Mv(q, A) to represent the set of all possible moves for A from q. Moreover a strategy σ A for A is a family (σ a ) a∈A . We write A for Agt A. Given a move c ∈ Mv(q, A) and c ∈ Mv(q, A), we write Edg(q, c • c) for the transition corresponding to these choices.

• Let A ⊆ Agt be a coalition and σ A be a strategy for A. An execution ρ = (q 0 , d 0 ) . . . (q i , d i ) . . . is an outcome of σ A from q 0 if, for any i, writing c i = σ A ((q 0 , d 0 ) . . . (q i , d i )), there exists c i ∈ Mv(q i , A) s.t.

(q i+1 , d i+1 -d i ) = Edg(q i , c • c).
We denote by Out A (q, σ A ) the set of all outcomes of σ A from q (we omit the superscript A when it is clear from the context).

Size of a TDCGS. The size |A| of A is the sum of the sizes of Loc and Edg. The size of Edg is defined as follows: |Edg| = q∈Loc c∈Mv(q,Agt) (1+ log(Edg τ (q, c) ).

1.2 Timed ATL (TATL) Definition 4. The syntax of TATL is defined by the following grammar:

TATL ϕ s , ψ s ::= | P | ¬ϕ s | ϕ s ∨ ψ s | A ϕ p ϕ p ::= X ϕ s | ϕ s U ∼ζ ψ s | ϕ s R ∼ζ ψ s with P ∈ AP, A ⊆ Agt, ∼ ∈ {<, ≤, =, ≥, >}, and ζ ∈ N.
We also define the usual shorthands, such as

⊥ def ≡ ¬ , A F ∼ζ ϕ s def ≡ A U ∼ζ ϕ s , and A G ∼ζ ϕ s def ≡ A ⊥ R ∼ζ ϕ s .
TATL formulae are interpreted over states of TDCGSs. Intuitively, the stateformula A ϕ p holds in q iff there exists a strategy for coalition A in order to enforce the path-formula ϕ p along all the outcomes. Formally: Definition 5. The following clauses define when a location q (resp. an execution ρ = (q 0 , d 0 )(q 1 , d 1 ) . . .) of a TDCGS A satisfies a TATL formula ϕ s (resp. a path-formula ϕ p ), written q |= A ϕ s (resp. ρ |= A ϕ p ), by induction over the formula (semantics of boolean operators and atomic propositions are omitted):

q |= A A ϕ p ⇔ ∃σ A . ∀ρ ∈ Out(q, σ A ). ρ |= A ϕ p ρ |= A X ϕ s ⇔ q 1 |= A ϕ s ρ |= A ϕ s U ∼ζ ψ s ⇔ ∃i ∈ N. q i |= A ψ s , d i ∼ ζ and q j |= A ϕ s for any 0 ≤ j < i ρ |= A ϕ s R ∼ζ ψ s ⇔ ρ |= A ¬(¬ϕ s U ∼ζ ¬ψ s )
When A is clear from the context, we just write q |= ϕ. Note that, contrary to usual definitions of ATL [START_REF] Alur | Alternating-time temporal logic[END_REF][START_REF] Alur | Alternating-time temporal logic[END_REF], we include the "release" modality R, as we proved in [START_REF] Laroussinie | Expressiveness and complexity of ATL[END_REF] that modality A R cannot be expressed using only A U and A G. Intuitively, ϕ s R ∼ζ ψ s requires that ψ s must hold when the condition "∼ ζ" is fulfilled, but this global requirement is released as soon as ϕ s holds. Formally:

ρ |= A ϕ s R ∼ζ ψ s ⇔ ∀i ∈ N. (d i ∼ ζ ⇒ q i |= A ψ s ) or ∃j < i. q j |= A ϕ s .
We use TATL ≤,≥ to denote the fragment of TATL where subscripts "= ζ" are not allowed in timing constraints for U and R.

The complexity of model-checking an ATL formula over a CGS has been shown to be linear in both the size of the structure and the size of the formula [START_REF] Alur | Alternating-time temporal logic[END_REF]. On the other hand, TCTL model checking on DKSs is PTIME-complete when timing constraints contain no equality, while it is ∆ P 2 -complete otherwise [START_REF] Laroussinie | Efficient timed model checking for discrete-time systems[END_REF]. We present in this section our model-checking algorithm for TATL over TD-CGSs. We explain how to handle modalities U ∼ζ and R ∼ζ . We then gather up those algorithms in a global labeling algorithm, which is PTIME-complete when no equality constraint is involved, and EXPTIME-complete otherwise.

Modalities U ≤ζ and R ≤ζ

First we consider the case of formula A ϕ 1 U ≤ζ ϕ 2 , that is, when the coalition A aims at reaching ϕ 2 within ζ time units (and verifying ϕ 1 in the intermediate states). We assume that states have already been labeled with ϕ 1 and ϕ 2 , which can therefore be seen as atomic propositions. We have: Lemma 6. Let A be a TDCGS, and ϕ = A P 1 U ≤ζ P 2 be a TATL formula (with P 1 , P 2 ∈ AP). Then we can compute in time O(|Loc| • |Edg|) the set of locations of A where ϕ holds.

Proof. For this proof, we define the extra modality U ≤i ≤n , with the following semantics:

ρ |= A P 1 U ≤i
≤n P 2 ⇔ ∃j ≤ i. q j |= A P 1 , d j ≤ n, and q k |= A P 2 for any 0 ≤ k < j

This modality requires that the right-hand side formula be satisfied within at most i steps. It is clear that, for any n ∈ N,

q |= A P 1 U ≤n P 2 ⇔ q |= A P 1 U ≤|Loc| ≤n P 2 . (1)
Indeed, if all the outcomes of a strategy satisfy P 1 U ≤n P 2 , it is possible to adapt that strategy so that each location is visited at most once along each outcome. We now define functions v i (q), for i ∈ N and q ∈ Loc, by the following recursive rules:

if q |= P 2 : v 0 (q) = 0 if q |= ¬P 2 : v 0 (q) = +∞      if q |= P 2 : v i+1 (q) = 0 if q |= ¬P 1 ∧ ¬P 2 : v i+1 (q) = +∞ otherwise : v i+1 (q) = min c∈Mv(q,A) max c∈Mv(q,A) Edg τ (q, c • c) + v i (Edg (q, c • c))
Our proof now amounts to showing the following lemma: Lemma 7. For any i ∈ N, for any n ∈ N and any q ∈ Loc, we have:

n ≥ v i (q) ⇔ q |= A P 1 U ≤i ≤n P 2 .
The proof is by induction on i: The base case is straightforward, as well as the induction step when q |= P 2 and when q |= ¬P 1 ∧ ¬P 2 . We thus only focus on the last case, when q |= P 1 ∧ ¬P 2 : Assume the induction hypothesis holds up to level i. If n ≥ v i+1 (q), then (by definition of v i+1 (q)) there exists a move c ∈ Mv(q, A) such that, for any move c ∈ Mv(q, A), we have

n ≥ Edg τ (q, c • c) + v i (Edg (q, c • c)).
By i.h., for any c ∈ Mv(q, A), we have

Edg (q, c • c) |= A P 1 U ≤i ≤n-Edg τ (q,c•c) P 2 .
The strategy σ A witnessing that property, combined with the move c ∈ Mv(q, A), yields a strategy for enforcing P 1 U ≤i+1 ≤n P 2 from q, as required. The converse implication follows the same lines: given a strategy σ A enforcing P 1 U ≤i+1 ≤n P 2 from q, we let c = σ A (q), and deduce that n satisfies the same inequalities as above.

From Equation (1), it suffices to compute v |Loc| (q), for each q ∈ Loc, to deduce the set of locations where ϕ holds. This algorithm thus runs in time

O(|Loc| • |Edg|).
The release modality is handled similarly: we define v i (q) as follows:

if q |= ¬P 2 : v 0 (q) = 0 if q |= P 2 : v 0 (q) = +∞      if q |= ¬P 2 : v i+1 (q) = 0 if q |= P 1 ∧ P 2 : v i+1 (q) = +∞ otherwise : v i+1 (q) = max c∈Mv(q,A) min c∈Mv(q,A) Edg τ (q, c • c) + v i (Edg (q, c • c))
and R ≤i ≤n as the dual of U ≤i ≤n . Then an equivalence similar to Equation (1) holds, and we have the following lemma (proof omitted): Lemma 8. For any i ∈ N, for any n ∈ N and any q ∈ Loc, we have:

n < v i (q) ⇔ q |= A P 1 R ≤i ≤n P 2 . Example 1.
Consider the example depicted on Figure 1. On that TDCGS, the duration is the integer written in the middle of each transition. The tuples that are written close to the source location indicates the choices of the agents for firing that transition (for instance, 2, 1 means that player a 1 chooses move 2 and player a 2 chooses move 1). They are omitted when each agent has a single choice.

The valuations of atomic propositions are given in the table on the right of the figure. This table shows the computation of v i (q), for each location. This computation converges in three steps. For instance, that v

3 (A) = 21 indicates that A |= a 1 P 1 U ≤21 P 2 holds, but A |= a 1 P 1 U ≤20 P 2 . A B C D E 1 1 1 1,1 10 1 1,2 1 2,1 1 2,2

Modalities U ≥ζ and R ≥ζ

We now consider formula A ϕ 1 U ≥ζ ϕ 2 expressing that coalition A has a strategy for staying at least ζ time units in ϕ 1 -states before reaching ϕ 2 . We have:

Lemma 9.
Let A be a TDCGS, and ϕ = A P 1 U ≥ζ P 2 be a TATL formula (with P 1 , P 2 ∈ AP). Then we can compute in time O(|Loc| • |Edg|) the set of locations of A where ϕ holds.

Proof. The idea is similar to that of the proof of Lemma 6. We introduce the following modality:

ρ |= A p U ≥i q ⇔ ∃j ≥ i. q j |= A q
and q k |= A p for any 0 ≤ k < j

We then compute a sequence of values, defined by the following recursive rules:

   if q |= ¬ A P 1 U P 2 : v 0 (q) = -∞ if q |= A P 1 U P 2 ∧ ¬ A P 1 U ≥1 P 2 : v 0 (q) = 0 if q |= A P 1 U ≥1 P 2 : v 0 (q) = +∞          if q |= ¬ A P 1 U P 2 : v i+1 (q) = -∞ if q |= A P 1 U P 2 ∧ ¬ A P 1 U ≥1 P 2 : v i+1 (q) = 0 if q |= A P 1 U ≥1 P 2 : v i+1 (q) = max c∈Mv(q,A) min c∈Mv(q,A) Edg τ (q, c • c) + v i (Edg (q, c • c))
This computation requires that we first compute the set of locations satisfying A P 1 U P 2 and those satisfying A P 1 U ≥1 P 2 . This can be done in time O(|Edg|) using standard ATL model-checking algorithms. Thus, computing v i (q) for each q ∈ Loc and each i ≤ |Loc| can be achieved in time O(|Loc| • |Edg|).

Those values satisfy the following lemma: Lemma 10. For any i ∈ N, for any n ∈ N and q ∈ Loc, we have

n ≤ v i (q) ⇔ q |= A (P 1 U ≥n P 2 ) ∨ (P 1 U ≥i+1 P 2 ) .
This will conclude the proof of Lemma 9, thanks to the following equivalence:

q |= A P 1 U ≥n P 2 ⇔ q |= A (P 1 U ≥n P 2 ) ∨ (P 1 U ≥|Loc|+1 P 2 ) .
This equivalence relies on the fact that all durations are strictly positive: if some outcome of the strategy satisfies P 1 U ≥|Loc|+1 P 2 , then one location is visited twice, and it is possible to adapt the strategy so that it is visited n times (thus with total duration larger than n) before visiting P 2 .

We now prove Lemma 10: we omit the easy cases, and only focus on the inductive step in the case when q |= A P 1 U ≥1 P 2 . In particular, we have q |= P 1 . First, pick some n ≤ v i+1 (q), assuming the result holds up to step i. By definition of v i+1 (q), there exists c ∈ Mv(q, A) such that, for any c ∈ Mv(q, A),

we have n ≤ Edg τ (q, c • c) + v i (Edg (q, c • c)).
From the induction hypothesis, this means that

Edg (q, c • c) |= A (P 1 U ≥n-Edg τ (q,c•c) P 2 ) ∨ (P 1 U ≥i+1 P 2 ) .
The strategy witnessing that property, combined with move c ∈ Mv(q, A), yields a strategy witnessing that

q |= A (P 1 U ≥n P 2 ) ∨ (P 1 U ≥i+2 P 2 ) .
The converse implication follows the same (reversed) steps.

We omit the case of the release modality, which is very similar.

Example 2. In Figure 2, we apply that algorithm to the same TDCGS as before. This table shows the computation of v i (q), for each location. This com- putation converges in three steps. For instance, that

A B C D E 1 1 1 1,1 10 1 1,2 1 2,1 1 2,2 1 1,1 20 1,2 vi(q) 0 1 2 3 A (P1, ¬P2) +∞ +∞ 2 2 B (P1, P2) +∞ 10 10 10
C (P1, ¬P2) +∞ 1 1 1 D (¬P1, P2) 0 0 0 0 E (P1, ¬P2) -∞ -∞ -∞ -∞
v 3 (A) = 2 indicates that A |= a 1 P 1 U ≥2 P 2 holds, but A |= a 1 P 1 U ≥3 P 2 .

Modalities U =ζ and R =ζ

Lemma 11. Let A be a TDCGS, and ϕ = A P 1 U =ζ P 2 be a TATL formula. We can compute in time O(ζ • |Edg|) the set of locations of A where ϕ holds.

Since ζ is encoded in binary, this algorithm runs in time exponential in the size of the formula.

Proof. We use dynamical programming, and recursively build a table T : Loc × {0, . . . , ζ} → { , ⊥} such that

T (q, i) = ⇔ q |= A A ϕ 1 U =i ϕ 2 . (2)
When i = 0, letting T (q, 0) = if, and only if, q |= P 2 clearly fulfills equation ( 2) (since all durations are non-zero). Now, pick i < ζ, and assume all the T (q, j) have been computed for j ≤ i. Then T (q, i + 1) = ⇔ q |= P 1 and ∃c ∈ Mv(q, A). ∀c ∈ Mv(q, A).

Edg(q, c • c) = (q , t) with T (q , i -t) = .
This computation can be done since all durations are non-zero. It is achieved by running through the transition table, and is thus in time linear in the size of Edg. It is clear that equation ( 2) is preserved by this construction, so that in the end, q |= ϕ iff T (q, ζ) = . This algorithm runs in time O(ζ × |Edg|).

A similar algorithm can be defined for handling A ϕ 1 R =ζ ϕ 2 : the table T (q, i) is initialized in the same way (i.e., T (q, 0) = ⇔ q |= P 2 ), and each step is computed according to the following rule:

T (q, i) = ⇔ q |= P 1 ∨ ∃c ∈ Mv(q, A). ∀c ∈ Mv(q, A). Edg(q, c • c) = (q , t) with T (q , i -t) = .

2.4 Results for TATL and TATL ≤,≥

From Lemmas 6, 9 and 11, we can deduce procedures to handle all modalities and this gives the following result: Note that this algorithm is polynomial in the size of the TDCGS, and is exponential only because of the binary encoding of the constants that appear in the formula. This complexity blow-up cannot be avoided: Theorem 13. Model-checking TATL over TDCGSs is EXPTIME-complete.

Proof. This result is based on the fact that deciding the countdown games is EXPTIME-hard [START_REF] Jurdziński | Countdown games[END_REF]. A countdown game is a two-player game. It consists of a weighted graph (V, E) where V is the set of vertices and E ⊆ V × N × V is the weighted transition relation. A configuration of a countdown game (V, E) is a pair (v, C) ∈ V × N. At every turn, Player 1 chooses, from the current configuration (v, C), a duration 1 ≤ d ≤ C s.t. (1) 0 < d ≤ C and (2) there exist at least one transition (v, d, v ) ∈ E. Then Player 2 chooses one of these transitions (issued from v and whose duration is d) and then the new configuration is (v , C -d). Any configuration (v, 0) is terminal and it is a winning configuration for Player 1. Any configuration (v, C) s.t. (1) C > 0 and (2) there is no transition (v, d, -) with d ≤ C is terminal and it is a winning configuration for Player 2. Deciding whether Player 1 has a wining strategy for a configuration (v, C) is an EXPTIME-hard problem [START_REF] Jurdziński | Countdown games[END_REF].

We can easily build a TDCGS A = Loc, Agt, AP, Lab, Mv, Edg corresponding to the countdown game (V, E). We let Agt = {a 1 , a 2 }. The set of locations Loc ⊆ V ∪ V × N is defined as follows: v ∈ Loc if v ∈ V , and (v, t) ∈ Loc if there exists a transition (v, t, -) in E. This is a turn-based game: agent a 1 plays (i.e., has several possible moves) in locations v, and agent a 2 plays in locations (v, t). From v, the moves of agent a 1 are the weights t s.t. there exist some transitions (v, t, -) in E, and the moves of agent a 2 from (v, t) are the possible successors v s.t. (v, t, v ) ∈ E. The transition table is defined in a natural way and the duration associated with transitions leading from v to (v, t) or from (v, t) to v is t. Then deciding whether the configuration (v, C) with C ∈ N is winning for Player 1 reduces to a model checking problem: v |= A a 1 F =2C .

Still, we can have efficient algorithm if we restrict to the fragment TATL ≤,≥ : Theorem 14. Model-checking a TATL ≤,≥ formula ϕ over a TDCGS A can be achieved in time O(|A| 2 • |ϕ|), and is thus in PTIME. This is an immediate consequence of Lemmas 6 and 9. PTIME-hardness follows from that of CTL model-checking over Kripke structures. Thus: Corollary 15. Model checking TATL ≤,≥ over TDCGSs is PTIME-complete.

Unitary TDCGSs

Unitary TDCGSs are TDCGSs where all durations equal 1. Intuitively, unitary TDCGSs are easier to handle because it is possible to verify ϕ = A ϕ 1 U =c ϕ 2 by dichotomy, i.e., by verifying A ϕ 1 U = c/2 ( A ϕ 1 U =c-c/2 ϕ 2 ), and so on [START_REF] Emerson | Quantitative temporal reasoning[END_REF]. That way, model-checking an U =ζ formula can be achieved in time O(log(ζ) • |A|). In the end: Theorem 16. Model checking a TATL formula ϕ over a unitary TDCGS A can be achieved in time O(|A| 2 • |ϕ|), and is thus PTIME-complete.

Model checking TATL

For full TATL, we also reduce the problem to that of finite TDCGSs.

Conclusion

We have introduced a new family of models of concurrent game structures, in which transitions carry a (set of) durations. The semantics of those models involve "time-agents", i.e., agents that decide the duration of the transition that will be fired. This allows to break the symmetry in time games, allowing some coalition to decide the duration of some of the transitions.

We proved that those models enjoy efficient quantitative model-checking algorithms, as soon as no timing constraint = ζ is involved. Equality constraints yield an exponential blow-up, which we saw cannot be avoided.

As future work, we plan to extend this "time agent"-semantics to concurrent game structures with clocks, similar to timed automata [START_REF] Alur | A theory of timed automata[END_REF]. As a first step, it would be nice if we could extend the algorithms presented here to the "continuous" semantics (as defined in [START_REF] Laroussinie | Efficient timed model checking for discrete-time systems[END_REF]) of DCGSs.

Fig. 1 .

 1 Fig. 1. The algorithm for U ≤ζ .

Fig. 2 .

 2 Fig. 2. The algorithm for U ≥ζ .

Theorem 12 .

 12 Model checking a TATL formula ϕ over a TDCGS A can be achieved in time O(|A| 2 • |ϕ| • ζ max ), where ζ max is the maximal constant appearing in ϕ. It is thus in EXPTIME.

  Given a DCGS S and a formula ϕ = A P 1 U =ζ P 2 , we explicitly add one extra agent per transition, with moves in [a, b] if the corresponding transition is labeled with [a, b], and moves in [a, max(a, ζ + 1)] if it is labeled with [a, +∞). This restriction makes the corresponding TDCGS to be finite, its size is inO(|S| • max(b M , ζ)) where b M is the maximal integer appearing as a bound of an interval in S. And applying the algorithm of Theorem 12 to that TDCGS, we get an EXPTIME algorithm for model-checking ϕ on our DCGS S. The algorithm is similar for the release modality. This must be repeated a polynomial number of times for verifying a TATL formula, yielding an algorithm in timeO(|S| 2 • b M • ζ max • |ϕ|) (where ζ max is the largest constant in the formula ϕ), that is, in time exponential in both the structure and the formula. Note that the blow-up is only due to the binary notation for the integers. Combined to Theorem 13, this gives: Theorem 21. Model-checking TATL over DCGSs is EXPTIME-complete.

This work is partly supported by ACI Sécurité & Informatique CORTOS, a program of the French ministry of research. This author is supported by a PhD grant from Région Ile-de-France.

We require in this paper that the durations be non-zero. The case of zero-durations makes some of our algorithms slightly more difficult, and will be handled in a long version of this paper.

i.e. (qi+1, ti+1 -ti) = Edg (qi, c a i • c t i ) with c a i • c t i ∈ Mv(qi, Agt ).

We now propose an extension of the models above that now allows transitions labeled with intervals (instead of a single integer). That way, agents don't know in advance the duration of the transitions. Special agents, one per transition, decide for the durations. This gives a very expressive framework, in which coalitions can mix "classical" agents with "time" agents.

Definition

We write I for the set of intervals with bounds in N >0 ∪ {+∞}. Definition 17. A durational CGS (DCGS) is a 6-tuple S = Loc, Agt, AP, Lab, Mv, Edg such that:

• Loc, Agt, AP, Lab and Mv have the same characteristics as in Definition 1;

• Edg : Loc × N k → Loc × I is the transition table, associating with each transition an interval containing its possible durations.

The size of the transition table is again the space needed to write it in binary notation, and the size of a DCGS is |Loc| + |Edg|. Again, we use Edg τ (q, c) to denote the interval of durations of the transition Edg(q, c), and Edg (q, c) to denote its location.

While the syntax is not very different to that of TDCGSs, the semantics is rather more involved: the crucial point is that the agents must select the transition the system will fire, but they must also choose the duration of that transition within the interval it's labeled with. This last part is achieved by special "time-agents": we consider one time-agent ta q,c per location q and move c in Mv(q, Agt). Formally the semantics of S is defined as a TDCGS A[S] = Loc, Agt , AP, Lab, Mv , Edg with:

• Agt = Agt ∪ {ta q,c | q ∈ Loc and c ∈ Mv(q, Agt)}, • Mv (q, a) = Mv(q, a) for any a ∈ Agt; Mv (q, ta q,c ) = Edg τ (q, c) for any ta q,c ∈ Agt , and Mv (q, ta q ,c ) = {0} for any ta q,c ∈ Agt with q = q, • Edg (q, c, t q0,c0 , . . . , t qn,cm ) = (q , t) iff c ∈ Mv (q, Agt) for any i, t = t q,c and t q,c ∈ Mv (q, ta q,c ), and t q ,c = 0 when q = q or c = c .

As for TDCGSs, we use the notions of coalition of agents (including the time-agents), strategy and outcome.

Note that the transition table of the corresponding TDCGS A[S] is infinite when there exist infinite intervals in the definition of S. And when it is finite, |Edg | is bounded by |Edg| • b M where b M is the maximal constant occurring in the intervals of durations in S: in Edg , we replace each entry (q, c) of Edg by (b -a) + 1 entries when Edg τ (q, c) = [a; b]. Thus the size of A[S] is potentially exponential in |S| (due to the binary encoding). Note that in every entry of Edg , only one time-agent may have more than one possible move.

Moreover time agents can be used in TATL modalities in order to express the existence of strategies for coalitions that may control the duration of a subset

1,1,0 ,3 Fig. 3. A DCGS for the simplified Nim game, and its associated TDCGS.

of transitions. Given a DCGS S, a location q, and a TATL formula ϕ, we write q |= S ϕ when q |= A[S] ϕ. We might omit the subscript if it raises no ambiguity.

Example 3. We illustrate our models by a simple example: the simplified Nim game. In that game, a set of N matches are aligned on a table, and each player, in turn, picks between 1 and 3 matches. The players who takes the last match is declared the winner. This game can easily be encoded as the DCGS (where "durations" are in fact the number of matches taken by the players) depicted on the left of Figure 3. Player A wins iff formula A, t A F =N B holds.

Time agents. The motivation for using time-agents is that the time elapsing should not be controlled by the same player along an execution. Depending on the state or the transition, it is convenient to be able to specify who decides the duration of an event. Note that assigning one time-agent per transition is more general than assigning one time-agent per location: indeed, in the former approach, a time-agent ta q (for controlling the duration of all the transitions issued from q) can be easily simulated by the coalition {ta q,c1 , . . . , ta q,cm } containing all the time-agents of the transitions leaving q.

Model checking TATL ≤,≥

When verifying TATL formulae containing modalities with timing constraints of the form "≤ c" or "≥ c", we do not need to consider all the transitions of A[S].

We can restrict the analysis to an abstraction of A[S]:

Definition 18. Let S = Loc, Agt, AP, Lab, Mv, Edg be a DCGS and let A[S] = Loc, Agt , AP, Lab, Mv , Edg be the TDCGS corresponding to the semantics of S.

Given an integer C, we define the C-abstraction of S as the TDCGS A[S] C = Loc, Agt , AP, Lab, Mv , Edg with:

)); and Mv coincides with Mv for other cases (a ∈ Agt or ta q ,c with q = q). • Edg is defined as Edg but with Mv instead of Mv .

In the TDCGS A[S] C , we replace the set of transitions corresponding to all durations in an interval λ by two transitions: a short one -the left-end value of λ-and a long one: either the right-end value of λ if λ is finite, or C + 1 (or the left-end of λ if C + 1 / ∈ λ). Indeed, an open interval is interesting for the truth value of some properties because it may allow arbitrary long durations. But delaying for C +1 t.u. is always enough when considering TATL ≤,≥ formulae with constants less than C: Lemma 19. Let S be the DCGS and C be an integer. For any ζ ≤ C and q ∈ Loc, we have:

Proof (sketch). There are more behaviors in A[S] than in A[S] C , but these additional executions do not change the truth value of TATL ≤,≥ formulae. Indeed let ρ = (q 0 , d 0 ) . . . (q i , d i ) . . . be an execution in A[S] and let c a i (resp. c t i ) be the i + 1-st move of the agents Agt (resp. the time-agents) along ρ 2 . We can change the move of the agent ta qi,ci and obtain another run ρ with the same prefix and the same suffix as ρ: the duration spent in q i has changed (and thus the global dates of actions) but not the time spent in other locations. This property allows to make local changes on delays without changing the sequence of visited states.

Consider a strategy σ A for the coalition A in A[S] to ensure ψ = P 1 U ≤ζ P 2 . From σ A , we can build a strategy σ A ensuring ψ in A[S] C . Indeed the only changes we have to make are for the moves of time-agents when, in q with a move c for Agt, σ A requires to wait for t q,c while t q,c is not in the restricted set of moves of A[S] C (i.e. t q,c ∈ Mv (q, ta q,c )). In that case, the strategy σ A can propose the minimal duration in Mv (q, ta q,c ): the ending state satisfying ψ will be reached sooner than along ρ and then ψ will be true. If the formula to be verified was U ≥c then the maximal duration will be enough to ensure the formula. The same holds for the release operators. Now consider a strategy σ A for the coalition A in A[S] C to ensure ψ = P 1 U ≤ζ P 2 . This strategy can be completed for ensuring ψ in the full TDCGS. Consider a finite execution ρ in A[S], we can define a corresponding execution ρ in A[S] C where any move of time-agent ta q,c from the location q is either left unchanged if ta q,c ∈ A -this is an "A-controllable" time-agent and having applied σ A from the beginning of the execution ensures that its move is in A[S] C -, or replaced by the maximal duration in Mv (q, ta q,c ) if ta q,c is not an A-controllable time-agent. Then it is sufficient to define σ A (ρ) as σ A (ρ).

Of course, if we consider ψ = P 1 U ≤ζ P 2 , we build ρ differently and consider minimal durations.


Nicolas Markey
email: nmarkey@ulb.ac.be

Jean-François Raskin
email: jraskin@ulb.ac.be

Model Checking Restricted Sets of Timed Paths

Keywords: Timed Automata Undecidable [4] EXPSPACE-c, [3] PSPACE-c, [1] Ult, Per, Zone Paths Undecidable EXPSPACE-c, PSPACE-c, Ult, Per, Region Paths Undecidable EXPSPACE-c, PTIME Finite PSPACE-c

In this paper, we study the complexity of model-checking formulas of three important real-time logics (MTL, MITL, and TCTL) over restricted sets of timed paths. The classes of restricted sets of timed paths that we consider are (i) a single finite (or ultimately periodic) timed path, (ii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) a infinite set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph.

MTL

Introduction

Timed automata have been introduced in [START_REF] Alur | A Theory of Timed Automata[END_REF] as a formal notation to model behaviors of real-time systems. Requirements for real-time systems modeled as timed automata are conveniently expressed using real-time logics. Real-time logics are quantitative extensions of temporal logics. Three main logics have been defined to express real-time requirements: TCTL [START_REF] Alur | Model-Checking in Dense Real-Time[END_REF] is a real-time extension of the CTL logic, while MTL and MITL [START_REF] Alur | The Benefits of Relaxing Punctuality[END_REF] are extensions of the LTL logic. The model checking problems for those logics over sets of timed paths defined by timed automata have been studied. The results are as follows: For the logic TCTL, the model checking problem has been shown PSPACE-complete in [START_REF] Alur | Model-Checking in Dense Real-Time[END_REF]. For the logic MTL, the problem has been shown undecidable in [START_REF] Alur | A Really Temporal Logic[END_REF]. For the logic MITL, the problem has been shown EXPSPACE-complete in [START_REF] Alur | The Benefits of Relaxing Punctuality[END_REF].

In this paper, we study the model checking problems for those real-time logics on several classes of restricted sets of timed paths. We consider the model checking problems related to TCTL, MTL, and MITL when the set of timed paths is (i) a single finite (or ultimately periodic) timed path, (ii) a set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a region graph, (iii) a set of finite (or infinite) timed paths defined by a finite (or ultimately periodic) path in a zone graph. Note that in cases (ii) and (iii), the sets contain uncountably many timed paths. Note also that finite or ultimately periodic region paths as well as zone paths can be seen as simple form of timed automata.

Beside the theoretical interest to study the complexity of the model checking problems for those subcases, there are important practical reasons to study them.

First, verification algorithms for timed automata have to manipulate symbolically infinite state spaces. This is done either through the region graph or through the zone graph. When the verification of a safety or a linear-time property fails, those symbolic algorithms identify a finite or an infinite ultimately periodic path in the region graph or in the zone graph [START_REF] Bouajjani | On-the-Fly Symbolic Model Checking for Real-Time Systems[END_REF]. This path is the symbolic representation of an infinite set of timed paths that are counter-examples to the property. Usually, the information that is given back to the user is a single timed path extracted from this symbolic path. Nevertheless, it may be much more interesting to give to the user not only a single counter-example but the entire infinite set of counter-examples actually computed by the symbolic algorithm. As this counter example is symbolic, the possibility to analyze this counter-example using model checking should be given to the user. In fact, in order to better understand this infinite set of counter examples, the user may want to formulate model checking questions about this set. We should then look if we can specialize our verification algorithms for those (possibly) simpler problems.

Second, a real-time system that is executing constructs naturally a timed path that represent the evolution of its state along time. Correctness requirements about this single execution path can be expressed using a linear real-time logic, like MTL. Can we efficiently verify properties expressed by MTL formulas on this single timed path? In the dense-time framework, we know from the undecidability result for MTL that we cannot construct, as in the finite state case for LTL, a monitor (in the form of a timed automaton for example) that will enter a bad state in the case the formula is not satisfied. It is clear again that we need to look at specific techniques.

Third, if a timed automaton is too complex to be completely verified, we may be interested to test it instead. Testing a timed automaton against a set of real-time formulas consists in: (i) extracting a set of timed paths out of the timed automaton by executing it, and (ii) verifying that the set of extracted path verify some given real-time formulas. The set of timed paths can be either extracted by explicit execution of the timed automaton (in this case it is a finite set) or, more interestingly, extracted through symbolic execution of the timed automaton which amounts to visit a subset of its region or zone graph. In the two latter cases, we must check real-time formulas on infinite sets of timed paths defined by a finite set of region or zone paths. Again, for those subcases, we should look at the existence of specialized techniques.

The results that we have obtained for the model checking problems of the three real-time logics over the six classes of restricted sets of timed paths are given in Table 1. To the best of our knowledge, only the three results from the first line were known, all the other results are new. The undecidability and EXP-SPACE-hard result for the model checking of MTL and MITL over ultimately periodic region paths were unexpected and their proofs have required new encoding techniques for Turing Machine computations using timed paths. Those hardness results imply hardness results for ultimately periodic zone paths. In those proofs, all the information about the tape of the Turing Machine (TM for short) is encoded into the timing information of the path, the sequence of propositional assignments being fixed by the ultimately periodic region path. This situation is rather different from the classical proofs in [START_REF] Alur | A Really Temporal Logic[END_REF] and in [START_REF] Alur | The Benefits of Relaxing Punctuality[END_REF]. Note also that the complexity of TCTL model checking goes from PSPACE-complete to PTIME in the case of region paths which is not the case for zone paths for which the problem stays PSPACE-complete. On the other hand, when we consider finite region or zone paths, the model checking problem for MTL becomes decidable and is co-NP-complete. The proofs for those results are based on (i) a polynomial time algorithm for checking the truth value of a MTL formula over a single finite timed path and on (ii) the proof that transitions between regions (respectively zones) in a region (respectively zone) path can be chosen nondeterministically in a finite subset of the rationals with polynomially many elements to establish if a region (respectively zone) path has at least one concretization that satisfies the MTL formula.

Related work. Path model checking has been introduced in [START_REF] Markey | Model Checking a Path (Preliminary Report)[END_REF], where efficient algorithms are proposed for several untimed temporal logics (LTL, LTL+Past, ...). The basic remark there is that a CTL algorithm can be applied in order to verify LTL specifications, since path quantifier would refer to the only possible run of the structure. This does not hold here when we deal with region or zone paths.

Runtime verification and monitoring is another related issue. In that case, properties are verified on the fly during the run, as the events occur. Recently, monitoring algorithms have been proposed in the discrete-time framework for MTL [START_REF] Thati | Monitoring Algorithms for Metric Temporal Logic Specifications[END_REF].

In our work, we verify properties expressed in three important timed temporal logics. The case where the property is expressed as a timed automaton is treated in [START_REF] Alur | Membership Question for Timed and Hybrid Automata[END_REF], where the authors show that deciding if a timed trace corresponds to an execution of a given timed automaton is PSPACE-complete. This result can easily be extended to region paths.

Structure of the paper. The rest of the paper is structured as follows. In a first section, we define the classes of restricted sets of timed paths for which we study the complexity of the model checking problems. We also recall in this section the syntax and semantics of MTL, MITL, and TCTL. In a second section, we present complexity results that can be interpreted as negative: we show that for some classes of restricted sets of timed models, some model checking problems are not easier than in the general case (when the set of timed paths is defined by a timed automaton). In a third section, we present complexity results that can be interpreted as positive: we show that for some interesting classes of restricted set of timed paths, some model checking problems are easier than in the general case.

1 Preliminaries

Timed automata and paths

We write R + for the set of positive real numbers. In the sequel, all intervals we consider are convex subsets of R + with rational greatest lower and least upper bounds. An interval is said to be singular if it contains only one value. Given two intervals I and J, and a positive rational number t, we write It for the set {x ∈ R + | x + t ∈ I} and I -J for the set {x ∈ R + | ∃y ∈ J. x + y ∈ I}. Given an interval I, we note l(I) the greatest lower bound of I and r(I) least upper bound of I. An interval J follows an interval I if I ∪ J is convex, I ∩ J = ∅ and r(I) = l(J). A finite (resp., infinite) sequence of intervals

(I i ), with 0 ≤ i ≤ n (resp. 0 ≤ i) partitions a set D ⊆ R + if for any 0 < i ≤ n (resp. 0 < i), interval I i follows I i-1 and ∪ i=n i=0 I i = D (resp. ∪ i=+∞ i=0 I i = D).
Let H be a set of variables. We define the set C(H) of clock difference constraints inductively as follows:

C(H) ∋ δ, δ ′ ::= x ∼ c | x -y ∼ c | δ ∧ δ ′
for any two variables x and y in H, for ∼ in {<, ≤, =, ≥, >}, and for any integer c.

Given a valuation v for the variables in H, the boolean value of a difference constraint δ is defined in the obvious way. Moreover, for any real t, we define the valuation v + t as being the valuation x → v(x) + t, and for any subset C of H, the valuation v C as being the valuation

x ∈ C → 0, x / ∈ C → v(x).
Definition 1.1. Given a set of states Q, and a set of clocks H, a timed path1 τ = (q i , v i , I i ) is a (finite or infinite) sequence s.t.:

-

(q i ) is a sequence of states in Q; -(I i
) is a sequence of intervals forming a partition of R + (or possibly of an interval [0, p] or [0; p) in the case of a finite path); v i : H → R + is the valuation of clocks in H when entering location q i , at date l(I i ). We require that, for each i and each clock x,

either v i+1 (x) = 0 or v i+1 (x) = v i (x) + r(I i ) -l(I i );
-for each i, either q i+1 = q i , or there exists a clock x s.t. v i+1 (x) = v i (x) + r(I i )l(I i ). This ensures that, at each step along that sequence, either we change location or we reset at least one variable2 .

A position along a timed path τ = (q i , v i , I i ) is a triple (q, v, t) ∈ Q × R H × R for which there exists an integer j s.t. q = q j and v = v j + tl(I j ) and t ∈ I j . For each t ∈ ∪ i I i , there exists exactly one position (q, v, t) along τ , which we denote by τ (t). Given a timed path τ = (q i , v i , I i ) and a position (q j , v, t) along ρ, the suffix of ρ starting at position (q j , v, t), denoted by ρ ≥t , is the timed path

(q ′ i , v ′ i , I ′ i ) where (1) q ′ i = q i+j for all i, (2) v ′ i = v i+j for i > 0, and v ′ 0 = v, (3)
I ′ i = I i+j -t for i > 0, and
I ′ 0 = ([t, +∞) ∩ I j ) -t. Definition 1.2. A timed automaton (TA) is a 6-tuple A = (Q, Q 0 , H, l, Inv, T, F ) where: Q is a (finite) set of states; Q 0 is a subset of Q containing the set of initial states; H is a finite set of real-valued clocks; l is a function Q → 2 AP labeling each state with atomic propositions of AP ; Inv is a function Q → C(H) labeling each state with a set of timing constraints (called "invariants"); T ⊆ Q × C(H) × 2 H × Q is a set of transitions; F ⊆ Q is a subset of Q containing the set of accepting states.
In the sequel, we generally identify a location q ∈ Q with its labeling l(q), if no ambiguity may arise from this notation. A position in a TA is a couple (q, v) where q is a state and v is a valuation of clocks in H satisfying Inv(q). Definition 1.3. Given a set of states Q and a set of clocks H, a timed path

(q i , v i , I i ) is a concretization of a TA (Q, Q 0 , H, l, Inv, T ) if -q 0 ∈ Q 0 ;
-For each j, and for each t ∈ I j , valuation v j + tl(I j ) satisfies Inv(q j ); -For each j, there exists a transition (q j , ϕ, C, q j+1 ) ∈ E s.t. valuation v j + r(I j )-l(I j ) satisfies ϕ, and for all x ∈ C, v j+1 (x) = 0, and for all x ∈ H C, v j+1 (x) = v j (x) + r(I j )l(I j ). -either the timed path is infinite or its last state q n is accepting, that is q n ∈ F . -for all clocks x ∈ H, either both v(x) and v ′ (x) are greater than c x , or both have the same integer part;

-for all clocks x ∈ H, if v(x) ≤ c x , then v(x) ∈ N iff v ′ (x) ∈ N; -for all x, y ∈ H with v(x) ≤ c x and v(y) ≤ c y , if fract(v(x)) ≤ fract(v(y)), then fract(v ′ (x)) ≤ fract(v ′ (y))
, where fract stands for the fractional part.

This obviously defines an equivalence relation. A clock region is an equivalence class for the equivalence relation between clocks. [START_REF] Alur | A Theory of Timed Automata[END_REF] proves that there are finitely many clock regions, more precisely at most

|H|! • 4 |H| • É x∈H (c x + 1).
A clock region α is a time-successor of a clock region β if for each valuation v ∈ β, there exists a positive t ∈ R s.t. valuation v + t is in α, and for each t ′ s.t.

0 ≤ t ′ ≤ t, valuation v + t ′ is in α ∪ β.
It can be proved that, each clock region α has exactly one time-successor, which we will denote by succ(α) in the sequel. A clock region α is a boundary class if for any valuation v ∈ α and for any positive real t, valuation v + t is not in α. Definition 1.5. Given a TA A = (Q, Q 0 , H, l, Inv, T, F ), and the family (c x ) of maximal constants to which each clock x is compared in A, the region graph R A of A is the labeled graph (V, l ′ , E) defined as follows:

-V is the product of the set of states of A and the set of clock regions; l ′ : V → 2 AP is defined by l ′ (q, α) = l(q); -E is the set of edges, containing two type of edges: Edges representing the elapse of time: for each vertex (q, α) in V , there is an edge to (q, succ(α)), if succ(α) exists and contains a valuation satisfying the invariant Inv(q); Edges corresponding to transitions in A: for each vertex (q, α) in V , for each edge (q, ϕ, C, q ′ ) in T , if there exists a valuation v ∈ α satisfying ϕ and s.t. v C satisfies Inv(q ′ ), then there is an edge from (q, α) to (q ′ , β) where β is the region containing valuation v C .

Definition 1.6. A region path is a (finite or infinite) sequence ρ = (q i , α i ) where q i are locations and α i are regions s.t. for all i either α i+1 = succ(α i ), and q i+1 = q i , or there exists a valuation v ∈ α i and a set of clocks C s.t.

v C ∈ α i+1 .
Definition 1.7. A zone is a convex union of regions. It can equivalently be defined as the set of clock valuations satisfying a difference constaint in C(H). A zone path is a (finite or infinite) sequence ρ = (q i , Z i , C i ) where q i are locations, Z i are zones and C i are the sets of clocks that are reset when entering Z i .

A region (resp. zone) path π is said to be ultimately periodic (u.p. for short) if it can be written under the form u • v ω , where u and v are finite region (resp. zone) paths. In both cases, finite paths are special cases of u.p. paths. A timed path is ultimately periodic if it is finite or if there exist two integers m and p > 0, and a real t, s.t. for any i ≥ m, q i+p = q i , v i+p = v i , and

I i+p = I i + t.
Note that a finite (or u.p.) region path is a special case of a TA, where states are pairs (q i , α i ), the set of initial states is the singleton {(q 0 , α 0 )}, invariants are region constraints, clocks that are reset are clocks whose value is 0 when entering the target region, and the set of final states F is the last state pair (q n , α n ) if the path is finite and is empty otherwise. A concretization of a region path is a concretization of the corresponding TA. The following proposition provides a simplified characterization.

Proposition 1.8. Let ρ = (p i , α i ) i be a region path. We say that a timed path π = (q j , v j , I j ) j is compatible with ρ, or is a concretization of ρ, iff (1) ρ and π are either both finite or both infinite, and for all k, p k = q k , (2) for all j, for all t ∈ I j , valuation v j + tl(I j ) belongs to region α j .

Similarly, finite or u.p. zone paths form another subclass of the class of TA. We have the following simplified characterization of a concretization for a zone path: Proposition 1.9. Let ρ = (p i , Z i , C i ) i be a zone path. We say that a timed path π = (q j , v j , I j ) j is compatible with ρ, or is a concretization of ρ, iff (1) ρ and π are either both finite or both infinite, and for all k, p k = q k , (2) for all k, for all

t ∈ I k , valuation v k + t -l(I k ) belongs to zone Z k , (3) for all k, for all x ∈ C k , v k (x) = 0.
Note that a concretization of an u.p. region (or zone) path is generally not u.p. However, verifying that an u.p. timed path is a concretization of a region (or zone) path may be done in polynomial time [START_REF] Alur | Membership Question for Timed and Hybrid Automata[END_REF].

1.2 Timed Temporal Logics Definition 1.10. Let AP be a set of atomic propositions. The logic MTL is defined as follows:

MTL ∋ ϕ, ψ ::= ¬ϕ | ϕ ∨ ψ | ϕ U I ψ | p | q | ...
where I is an interval with integer greatest lower and least upper bounds and p, q, ... belong to AP . The logic MITL is the sub-logic of MTL where intervals may not be singular.

MTL (and MITL) formulas are interpreted along timed paths 3 . Given a timed path τ = (q i , v i , I i ) and an MTL formula ϕ, we say that τ satisfies ϕ (written τ |= ϕ) when:

if ϕ = p then p ∈ l(q 0 ) if ϕ = ¬ξ then τ |= ξ if ϕ = ξ ∨ ζ then τ |= ξ or τ |= ζ if ϕ = ξ U I ζ then there exists a position (q, v, t) along τ s.t. t ∈ I, τ ≥t |= ζ
and, for all t ′ ∈ (0; t), τ ≥t ′ |= ξ.

Standard unary modalities F I and G I are defined with the following semantics:

F I ξ def = ⊤ U I ξ and G I ξ def = ¬F I ¬ξ,
where ⊤ is always true. We simply write F and G for F R + and G R + , respectively. Definition 1.11. Let A be a TA, and ϕ be an MTL formula. The model checking problem defined by A and ϕ consists in determining if, for any concretization τ of A starting in an initial state, we have that τ |= ϕ. Definition 1.12. Let AP be a set of atomic propositions. The logic TCTL is defined as follows:

TCTL ∋ ϕ, ψ ::= ϕ ∨ ψ | ¬ϕ | E (ϕ U I ψ) | A (ϕ U I ψ) | p | q | ...
where I is an interval with integer greatest lower and least upper bounds and p, q, ... belong to AP .

TCTL formulas are interpreted at a position in a TA. Given a TA A, a position (q, v) and a TCTL formula ϕ, we say that position (q, v) in A satisfies ϕ, written A, (q, v) |= ϕ, when:

if ϕ = p then p ∈ l(q 0 ) if ϕ = ¬ξ then A, (q, v) |= ξ if ϕ = ξ ∨ ζ then A, (q, v) |= ξ or A, (q, v) |= ζ if ϕ = E (ξ U I ζ) then there exists a concretization τ = (q i , v i , I i ) of A s.t.
q 0 = q and v 0 = v, and a position (q

′ , v ′ , t ′ ) along τ , s.t. t ′ ∈ I, A, (q ′ , v ′ ) |= ζ and all intermediate position τ (t ′′ ) = (q ′′ , v ′′ , t ′′ ) with 0 < t ′′ < t ′ , A, (q ′′ , v ′′ ) |= ξ if ϕ = A (ξ U I ζ) then for any concretization τ = (q i , v i , I i ) of A with q 0 = q and v 0 = v, there exists a position (q ′ , v ′ , t ′ ) along τ , s.t. t ′ ∈ I, A, (q ′ , v ′ ) |= ζ and all intermediate position τ (t ′′ ) = (q ′′ , v ′′ , t ′′ ) with 0 < t ′′ < t ′ , A, (q ′′ , v ′′ ) |= ξ
We also define standard unary abbreviations E F I ξ, A F I ξ and E G I ξ, A G I ξ respectively as E (⊤ U I ξ), E (⊤ U I ξ) and ¬A F I ¬ξ, ¬E F I ¬ξ. We omit the subscript I when it equals R + . Since region and zone paths can be seen as TA, satisfaction of a TCTL formula at a position along a region or zone path is defined in the obvious way. Note that contrary to the untimed case [START_REF] Markey | Model Checking a Path (Preliminary Report)[END_REF], TCTL is not equivalent to MTL along a region or zone path, since such a path contains (infinitely) many timed paths. Definition 1.13. Let A be a TA, (q, v) be a position of A, and ϕ be a TCTL formula. The model-checking problem defined by A, (q, v) and ϕ consists in determining if A, (q, v) |= ϕ.

In the sequel, for the two problems defined above, we consider the subcases where A is (i) a single finite (or u.p.) timed path, (ii) a finite (or u.p.) region path, (iii) a finite (or u.p.) zone path.

Negative results

The main goal of restricting to subclasses of TA is to obtain feasible algorithms for problems that are hard in the general case. This section presents cases where our restrictions are not sufficient and do not reduce complexity.

Linear time logics along ultimately periodic region paths

What we expected most was that model checking MTL would become decidable along an u.p. region path. This is not the case, as shown in Theorem 2.1. The proof of this theorem requires an encoding of a TM computation by timing information only. Remember that the proof for the general model checking problem (for sets of models defined by TA) is simply a reduction from the satisfiability problem of MTL. The technique needed here is different: We encode the tape of an unbounded TM on a unit-length path by an atomic proposition being true for a strictly positive (but as small as we want) amount of time. MTL can distinguish between those two cases, and allows us to ensure that the path really encodes a computation of the TM. See Fig. 1 for an example. tape head p q p q p q p q p q p q p q p 1 time unit Proof. This is done by encoding the acceptance problem for a TM (does M accept w?) to the problem of verifying a MTL formula along a region path. Wlog, we assume that the alphabet has only two letters {a, b}, and a special symbol # for empty cells. Since the ordering of atomic propositions along the path is fixed, the contents of the tape has to be encoded through timing informations only. Since we have no bound on the total length needed for the computation, encoding of one letter must be arbitrarily compressible. Encoding of an a is done by atomic proposition q being true at only one precise moment (with duration 0), while b is encoded by q being true for a positive amount of time. An atomic proposition p is used in the same way for indicating the beginning and end of the encoding of the tape. See top of Fig. 1 for an example. For any atomic proposition x, we write x + = x U >0 ⊤ and x 0 = x∧¬x + . Then a is encoded with p + and b with p 0 .

A third letter, r, is used for encoding the position of the control head: r + is true (between p and q) at the position where the control head stands, and r + is false everywhere else. Encoding the control state (s k , for some k between 0 and n -1) is done through n 1-time-unit-long slices of the path. Along each slice, q + and r + will never be satisfied; p + will be true only in the k + 1-th slice, meaning that the current control state is s k , and false everywhere else. Fig. 1 shows a complete encoding of one configuration. The configuration separator will be the only slice where d + will hold, for a fourth atomic proposition d. There is one last atomic proposition, b, used for filling up all the gaps. The region path generating such an encoding is shown on Fig. 2.

With this encoding, it is possible to write MTL formulas ensuring the correct behavior of the TM.

In the same way, MITL model checking problems are not easier with u.p. region paths than in the general case. Again, the proof for the general model checking problem is a reduction from the satisfiability problem for MITL. Here, we cannot proceed that way and must encode the computation of an exponential space TM using a single region path and an MITL formula.

Theorem 2.2. Model checking an MITL formula along an u.p. region path is EXPSPACE-complete.

TCTL along finite or ultimately periodic zone paths

Since zones are more general than regions, hardness results for region paths extend to zone paths. Thus model checking MITL and MTL along a zone path is respectively EXPSPACE-complete and undecidable.

Regarding TCTL, the algorithm we propose for region paths (see Section 3.3) could be extended to zone paths, but would result in an exponential explosion in the number of states (since a zone may contain an exponential number of regions). In fact, this explosion cannot be avoided (unless PTIME=PSPACE), since we have the following result: Theorem 2.3. Model checking TCTL along an ultimately periodic zone path is PSPACE-complete.

Positive results

Restricting to paths sometimes allows for more efficient algorithms. This happens for MTL and MITL along single timed paths as well as along finite region or zone paths, and for TCTL along u.p. region paths.

Linear time logics and timed paths

Along a timed path, all quantitative information is precisely known, and model checking MTL can be performed quite efficiently. Proof. Consider a finite4 timed path τ = (q i , v i , I i ) i=0..p . The idea is to compute, for each subformula ψ of the MTL formula ϕ under study, the set of reals t s.t. τ ≥t |= ψ. We represent this set S ψ as a union (which we prove is finite) of intervals whose interiors are disjoint.

The sets S ψ = {J ψ i } are computed recursively as follows: -For atomic propositions, the intervals are trivially computed by "reading" the input path; -For boolean combinations of subformulas, they are obtained by applying the corresponding set operations, and then possibly merging some of them in order to get disjoint intervals. Obviously the union of two families ∪ m i=1 I i and ∪ n j=1 J j of intervals contains at most m+n intervals, and the complement of ∪ m i=1 I i contains at most m + 1 intervals. Thus the intersection of ∪ m i=1 I i and ∪ n j=1 J j contains at most m + n + 3 intervals;

-For subformulas of the form ϕ U I ψ, the idea is to consider, for each interval J ϕ i ∈ S ϕ and each interval J ψ j ∈ S ψ , the interval ((J ϕ i ∩ J ψ j ) -I) ∩ J ϕ i . It precisely contains all points in J ϕ i satisfying ϕ U I ψ with a witness for ψ in J ψ j . This construction seems to create |S ϕ | • |S ψ | intervals, but a more careful enumeration shows that it only creates at most |S ϕ | + |S ψ | + 3: indeed, the procedure only creates at most one interval for each non-empty interval J ϕ i ∩J ψ j , and the intersection of ∪ m i=1 I i and ∪ n j=1 J j contains at most m+n+3 intervals.

At the end of this procedure, S ϕ contains O(p • |ϕ|) intervals, and τ |= ϕ iff 0 is in one of these intervals. Our algorithm thus runs in time O(|τ | • |ϕ|).

Timed paths could be seen as timed automata if rational difference constraints were allowed in guards and invariants. In that case, the semantics of TCTL along a timed path would have been equivalent to the semantics of MTL, since timed automaton representing a timed path would be completely deterministic.

MTL and MITL along finite region and zone paths

The difficulty for model checking MTL along infinite u.p. region or zone paths was that we had to remember precise timing information about the (infinite, not periodic) concretization against which we verify the MTL formula. In the finite case, we prove we only have to guess and remember a finite (in fact, polynomial) amount of information, making the problem decidable: Lemma 3.2. Model checking MTL along a finite zone path is in co-NP.

Proof. We prove that the existential model checking problem is in NP, which is equivalent. The basic idea is to non-deterministically guess the dates t i at which each of the n transitions is fired. Once these dates are known, we have a timed path and we can check in polynomial time that this path is a concretization of the initial zone path and that it satisfies the MTL formula (see Theorem 3.1).

What remains to be proved is that t i 's can be chosen in polynomial time, i.e. the number of non-deterministic steps is polynomial. To that purpose, we consider an MTL formula ϕ, and prove that if ϕ is true along the region path, i.e. if there exist timestamps s.t. the corresponding timed path satisfies ϕ, then there exists timestamps in the set {p/(n + 1) | 0 ≤ p ≤ (n + 1) • (c Z + c ϕ )} where n is the number of states in the zone path, c Z is the sum of the constants appearing in the zone path and c ϕ is the sum of the constants appearing in ϕ.

The proof of this last statement is as follows: the set of (in)equalities t i 's must satisfy are: (In)equalities related to the zone path: when t i 's are "fixed", we can compute all valuations of clocks along the zone path. The constraints those valuations must satisfy give constraints that t i 's must satisfy. These constraints have the form a ≤ t it j ≤ b or a ≤ t i ≤ b; (In)equalities related to the formula: for each subformula, we can compute a set of disjoint time intervals (depending on t i 's) in which the subformula is true (see proof of Theorem 3.1). This leads to a disjunction of difference constraints, which has a solution iff the formula is true along one concretization of the finite zone path. Since a difference constraints cannot distinguish between two equivalent valuations (for the equivalence of Definition 1.4), if there exists a solution, any equivalent valuation of t i 's is a solution. This ensures that if there is a solution, then there is a solution in {p/(n+1) | p ∈ N}. Moreover, each date can be bounded with the sum of all the constants appearing in the zone path or in the formula: Indeed, constraints between t i 's only involves constants lower than this sum. Thus the dates can be guessed in polynomial time.

This algorithm is in fact optimal, and we have the following result: Theorem 3.3. Model checking MTL or MITL along finite region (or zone) paths is co-NP-complete.

The co-NP-hardness proof is similar to the one of Theorem 2.3, and consists in encoding 3-SAT into an (existential) model checking problem.

TCTL along ultimately periodic region paths

We prove that TCTL properties can be verified in polynomial time along region paths. This contrasts with the negative results we got previously for MTL and MITL, and intuitively relies on the fact that, contrary to MTL, we don't have to "remember" the precise values of the clocks when we fire a transition, since path quantifiers are applied to all modalities of the formula.

In this section, we describe our algorithm. It first requires to compute temporal relations between any two regions. Definition 3.4. Let ρ = (ρ) i be a region path. Given two integers k and l, we say that a real d is a possible delay between regions ρ k and ρ l if there exists a concretization π = (p j , v j , I j ) j of ρ, and a real t, s.t. t ∈ I k and t + d ∈ I l . We write delay(ρ, k, l) for the set of possible delays between ρ k and ρ l along ρ.

The following two lemmas prove that possible delays form an interval with integer bounds: Lemma 3.5. Given a region path ρ and two integers k and l, delay(ρ, k, l) is an interval. Lemma 3.6 ([7]). Let ρ be a region path, k, l and c be three integers. If there exists d ∈ (c; c + 1) s.t. d ∈ delay(ρ, k, l), then (c, c + 1) ⊆ delay(ρ, k, l).

There remains to compute both upper and lower bounds. [START_REF] Courcoubetis | Minimum and Maximum Delay Problems in Real-Time Systems[END_REF] designed algorithms for computing minimum and maximum delays between valuations and regions. We could apply them in our case. However, their algorithms would compute delays between regions of a finite structure, and we need to compute delays between any two regions of the infinite, u.p. path.

It happens that possible delays in an u.p. region path are u.p., but won't necessarily have the same initial and periodic parts. Below, we compute a table containing the minimum and maximum delays between one region and any future region, by computing those delays for a finite set of regions until a periodicity is detected. Thus, we build a table containing "initial" delays of the minimal and maximal paths, plus the length and duration of their periodic parts. Lemma 3.7. Let ρ = u • v ω be an u.p. region path. We can effectively build in time O(|u| 2 •|H|) the table containing all the necessary information for computing (i, j) → delay(ρ, i, j).

Proof. We build the region graph G of the product of ρ, seen as a timed automaton, and T 1 shown on Fig. 3. Graph G is not u.p. in the general case: see Fig. 4 for an example.

Since we add one new clock which is bounded by 1, the total number of regions is at most multiplied by 2(1 + |H|), corresponding to the 2(1 + |H|) possible ways of inserting fract(t) among the fractional parts of the other clocks.

In automaton T 1 , t is the fractional part of

t ≤ 1 t = 1 → t := 0 t := 0 Fig. 3: Automaton T 1
the total time elapsed since the beginning of the path, and the number of times t has been reset is the integral part of that total time. Extracting the minimal and maximal delay paths is now an easy task, since in each region of G:

-either fract(t) = 0, and possibly two transitions may be firable: one corresponding to letting time elapse, going to a region where t > 0, and the other one corresponding to the transition in ρ;

-or fract(t) > 0, and clock t can't reach value 1 in that region, because another clock will reach an integer value before; The only possible outgoing edge is the transition of the original region path; -or fract(t) > 0, and clock t can reach value 1 (and then be reset to 0). Two cases may arise: resetting t might be the only outgoing transition, or there could be another possible transition derived from the original region path. If there are two outgoing edges, firing the transition that resets t amounts to letting time elapse, and firing the other transition amounts to running as quickly as possible.

In all cases, we also have the condition that we cannot cross two successive immediate transitions, since the resulting region path would not have any concretization. Now, the maximal delay path is obtained by considering the path where we always select the transition corresponding to time elapsing, i.e. resetting t or switching from t = 0 to 0 < t < 1, when such a transition is available; The minimal delay path is the one we get when always selecting the other transition. Moreover, those minimal and maximal delay paths are u.p., since G has finitely many regions and the paths are built deterministically. They have at most |u| + From these paths, we can build a table containing all relevant information for computing minimal and maximal delays between the initial region and any region along ρ (see Fig. Proof. This is achieved by a labeling algorithm. We label region ρ i of ρ with subformula ψ of ϕ iff ρ i |= ψ. This is not ambiguous as a TCTL formula cannot distinguish between two equivalent valuations [START_REF] Alur | Model-Checking in Dense Real-Time[END_REF].

Definition 1 . 4 .

 14 Two clock valuations v and v ′ are said to be equivalent w.r.t. a family (c x ) x∈H of constants, if the following conditions hold:

Fig. 1 :Fig. 2 :

 12 Fig. 1: Encoding of the tape of a Turing Machine

Theorem 3 . 1 .

 31 Model checking MTL along a u.p. timed path is in PTIME.

ρ 0 ρ 1 ρ 2 ρ 3 ρ 4 ρ 5 Fig. 4 :

 54 Fig. 4: Computation of possible delays between regions

Theorem 3 . 8 .

 38 4(c)). Any value inbetween is a possible delay thanks to lemma 3.5. Computing this table takes time O(|u| + 2(|H| + 1) • |v|). Computing possible delays between any two states along ρ can be achieved by repeating the above procedure starting from the first |u| + |v| states of ρ (since removing longer prefixes gives rise to the same paths), thus in total time O((|u| + 2(|H| + 1) • |v|) • (|u| + |v|)) ⊆ O(|H| • |ρ| 2 ). Model checking a TCTL formula ϕ along an u.p. region path ρ can be done in polynomial time (more precisely O(|ϕ| • |ρ| • |H| + |H| • |ρ| 2 )).

  The labeling procedure runs in time O(|ϕ| • |ρ| • |H|). Since delays between regions must be computed, the global TCTL model checking problem along u.p. region paths can be performed in time O(|ϕ| • |ρ| • |H| + |H| • |ρ| 2 ).

Table 1 :

 1 Complexity of path model checking

	Finite Region Paths	co-NP-c.	co-NP-c.	PTIME
	Ult. Per. Timed Paths	PTIME	PTIME	PTIME
	Finite Timed Paths	PTIME	PTIME	PTIME

For the sake of brevity, we only consider dense time in the sequel. However, our results still hold when considering super-dense time[START_REF] Manna | Verifying Hybrid Systems[END_REF].

This conditions rules out "stuttering" paths. This is not restrictive as our logics, as you'll see later, cannot distinguish between timed traces with or without stuterring.

For the sake of simplicity, we interpret MTL (and MITL) formulas directly on timed paths instead of defining a notion of timed model where states and clocks are hidden.

We describe our algorithm only for finite paths, but it can easily be extended to infinite u.p. paths, by reasoning symbolicaly about the periodic part.