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

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

Model Checking Restricted Sets of Timed Paths

Keywords: Model checking, path checking, timed automaton, timed path, clock region, timed temporal logics Undecidable EXPSPACE-c. PSPACE-c. Ult. Per. Region Paths PTIME Finite Region Paths Decidable Ult. Per. Timed Paths PSPACE-h. PTIME

HAL is

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 [START_REF] Pnueli | The temporal logic of programs[END_REF]. Four 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 CTL [START_REF] Clarke | Design and synthesis of synchronous skeletons using branching-time temporal logic[END_REF], while TPTL [START_REF] Alur | A really temporal logic[END_REF], MTL [START_REF] Koymans | Specifying real-time properties with metric temporal logic[END_REF] and MITL [START_REF] Alur | The benefits of relaxing punctuality[END_REF] are extensions of LTL [START_REF] Gabbay | On the temporal analysis of fairness[END_REF].

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]. The PSPACE algorithm relies on the region graph construction, which is a quotient of the timed automaton by an equivalence relation on clock valuations. In practice, zones, i.e. convex union of regions, are used, since they may gather up to an exponential number of regions. For the logics TPTL and 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 over several classes of restricted sets of timed paths. We consider the model checking problems related to the four logics above 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 forms of timed automata.

Beside the theoretical interest to study the complexity of the model checking problems for those subcases, there are also 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 lineartime 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 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 it using model checking should be given to the user. In fact, in order to better understand this infinite set of counterexamples, the user may want to formulate model checking questions about this set. We should then examine whether 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 represents 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 PSPACE-complete to PTIME in the case of region paths; it 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 problems for TPTL becomes decidable. For that logic, we prove a PSPACE lower bound but we have no upper bound. As regards MTL, we show that these problems are co-NP-complete. The proofs for these latter results are based on (i) a polynomial time algorithm for checking the truth value of an 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[END_REF]; that paper proposes efficient algorithms for path moedl checking 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 quantifiers would refer to the only possible run of the structure. This does not hold here: region or zone paths may contain infinitely many timed paths.

Runtime verification and monitoring [START_REF]Proceedings of the 1st International Workshop on Runtime Verification (RV 2001)[END_REF] are other related issues. 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 four 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 whether a finite timed trace corresponds to an execution of a given timed automaton is already PSPACE-complete.

Structure of the paper. The rest of the paper is structured as follows.

In the 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 the logics under study. In the 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 just as difficult as in the general case (when the set of timed paths is defined by a timed automaton). In the third section, we present complexity results that can be interpreted as positive: We show that for some interesting classes of restricted sets 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 nonnegative 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 I -t 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 denote the greatest lower bound of I with l(I) and the least upper bound of I with r(I). The closure of an interval I, denoted by I, is the union I ∪ {l(I), r(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 nonnegative 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 ← 0] as being the valuation that maps clocks in C to 0 and other clocks to their value according to v.

Definition 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) s.t. for all i, I i+1 follows I i ; • 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

• q ′ i = q i+j for all i, • v ′ i = v i+j for i > 0, and v ′ 0 = v, • I ′ i = I i+j -t for i > 0, and
I ′ 0 = ([t, +∞) ∩ I j ) -t.
Definition 2 Let AP be a finite, non empty set of atomic propositions. A timed automaton (TA) is a 6-tuple A = (Q, Q 0 , H, lab, 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;

• lab 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 finite set of transitions; • F ⊆ Q is a subset of Q containing the set of accepting states.
In the sequel, we generally identify a state q ∈ Q with its labeling lab(q), if no ambiguity may arise from this notation. A position in a TA is a pair (q, v) where q is a state and v is a valuation of clocks in H satisfying Inv(q). Definition 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, or is compatible with, 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 .

Definition 4 Two clock valuations v and v ′ are said to be equivalent w.r.t. a constant M , if the following conditions hold:

• for all clocks x ∈ H, either both v(x) and v ′ (x) are greater than M , or both have the same integer part;

• for all clocks x ∈ H, if v(x) ≤ M , then v(x) ∈ N iff v ′ (x) ∈ N; • for all x, y ∈ H with v(x) ≤ M and v(y) ≤ M , if fract(v(x)) ≤ fract(v(y)), then fract(v ′ (x)) ≤ fract(v ′ (y))
, where fract stands for the fractional part. Definition 5 Given a TA A = (Q, Q 0 , H, lab, 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, lab ′ , E) defined as follows:

• V is the product of the set of states of A and the set of clock regions w.r.t. the constant M = x c x ; • lab ′ : V → 2 AP is defined by lab ′ (q, α) = lab(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 ← 0] satisfies Inv(q ′ ) (or, equivalently, if all valuations in α satisfy these conditions), then there is an edge from (q, α) to (q ′ , β) where

β is the region containing valuation v[C ← 0].
Definition 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 ← 0] ∈ α i+1 .
Definition 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 in 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 each i ≥ m, q i+p = q i , v i+p = v i , and

I i+p = I i + t.
The length of a region (or zone) path π, denoted by |π|, is the smallest sum m + p for m and p verifying both requirements above.

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 8 Let ρ = (p i , α i ) i be a region path. A timed path π = (q j , v j , I j ) j is compatible with ρ iff there exists an increasing function f from the index set of (ρ i ) i onto the index set of (π j ) j s.t.

• the index sets of ρ and π are either both finite or both infinite, and for all k, p k = q f (k) , • for all j, for all t ∈ I f (j) , valuation v f (j) + tl(I f (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 9 Let ρ = (p i , Z i , C i ) i be a zone path. A timed path π = (q j , v j , I j ) j is compatible with ρ iff there exists an increasing function f from the index set of (ρ i ) i onto the index set of (π j ) j s.t.

• ρ and π are either both finite or both infinite, and for all k,

p k = q f (k) , • for all k, for all t ∈ I f (k) , valuation v f (k) + t -l(I f (k) ) belongs to zone Z k , • for all k, for all x ∈ C k , v f (k) (x) = 0.
Note that a concretization of an u.p. region (or zone) path is generally not u.p. Consider for instance the u.p. region path displayed on figure 8(a): one concretization of that region path is the path where, clocks x and y are reset when they reach 1/2, except at the 2 p -th run through the loop, for each integer p, where they are reset when they reach 1/4. 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].

Timed Temporal Logics

Definition 10 Let AP be a finite, non empty set of atomic propositions. The logic MTL is defined as follows:

MTL ∋ ϕ, ψ ::= p | ¬ϕ | ϕ ∨ ψ | ϕ U I ψ
where I is an interval whose bounds are in N ∪ {∞}, and p is any atomic proposition in AP . The logic MITL is the sub-logic of MTL where intervals may not be singular.

The size of an MTL (or MITL) formula is defined inductively on the structure of the formula. For instance, MTL (and MITL) formulas are interpreted along timed paths3 . Given a timed path τ = (q i , v i , I i ) and an MTL formula ϕ, we say that τ satisfies ϕ (written τ |= ϕ) when:

if ϕ = p then p ∈ 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 ⊤, defined as p ∨ ¬p for some atomic proposition p, is always true. We simply write F and G for F R + and G R + , respectively.

Definition 11 Let AP be a set of atomic propositions, and V be a set of variables s.t. V ∩ H = ∅. The logic TPTL is defined as follows:

TPTL ∋ ϕ, ψ ::= p | ¬ϕ | ϕ ∨ ψ | ϕ U ψ | x. ϕ | δ
where p is any atomic proposition in AP , x ∈ V is a clock variable, and δ ∈ C(V ) is a difference constraint involving only variables in V .

As for MTL, the size of a TPTL formula is defined inductively, still using binary notation for integers appearing in difference constraints.

Here again, formulas are interpreted along timed paths, but the interpretation depends on the valuation of variables appearing in the formula: Given a timed path τ = (q i , v i , I i ), an TPTL formula ϕ and a valuation E of the variables in the formula, we say that τ, E satisfies ϕ (written τ |= E ϕ) when:

if ϕ = p then p ∈ q 0 if ϕ = ¬ξ then τ |= E ξ if ϕ = ξ ∨ ζ then τ |= E ξ or τ |= E ζ if ϕ = ξ U ζ then there exists a position (q, v, t) along τ s.t. τ ≥t |= E+t ζ and, for all t ′ ∈ (0, t), τ ≥t ′ |= E+t ′ ξ. if ϕ = x -y ∼ c then E(x) -E(y) ∼ c if ϕ = x ∼ c then E(x) ∼ c if ϕ = x. ϕ then τ |= E[x←0] ϕ
In this definition, E+t represents the function

E ′ : x → E(x)+t for each variable x ∈ V , and E[x ← 0] is the function E ′ s.t. E ′ (x) = 0 and E ′ (y) = E(y) for each y = x. A timed path τ satisfies a TPTL formula ϕ whenever τ |= E 0 ϕ with E 0 (x) = 0 for each variable x ∈ V .
Obviously enough, MTL formulas can be translated into TPTL. The question whether TPTL is strictly more expressive than MTL has recently been answered (positively): the TPTL formula x.F (a ∧ x ≤ 1 ∧ ¬b U (a ∧ x ≥ 1)) cannot be expressed in MTL [START_REF] Bouyer | TPTL is strictly more expressive than MTL[END_REF].

Definition 12

Let A be a TA, and ϕ be an MTL, MITL or TPTL 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 13 Let AP be a finite, non empty set of atomic propositions. The logic TCTL is defined as follows:

TCTL ∋ ϕ, ψ ::= p | ¬ϕ | ϕ ∨ ψ | E (ϕ U I ψ) | A (ϕ U I ψ)
where I is an interval with bounds in N∪{∞}, and p is any atomic proposition in AP .

The size of a TCTL formula is defined in the same way as for MTL.

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 (q, v) in A satisfies ϕ, written A, (q, v) |= ϕ, when:

if ϕ = p then p ∈ 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 for all intermediate positions τ (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 for all intermediate positions τ (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.

Definition 14 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 (Def. 12 and 14), 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 to achieve this goal, and do not reduce complexity. tape head p q p q p q p q p q p q p q p 1 time unit r r r r r r r control state tape config.

separator Fig. 1. Encoding of the tape of a Turing Machine

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 15. However, the proof here requires an encoding of a Turing machine, while for the general model checking problem (for sets of models defined by TA), it is simply a reduction from the satisfiability problem for MTL.

Theorem 15 Model checking a MTL formula along an u.p. region path is undecidable.

PROOF. The proof is by encoding the acceptance problem for a TM (does M accept w?) to the problem of verifying an MTL formula along a region path. Wlog, we assume that the alphabet of the TM 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 information only. Since we have no bound on the total length needed for the computation, we require that the encoding of one letter can be made arbitrarily small.

Encoding of letter a is done by atomic proposition q being true in a non-empty open interval (thus for a strictly positive amount of time), while letter b is encoded by q being true on a singular interval (with duration 0). To encode this, we define the following abreviations for each atomic proposition x:

x

+ def = ¬x ∧ (x U (0,∞) ¬x) x 0 def = x ∧ (¬x U (0,∞) ⊤)
Thus letter a is encoded with q + being true "not too far away from the next configuration delimiter" (this will be made more precise later), and letter b with q 0 . An atomic proposition p is used in the same way for indicating the beginning and end of the encoding of the tape. 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 (except that we omitted d's) 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.

It now suffices to encode the behavior of the TM through an MTL formula. Below, we write a set of formulas whose conjunction Φ satisfies the following equivalence:

M accepts w iff ∃π compatible with ρ s.t. π |= Φ
where ρ is the path shown on Fig. 2. This clearly entails undecidability of MTL model checking along a region path.

We first define the following abbreviations:

ϕ delim def = p + ∧ F [0,1) d + ϕ tape def = p + ∧ F [1,1] ϕ delim ϕ a def = F [0,1) ϕ delim ∧ q + ϕ cs def = p + ∧ ¬ϕ tape ∧ ¬ϕ delim ϕ b def = F [0,1) ϕ delim ∧ q 0 ϕ cs def = p 0 ∧ ¬ϕ tape ∧ ¬ϕ delim ϕ letter def = ϕ a ∨ ϕ b ϕ head def = r + ∧ F [0,1) ϕ delim
We split the formulas to be verified in several groups:

• Except for b, we first require that intervals where an atomic proposition holds are either singular or closed: For each atomic proposition x in {p, q, r, d}, we require the following:

¬F (¬x U (x ∧ x U >0 ⊤)) ∧ ¬F (x U (x ∧ (¬x) U >0 ⊤))
This way, any interval where x holds is either a witness for x 0 or a witness for x + . Moreover, (x 0 ∨ x + ) holds precisely at the left end of the closure of that interval. • Formulas ensuring that the path is correctly sliced as explained above:

(¬ϕ delim U =n+1 ϕ delim ) ∧ G (ϕ delim ↔ (¬ϕ delim U =n+2 ϕ delim )) (¬ϕ tape U =n ϕ tape ) ∧ G (ϕ tape → (¬ϕ tape U =n+2 ϕ tape )) (p 0 ∨ p + ) ∧ G (((p 0 ∨ p + ) ∧ ¬ϕ tape ) → (¬(p 0 ∨ p + ) U =1 (p 0 ∨ p + )))
The first line ensures that the delimiter occurs after n + 1 time units, and then exactly each n + 1 time units. The second one checks that the encoding of the tape starts exactly one t.u. before each delimiter. The last line ensures that, except during the encoding of the tape, one run through the loop of the region path takes exactly one t.u.

• Each part between two consecutive delimiters corresponds to a configuration of the TM:

G (ϕ delim → ((¬ϕ delim ∧ ¬ϕ cs ) U (ϕ cs ∧ ¬ϕ delim ∧ (¬ϕ cs U ϕ delim )))) G (ϕ tape → (¬ϕ t h U <1 (ϕ head ∧ (¬ϕ head U ϕ delim ))))
These formulas ensure resp. that there is exactly one control state and one tape head in each configuration.

• The initial state is correct (the tape initially contains w):

ϕ cs ∧ F =1 ϕ cs ∧ . . . ∧ F =n-1 ϕ cs ∧ F =n (ϕ tape ∧ ((¬q U (ϕ w 0 ∧ (¬p U (p ∧ ¬q U (ϕ w 1 ∧ . . . U (ϕ w k ∧ ¬p U ϕ delim ) • • • ))))
• Transitions are applied correctly between two successive configurations:

There are several cases here.

• First, we have to ensure that we always have at least as many cells on the tape from one configuration to the next one:

G ((F <1 ϕ delim ∧ p) → F =n+2 p)
The following formula ensures that we will not add one cell between the other ones, by ensuring that no p is added. We express that b's that are followed by a p before the configuration delimiter may only be turned to r's or q's, or left unchanged:

G ((F <1 ϕ delim ∧ (¬ϕ delim U (p ∧ ¬ϕ delim )) ∧ b) → F =n+2 (b ∨ r ∨ q))
We now express that, except for the cell that is under the tape head, letters are copied verbatim from one configuration to the next one:

G ((F <1 ϕ delim ∧ p 0 ∧ (¬r U (r 0 ∧ ¬ϕ letter U ϕ a ))) → F =n+2 (p 0 ∧ ¬ϕ letter U ϕ a )) G ((F <1 ϕ delim ∧ p 0 ∧ (¬r U (r 0 ∧ ¬ϕ letter U ϕ b ))) → F =n+2 (p 0 ∧ ¬ϕ letter U ϕ b ))
• For transition (s i , a) → (s j , b, Right), two cases may arise, depending on whether we must "add" a new cell at the end of the tape or not. In the first case:

G ((F =n+1 ϕ delim ∧ F =i ϕ cs ∧ F <n+1 (ϕ head ∧ ¬ϕ letter U (ϕ a ∧ ¬p U ϕ delim ))) → (F =n+2+j ϕ cs ∧ F <n+1 (ϕ head ∧ (¬ϕ letter U (ϕ a ∧ F =n+2 (ϕ b ∧ (¬ϕ delim U (p 0 ∧ (¬p U (ϕ head ∧ (¬p U (ϕ a ∧ ¬p U ϕ delim ))))))))))))
In the second case:

G ((F =n+1 ϕ delim ∧ F =i ϕ cs ∧ F <n+1 (ϕ head ∧ ¬ϕ letter U (ϕ a ∧ F <1 (¬ϕ letter ∧ F <1 ϕ letter )))) → (F =n+2+j ϕ cs ∧ F <n+1 (ϕ head ∧ (¬ϕ letter U (ϕ a ∧ F =n+2 (ϕ b ∧ (¬ϕ delim U (p 0 ∧ (¬p U (ϕ head ∧ (¬p U ϕ a )))))))))∧ F =n+2 (F <n+2 (p 0 ∧ ¬p U ϕ delim ∧ F =n+2 (p 0 ∧ ¬p U ϕ delim )))))
• Transitions "to the left" are handled in a similar way (except that we must handle separately the case where the tape head is on the first cell of the tape)..

• Last, we must ensure that the accepting state (s n , say) is eventually reached. This is achieved through formula F (ϕ delim ∧ F =n ϕ cs ).

Now assume there exists a concretization of ρ satisfying the conjunction of those formulas. It suffices to slice that path into n + 2-time-unit-long slices in order to get an accepting computation of the Turing machine. Conversely, if the Turing machine accepts w, it is possible to encode an accepting execution into a timed path compatible with ρ and satisfying Φ.

In the same way, MITL model checking problems are not easier over 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 16 Model checking an MITL formula along an u.p. region path is EXPSPACE-complete.

PROOF. It is well known that the model checking problem for MITL is EXP-SPACE-complete on classical TA in dense time [START_REF] Alur | The benefits of relaxing punctuality[END_REF]. Our problem is thus in EXPSPACE. We prove that it is EXPSPACE-hard by encoding an exponential space deterministic TM as an MITL ultimately periodic region path model checking problem.

Each cell of the tape is encoded using a slice of total duration at most n + 7, where n is the number of control states in the TM. Along one slice, the first part (starting with atomic proposition l) is used for encoding the content of the current cell, the next one (starting with s) for the control state, the next one (starting with h) for the tape head and the last one (starting with d) for a configuration delimiter. A proposition p is used for the encoding: Letter a is encoded by the next p being true less than 1 t.u. after l, while letter b is encoded by p being true at some point between 1 and 2 t.u. after l. The presence of the tape head is encoded by p being true less than 1 t.u. after h; the end of the encoding of a configuration by p being true less than 1 t.u. after d.

As regards control states: State s k corresponds to p being true between time k and time k + 1 after s. Note that the relevant value for the control state is the one defined in the (only) configuration where the tape head lies. Fig. 3 shows a sample path, and Fig. 4 shows the region path we consider in the rest of this proof.

The region-path

We now enumerate the conditions a path should satisfy to encode a complete computation of the TM. More precisely, for a word w and an exponential space Turing machine M, we define a formula Φ ∈ MITL s.t.

M accepts w iff ∃π compatible with ρ s.t. π |= Φ where ρ is the region path of Fig. 4. We also require that the size of the formula Φ is polynomial in the sizes of M and w.

We will use the following abbreviations:

ϕ delim def = d ∧ F [0,1) p ϕ head def = h ∧ F [0,1) p ϕ a def = l ∧ F [0,1) p ϕ b def = l ∧ F [1,2] p ϕ # def = l ∧ G [0,2] ¬p
• We ensure that exactly 2 t.u. elapse between l and s, h and d, and d and l, and exactly n between s and h:

G (l → (¬s U [2,∞) ∧ ¬s U [0,2] s)) ∧ G (s → (¬h U [n,∞) h ∧ ¬h U [0,n] h))∧ G (h → (¬d U [2,∞) d ∧ ¬d U [0,2] d)) ∧ G (d → (¬l U [2,∞) l ∧ ¬l U [0,2] l))
• There is a delimiter every T cells, where T is the length of the tape:

G (ϕ delim → ((¬ϕ delim ) U [((n+7)•T -1),((n+7)•T +1)] ϕ delim ))∧ (¬ϕ delim ) U [((n+7)•T -2),((n+7)•T )] ϕ delim
Since integers are written using binary notation, the size of this formula is polynomial in the size of the TM. • The initial configuration is correct (the first k cells contain w, where k is the length of w, and the other ones contain #):

G [0,1] (l → ϕ w 0 ) ∧ G [(n+7),(n+7)+1] (l → ϕ w 1 ) ∧ ... G [(k+1)(n+7),(T -1)(n+7)+1] (l → ϕ # )∧ F [0,n+7) (s ∧ F <1 p) ∧ F [0,n+7) ϕ head
• All configurations contain exactly one tape head:

G (ϕ head → (¬ϕ head U ϕ delim )) ∧ G (ϕ delim → (¬ϕ delim U ϕ head ))
• Transitions are applied correctly. We write this formula for a transition (s k , a) → (s m , b, RIGHT) and leave the other cases since they are similar:

G (ϕ a ∧ F [0,n+7) (s ∧ F [k,k+1] p ∧ F [k-1,k] p) ∧ F [0,n+7) ϕ head ) → F [(n+7)•T -1,(n+7)•T ] (ϕ b ∧ F [0,n+7) (s ∧ F [m,m+1] p ∧ F [m-1,m] p)∧ F [n+6,n+7] (l ∧ F [0,n+7) ϕ head ))
• Except around the tape head, the content of the tape is not modified between two consecutive configurations: For each letter x in {a, b, #},

G ((ϕ x ∧ G [0,n+7) ¬ϕ head ) → F [(n+7)•T -1,(n+7)•T ] ϕ x )
• Finally, we must reach the accepting state (assuming the only accepting state of the TM is s n ):

F (s ∧ (¬p U [n-1,n] p))

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 increase in the number of states (since a zone may contain an exponential number of regions). In fact, this increase cannot be avoided (unless PTIME=PSPACE), since we have the following result:

Theorem 17 Model checking TCTL along an ultimately periodic zone path is PSPACE-complete.

PROOF. Membership in PSPACE already occurs for general TA. PSPACEhardness is proved by reduction from QBF. We prove PSPACE-hardness by reducing QBF to our model checking problem. To this aim, consider an instance ϕ = Q 1 p 1 . Q 2 p 2 . . . . Q n p n . ψ of QBF, where ψ = m j=1 (l j,1 ∨ l j,2 ∨ l j,3 ) and Q i ∈ {∀, ∃} for any i s.t.

1 ≤ i ≤ n.
The zone path we consider is made of two parts: In the initial part, we "encode" values of the boolean variables, and in the second part, we check if ψ is satisfied. See Fig. 5 for the details.

We encode the fact that p i is true by staying exactly one time unit in state P i , i.e. by moving to R i when x i = 1. In that case, when we enter in i , y i = x i -1 and we can stay in in i for one time unit, making l j,i true. On the other hand, if we moved to R i with x i < 1, then when entering in i , y i > 1x i and we cannot stay in in i for one time unit.

We are left to write the TCTL formula to be evaluated along that path. The formula has the following form:

ϕ = Q ′ 1 F (P 1 ∧ Q ′ 2 F (P 2 . . . Q ′ n F (P n ∧ E F (G ∧ ψ)) . . .)) I P 1 R 1 P 2 R n G x 1 :=0 y 1 :=0 x 2 :=0 yn:=0 with Inv(I) = 0 ≤ x 1 = y 1 = • • • = x n = y n ≤ 1 Inv(P i ) = 0 ≤ x i ≤ 1, Inv(R i ) = 0 ≤ y i ≤ 1
"Encoding" part: where

G in 1 out 1 in 2 in n end "Verification" part: with Inv(G) = x 1 ≤ 2n Inv(end) = 2n ≤ y n Inv(in i ) = y i ≤ 2n ≤ x i Inv(out i ) = x i ≤ 2n ≤ y i-1
Q ′ i = A (resp. E ) if Q i = ∀ (resp. ∃), and ψ = m j=1 l j,1 ∨ l j,2 ∨ l j,3 with if l j,i = p k then l j,i = E F (in k ∧ E F =1 in k ) if l j,i = ¬p k then l j,i = E (¬in k U (in k ∧ ¬E F =1 in k )

TPTL along finite paths

It is well-known that the logic TPTL subsumes the logic MTL [START_REF] Alur | A really temporal logic[END_REF]. As a consequence, we know that the model-checking of TPTL over timed automata, ultimately periodic zone paths and ultimately periodic zone path are undecidable.

Here, we show that model-checking the logic TPTL is harder than MTL. In fact, we show in this subsection that model-checking a TPTL formula against a finite timed path is already PSPACE-hard. In our opinion, this means that TPTL is hardly usable as a specification language within an automatic verification method.

Theorem 18 Model checking a TPTL formula along a finite timed path is PSPACE-hard.

PROOF. The proof consists in encoding a QBF instance into a TPTL formula that will be evaluated along a simple timed path τ = (q, 0, [0, n + 1])

where n is the number of variables involved in the QBF instance.

Let ϕ be a QBF instance. Wlog, we may assume that it has the form ∀x 1 . ∃x 2 . ∀x 3 . . . . ψ(x 1 , x 2 , x 3 , . . .). and that each variable x i is quantified exactly once. Now consider the TPTL formula obtained by recursively applying the following transformations to ϕ:

∀x i .ψ translated to G [(X i = 0 ∨ X i = 1) → X i+1 . ψ] ∃x i .ψ translated to F [(X i = 0 ∨ X i = 1) ∧ X i+1 . ψ] ψ(x 1 , x 2 , . . .) translated to ψ(X 1 -X 2 = 1, X 2 -X 3 = 1, . . . , X n -X n+1 = 1)
This TPTL formula involves n+1 real variables X i , and the truth value of each boolean variable x i of the orignial QBF instance is encoded by the difference X i -X i+1 being compared to 1. This difference is constant once X i+1 has been "reset", and it equals 0 or 1 depending on the value of X i at the time it is reset. Obviously enough, the TPTL formula holds along τ iff the initial QBF instance is true.

As a corollary, we have that:

Corollary 19 Model checking a TPTL formula along an ultimately periodic timed path is PSPACE-hard.

The proof above can be trivially adapted to establish the following theorem:

Theorem 20 Model checking a TPTL formula along a finite zone path or a finite region path is PSPACE-hard.

So, TPTL model-checking is already difficult for our simpliest problems. For the sake of completeness, we show here that those four restricted modelchecking problem even if hard are solvable algorithmically. We first show that the model-checking problem of a TPTL formula against a finite zone path or a finite region path is reducible to the validity checking of sentences in the additive theory of the reals.

Theorem 21 Model checking a TPTL formula along a finite zone path or a finite region path is decidable.

PROOF. We prove the result for finite zone path as it is more general. Let ρ be a finite zone path (q 0 , Z 0 , C 0 )(q 1 , Z 1 , C 1 ) . . . (q n , Z n , C n ). Any concretization π of ρ is completely caracterized by the following two items of information:

• the sequence of time stamps t 0 , t 1 , . . . , t n-1 , t n where each t i , for 0 ≤ i ≤ n -1, is the time at which π jumps from zone Z i to zone Z i+1 , and t n is the time of the end of π if π is a finite timed path or +∞ if π is infinite. • the sequence of bits b 0 , b 1 , . . . , b n that says if at time t i , π is still in zone Z i , in that case b i = 1, or already in zone Z i+1 , in that case b i = 0. The set of all those sequences is denoted by B.

When B ∈ B is fixed, the sequence of time stamps t 0 , t 1 , . . . , t n must satisfy the following set of constraints that can be defined in the additive logic of the reals:

(1) the sequence of time stamps is increasing. So, we have the constraint:

t 1 ≤ t 2 ≤ • • • ≤ t n ;
(2) the sequence of time stamps t 0 , t 1 , . . . , t n gives the times at which clocks are reset along the concretization π of ρ. This sequence must be consistent with the constraints on clocks contained in the zones along ρ. As a consequence, for each i, 0 ≤ i ≤ n, we have that:

• for each clock constraint of the form x ∼ c in Z i , let k ≤ i be the greatest index such that x ∈ C k . We construct the following constraint:

∀t : t i-1 ∼ 1 t ∼ 2 t i : t -t k ∼ c, if i ≥ 1 ∀t : 0 ≤ t ∼ 2 t 0 : t -t k ∼ c, if i = 0.
where

∼ 1 is < if b i-1 is 1 and ≤ otherwise, and conversely, ∼ 2 is ≤ if b i is 1, and < otherwise. • for each i ≥ 1 and each clock constraint of the form x -y ∼ c in Z i , let k 1 ≤ i (respectively k 2 ≤ i) be the greatest index such that x ∈ C k 1 (respectively y ∈ C k 2 )
. The associated constraint is:

t k 2 -1 -t k 1 -1 ∼ c
We denote by Ψ ρ B (t 0 , t 1 , . . . , t n ) the conjunction of all the constraints above.

Given a TPTL formula ϕ, our finite zone path ρ, and a sequence of bits B = b 0 , b 1 , . . . , b n , we now explain how to construct a formula of the additive theory of the reals over the free variables t 0 , t 1 , . . . , t n that formalizes the semantics of ϕ over any concretization π of ρ that respects B.

Given a proposition p, let I(ρ, B, p) denote the set of symbolic intervals I i for each 0 ≤ i ≤ n such that p ∈ q i . Each such interval I i is as follows:

l(I i ) = t i-1 , if i ≥ 1, and l(I i ) = 0 if i = 0, r(I i ) = t i ,
and, furthermore,

I i is left-open iff b i-1 = 1, and I i is right closed iff b i = 1.
This set of intervals will allow us to construct constraints for atomic propositional formulas.

As TPTL formulas contain clock variables, we need to know at which time each clock variable has last been reset. This is formalized in the following by the function r that maps each clock to the last time at which it has been reset.

We are now fully equipped to define the function Tr that given a TPTL formula ϕ, a finite zone path ρ, a sequence of bits B, a time variable t and a reset function r returns a formula of the additive logic of the reals that formalizes the semantics of ϕ at time t along any concretization π of ρ that respect B. This function Tr is defined on the structure of TPTL formulas as follows:

• Tr (p, ρ, B, t, r) = I∈I(ρ,B,p) t ∈ I • Tr (x ∼ c, ρ, B, t, r) = t -r(x) ∼ c • Tr (x.ϕ, ρ, B, t, r) = Tr (ϕ, ρ, B, t, r[x → t]) • Tr (ϕ 1 ∧ ϕ 2 , ρ, B, t, r) = Tr (ϕ 1 , ρ, B, t, r) ∧ Tr (ϕ 1 , ρ, B, t, r) • Tr (¬ϕ, ρ, B, t, r) = ¬Tr (ϕ, ρ, B, t, r) • Tr (ϕ 1 Uϕ 2 , ρ, B, t, r) = ∃t 1 ≥ t : Tr (ϕ 2 , ρ, B, t 1 , r) ∧ ∀t 2 : t < t 2 < t 1 :
Tr (ϕ 1 , ρ, B, t 2 , r).

We are now ready to define the reduction of the finite zone path modelchecking problem of TPTL to the validity problem of a formula of the additive theory of the reals. In fact, by construction, we have that:

ρ |= ϕ iff B∈{0,1} n+1 ∀t 0 , t 1 , . . . , t n : (Ψ ρ B → Tr (ϕ, ρ, B, 0, r 0 ))
where n is the length of ρ and r 0 (x) = 0 for any clock x that appears in ϕ.

An easy adaptation of the last proof allow us to establish that:

Theorem 22 Model checking a TPTL formula along a finite timed path is decidable.

For utimately periodic path, we need to use the additive theory of the reals extended with the integer predicate. This extended logic allows us to characterize the periodic part to the timed path:

Theorem 23 Model checking a TPTL formula along a ultimately periodic timed path is decidable.

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.

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

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 . If 0 ∈ I, we must also add intervals J ψ j , since those points also satisfy ϕ U I ψ but might not belong to any J ϕ i . The construction ((J ϕ i ∩ J ψ j ) -I) ∩ J ϕ i 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 nonempty 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. 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 25 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 24). What remains to be proved is that the 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 zone 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 the 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 the 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 the t i 's) in which the subformula is true (see proof of Theorem 24).

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 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 by the sum of all the constants appearing in the zone path or in the formula. Indeed, constraints between the t i 's only involve 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:

Lemma 26 Model checking MITL along a finite region path is co-NP-hard.

PROOF. Here again, we prove that the dual problem is NP-hard by providing a reduction from 3-SAT. Let ϕ = m i=1 (l i,1 ∨ l i,2 ∨ l i,3 ) be an instance of 3-SAT, built using a set of atomic propositions {p 1 , . . . , p n }. We consider the finite region path ρ shown on Fig. 6. It uses only one clock x, and atomic propositions {q 1 , . . . , q n }. The encoding is as follows: an atomic proposition p i in the 3-SAT instance is evaluated to true iff the corresponding atomic proposition q i (in the region path) holds for more than 1 t.u. along the concretization.

q 1 0<x<1 q 1 x=0 q 1 0<x<1 q 1 x=0 x:=0 x:=0 q 2 0<x<1 q 2 x=0 q 2 0<x<1 q 2 x=0 x:=0 x:=0 q n 0<x<1 q n x=0 q n 0<x<1 q n x=0 x:=0 x:=0
Fig. 6. The path associated to an instance of 3-SAT Formula ϕ is then easily transformed into the

MITL formula ϕ = m i=1 ( l i,1 ∨ l i,2 ∨ l i,3 ) where l i,j = F (q k ∧ F (1,2) q k ) if l i,j = p k , and l i,j = ¬F (q k ∧ F (1,2) q k ) if l i,j = ¬p k .
There exists a concretization of ρ satisfying ϕ iff ϕ is satisfiable.

The previous two Lemmas entail the following Theorem:

Theorem 27 Model checking MTL or MITL along finite region (or zone) paths is co-NP-complete.

Lemma 30 ( [START_REF] Bruyère | Durations, parametric model checking in timed automata with Presburger arithmetic[END_REF]) 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).

PROOF. We consider the product of the suffix ρ k (seen as a TA) of ρ starting at state k, with the TA T 1 shown on Fig. 7 (assuming that clock t of T 1 does not occur in ρ). By construction of T 1 , clock t represents the fractional part of the total time elapsed since the beginning of the run, and the integer part is the number of times t has been reset.

Consider the region graph corresponding to the resulting TA: By hypothesis, there exists a timed path starting in the initial region (namely (ρ k , t = 0)) and reaching the region (ρ l , 0 < t < 1), namely with t = fract(d). Since the transition relation of the region graph is back-stable [START_REF] Alur | Computing accumulated delays in real time systems[END_REF], it follows that, for any clock valuation v in (ρ l , 0 < t < 1), there exists a timed path starting in the initial region (ρ k , t = 0), crossing exactly the same regions, and ending with valuation v. That is, for any 0 < δ ′ < 1, there exists a timed path starting in region (ρ k , t = 0), along which t is reset exactly c times, and ending with t = δ ′ . The same argument can be applied for finding the first part of the path, i.e. the offset t ′ . This proves that c + δ ′ is a possible delay between ρ k and ρ l along ρ.

There remains to compute both upper and lower bounds. In [START_REF] Courcoubetis | Minimum and maximum delay problems in real-time systems[END_REF], Courcoubetis and Yannakakis 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. This table contains all the necessary information for computing the delays between any two regions along the region path.

Lemma 31 Let H be a set of clocks, and ρ = u • v ω be an u.p. region path involving clocks in H. We can effectively compute, in time O(|ρ| 2 • |H|), the function (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. 7. Graph G is not u.p. in the general case: see Fig. 8 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 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. 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. Computing possible delays between any two states along ρ can be achieved by repeating the above procedure starting from the first |u| + |v| states of ρ

  |ϕ U [a,b] ψ| = |ϕ| + 1 + |a| + |b| + |ψ| assuming binary notation for a and b (and |∞| = 1).

Fig. 2 .

 2 Fig. 2. The region path ρ

Fig. 3 .

 3 Fig. 3. Encoding a Turing Machine for MITL

Fig. 5 .

 5 Fig. 5. Encoding QBF for TCTL model checking along a zone path

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

t ≤ 1 tFig. 7 .

 17 Fig. 7. Automaton T 1

Fig. 8 .

 8 Fig. 8. Computation of possible delays between regions

  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 α, except the region where all clocks are larger than M , has exactly one time-successor, which we will denote by succ(α) in the sequel[START_REF] Alur | Model-checking in dense real-time[END_REF]. A clock region α is a boundary class if for any valuation v ∈ α and for any positive real t, valuation v + t is not in α.

	This obviously defines an equivalence relation. A clock region is an equivalence
	class of this equivalence relation over the set of clock valuations. In [1], Alur
	and Dill prove that there are finitely many clock regions, more precisely at
	most |H|! • 4 |H| • (M + 1) |H| .
	A clock region α is a time-successor of a clock region β if for each valuation
	v ∈ β,

  8(c)). Any intermediate value is a possible delay thanks to Lemma 29. Computing this table takes time O(|u| + 2(|H| + 1) • |v|).

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 because 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 symbolically about the periodic part.

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 obtained 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 28 Let ρ = (ρ i ) 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, called the offset, 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 29 Given a region path ρ and two integers k and l, delay(ρ, k, l) is an interval. PROOF. Let d and d ′ be two possible delays between ρ k and ρ l along ρ. According to the definition, let τ = (p j , v j , I j ) j , τ ′ = (p j , v ′ j , I ′ j ) j be the respective concretizations for d and d ′ , and t and t ′ be their respective offsets.

j and I ′′ j is obtained from I j by replacing l(I j ) and r(I j ) with λl(I j ) + (1λ)l(I ′ j ) and λr(I j ) + (1λ)r(I ′ j ), respectively. We also define

We claim that τ ′′ and t ′′ witness the fact that d ′′ ∈ delay(ρ, k, l):

• τ ′′ is a timed path: indeed, (I ′′ k ) satisfies the requirements of Definition 1, since I k and I ′ k do. Valuation v ′′ j fulfills the "continuity" condition for clocks that are not reset: If a clock x is reset when entering a given region ρ n , then v n (x) and v ′ n (x) both equal 0, and so does v ′′ n (x). • τ ′′ is compatible with ρ, by convexity of regions, and since τ and τ ′ are;

(since removing longer prefixes gives rise to the same paths), thus in total time O((|u|

Theorem 32 Model checking a TCTL formula ϕ along an u.p. region path ρ can be done in polynomial time (more precisely in time O(|ϕ|

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].

The algorithm consists in recursively applying the following rules:

• Obvious rules when ψ is an atomic proposition or a boolean combination of already labeled subformulas; If I is unbounded, for instance I = [k, +∞), we consider the earliest (if any) region labeled with ξ and whose possible delays contain a value larger than or equal to k. We label ρ i with ψ iff such a region exists and all intermediate regions are labeled with ζ.

• if ψ = E G I ζ, where I is bounded and its lower bound is 0: We consider the example where I = (0, p), the other cases being similar. We look for the earliest region ρ j whose possible delays from ρ i contains p. It is necessary and sufficient that all regions between ρ i+1 and ρ j-1 satisfy ζ for ρ i to satisfy E G (0,p) ζ.

If I is bounded but the lower bound is not 0, for instance with I = (q, p), we replace

easy, since it is equivalent to verifying that all future states, except possibly the current one, satisfy ζ, and that there exists a non-zeno path.

These modalities are sufficient for handling other TCTL modalities. For instance, A (ζ U (p,q] ξ) is equivalent to A F (p,q] ξ ∧ A G [0,p] (ζ ∧ ¬E (¬ξ U (0,∞) (¬ζ ∧ ¬ξ))).