S Lawomir Lasota

Alternating Timed Automata

Keywords: F.1.2 [Theory of Computation]: Modes of Computation-Alternation and nondeterminism; F.4.3 [Theory of Computation]: Formal Languages-Decision problems Languages, Theory Alternation, timed automata, emptyness problem

A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages which is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is non-primitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock. We investigate extension of the model with epsilon-transitions and prove that emptiness is undecidable. Over infinite words, we show undecidability of the universality problem.

INTRODUCTION

Timed automata is a widely studied model of real-time systems. It is obtained from finite nondeterministic automata by adding clocks which can be reset and whose values can be compared with constants. In this paper we consider alternating version of timed automata obtained by introducing universal transitions in the same way as it is done for standard nondeterministic automata. From the results of Alur and Dill [START_REF] Alur | A theory of timed automata[END_REF] it follows that such a model cannot have decidable emptiness problem as the universality problem for timed automata is not decidable. In the recent paper [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF] Ouaknine and Worrell has shown that the universality problem is decidable for nondeterministic automata with one Author's addresses: S lawomir Lasota, Institute of Informatics, Warsaw University, Banacha 2, 02-097 Warszawa Igor Walukiewicz, LaBRI, Université Bordeaux-1, 351, Cours de la Libération, F-33 405, Talence cedex, France Work reported here has been partially supported by the European Community Research Training Network Games. The first author has been partially supported by the Polish Kbn grant No. 4 T11C 042 25. Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. c 2006 ACM 1529-3785/06/0900-0001 $5.00 clock, over finite timed words. Inspired by their construction, we show that the emptiness problem for alternating timed automata with one clock is decidable as well. We also prove not primitive recursive lower bound for the problem. The proof implies the same bound for the universality problem for nondeterministic timed automata with one clock, thereby answering the question posed by Ouaknine and Worrell [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF]. To complete the picture we also show that an extension of our model with -transitions has undecidable emptiness problem. Furthermore, we prove undecidability of the universality problem for one-clock nondeterministic automata over infinite timed words.

The crucial property of timed automata models is the decidability of the emptiness problem. The drawback of the model is that the class of languages recognized by timed automata is not closed under complement and the universality question is undecidable (Π 1 1 -hard) [START_REF] Alur | A theory of timed automata[END_REF]. One solution to this problem is to restrict to deterministic timed automata. Another, is to restrict the reset operation; this gives the event-clock automata model [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF]. A different ad-hoc solution could be to take the boolean closure of the languages recognized by timed automata. This solution does not seem promising due to the complexity of the universality problem. This consideration leads to the idea of using automata with one clock for which the universality problem is decidable. The obtained class of alternating timed automata is by definition closed under boolean operations. Moreover, using the method of Ouaknine and Worrell, we can show that the class has decidable emptiness problem. As it can be expected, there are languages recognizable by timed automata that are not recognizable by alternating timed automata with one clock. More interestingly, the converse is also true: there are languages recognizable by alternating timed automata with one clock that are not recognizable by nondeterministic timed automata with any number of clocks.

Once the decidability of the emptiness problem for alternating timed automata with one clock is shown, the next natural question is the complexity of the problem. We show a non-primitive recursive lower bound. For this we give a reduction of the reachability problem for lossy channel systems [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]]. The reduction shows that the lower bound holds also for purely universal alternating timed automata. This implies non-primitive recursive lower bound for the universality problem for nondeterministic timed automata with one clock. We also point out that allowing -transitions in our model permits to code perfect channel systems and hence makes the emptiness problem undecidable.

All this applies to automata over finite timed words. In the case of infinite words, we prove undecidability of the universality problem of nondeterministic automata with one clock, by the reduction of the halting problem. This immediately implies undecidability of the emptiness problem for alternating one-clock automata.

Related work. Our work is strongly inspired by the results of Ouaknine and Worrell [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF]. Techniques similar to our decidability proof and to insights of [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF] have been developed eariler in [START_REF] Abdulla | Veryfying networks of timed processes[END_REF]2001].

Except for [START_REF] Dickhöfer | Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem[END_REF], it seems that the notion of alternation in the context of timed automata was not studied before. The reason was probably undecidability of the universality problem. The alternating automata introduced Alternating Timed Automata • 3 in [START_REF] Dickhöfer | Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem[END_REF] run over infinite timed trees and were used to show decidability of model checking for TCTL. Emptiness for these automata is apparently undecidable, even under one-clock restriction, in view of our result for one-clock automata over infinite words. On the other hand, emptiness for nondeterministic timed tree automata is decidable [START_REF] Torre | Timed tree automata with an application to temporal logic[END_REF].

Some research (see [START_REF] Asarin | Controller synthesis for timed automata[END_REF][START_REF] Cassez | A comparison of control problems for timed and hybrid systems[END_REF][START_REF] Bouyer | Timed control with partial observability[END_REF][START_REF] Alur | Optimal reachability for weighted timed games[END_REF][START_REF] Bouyer | Optimal strategies in priced timed game automata[END_REF]] and references within) was devoted to the control problem in the timed case. While in this case one also needs to deal with some universal branching, these works do not seem to have direct connection to our setting.

Furthermore, let us mention that restrictions to one clock (and two clocks) have been already considered in the context of TCTL model-checking of timed systems [START_REF] Dima | Real-time automata and the Kleene algebra of sets of real numbers[END_REF][START_REF] Laroussinie | Model checking timed automata with one or two clocks[END_REF]], leading to a lower complexity in some cases. Finally, in [START_REF] Alur | Parametric real-time reasoning[END_REF]] the parametric variant of emptiness problem was shown decidable under restriction to one clock (similarly as in our setting) and undecidable for three clocks; the two-clock case is left as an open question.

Similar results to ours were obtained independently by Ouaknine and Worrell [START_REF] Ouaknine | On the decidability of metric temporal logic[END_REF] and by Abdulla et al [START_REF] Abdulla | Decidability and complexity results for timed automata via channel machines[END_REF]]. The former paper defines alternating timed automata, in a slightly different way than ours, and applies these automata to prove decidability of model-checking for Metric Temporal Logic. The non-primitive recursive lower bound is also established. In the latter paper, the undecidability result for the universality problem over infinite words is proved.

Organization of the paper. In the next section we define alternating timed automata; we discuss their basic properties and relations with nondeterministic timed automata. In Section 3 we show decidability of the emptiness problem for alternating timed automata with one clock. In the following two sections we show a non-primitive recursive lower bound for the problem, and then the undecidability result for an extension of our model with -moves. In Section 6 we investigate automata over infinite words.

A preliminary version of this article appeared as [START_REF] Lasota | Alternating timed automata[END_REF].

ALTERNATING TIMED AUTOMATA

In this section we introduce the alternating timed automata model and study its basic properties. The model is a quite straightforward extension of the nondeterministic model. Nevertheless some care is needed to have the desirable feature that complementation corresponds to exchanging existential and universal branchings (and final and non-final states). As can be expected, alternating timed automata can recognize more languages than their nondeterministic counterparts. The price to pay for this is that the emptiness problem becomes undecidable, in contrast to timed automata [START_REF] Alur | A theory of timed automata[END_REF]. This motivates the restriction to automata with one clock. With one clock alternating automata can still recognize languages not recognizable by nondeterministic automata and moreover, as we show in the next section, they have decidable emptiness problem. For a given finite set C of clock variables (or clocks in short), consider the set Φ(C) of clock constraints σ defined by

σ ::= x < c | x ≤ c | σ 1 ∧ σ 2 | ¬σ,
where c stands for an arbitrary nonnegative integer constant, and x ∈ C. For instance, note that tt (always true), or x = c, can be defined as abbreviations.

Each constraint σ denotes a subset [σ] of (R + ) C , in a natural way, where R + stands for the set of nonnegative reals.

Transition relation of a timed automaton [START_REF] Alur | A theory of timed automata[END_REF] is usually defined by a finite set of rules δ of the form

δ ⊆ Q × Σ × Φ(C) × Q × P(C),
where Q is a set of locations (control states) and Σ is an input alphabet. A rule q, a, σ, q , r ∈ δ means, roughly, that when in a location q, if the next input letter is a and the constraint σ is satisfied by the current valuation of clock variables, the next location can be q and the clocks in r should be reset to 0. Our definition below uses an easy observation, that the relation δ can be suitably rearranged into a finite partial function

Q × Σ × Φ(C) • → P(Q × P(C)).
The definition below comes naturally when one thinks of an element of the codomain as a disjunction of a finite number of pairs (q, r). Let B + (X) denote the set of all positive boolean formulas over the set X of propositions, i.e., the set generated by:

φ ::= X | φ 1 ∧ φ 2 | φ 1 ∨ φ 2 .
Definition 2.1 Alternating timed automaton. An alternating timed automaton is a tuple A = (Q, q 0 , Σ, C, F, δ) where: Q is a finite set of locations, Σ is a finite input alphabet, C is a finite set of clock variables, and δ :

Q × Σ × Φ(C) • → B + (Q × P(C))
is a finite partial function. Moreover q 0 ∈ Q is an initial state and F ⊆ Q is a set of accepting states. We also put an additional restriction:

(Partition). For every q and a, the set {[σ] : δ(q, a, σ) is defined} gives a (finite) partition of (R + ) C . The (Partition) condition does not limit the expressive power of automata. We impose it because it permits to give a nice symmetric semantic for the automata as explained below. We will often write rules of the automaton in a form: q, a, σ → b.

By a timed word over Σ we mean a finite sequence

w = (a 1 , t 1 )(a 2 , t 2 ) . . . (a n , t n ) (1)
of pairs from Σ × R + . Each t i describes the amount of time that passed between reading a i-1 and a i , i.e., a 1 was read at time t 1 , a 2 was read at time t 1 +t 2 , and so on.

In Sections 4 and 5 it will be more convenient to use an alternative representation where t i denotes the time elapsed since the beginning of the word. In this paper we deal with finite timed words, except Section 6, where we will investigate timed ω-words.

To define an execution of an automaton, we will need two operations on valuations v ∈ (R + ) C . A valuation v+t, for t ∈ R + , is obtained from v by augmenting value

• 5 of each clock by t. A valuation v[r := 0], for r ⊆ C, is obtained by reseting values of all clocks in r to zero.

For an alternating timed automaton A and a timed word w as in (1), we define the acceptance game G A,w between two players Adam and Eve. Intuitively, the objective of Eve is to accept w, while the aim of Adam is the opposite. A play starts at the initial configuration (q 0 , v 0 ), where v 0 : C → R + is a valuation assigning 0 to each clock variable. It consists of n phases. The (k+1)-th phase starts in (q k , v k ), ends in some configuration (q k+1 , v k+1 ) and proceeds as follows. Let v := v k +t k+1 . Let σ be the unique constraint such that v satisfies σ and b = δ(q k , a k+1 , σ) is defined. Existence and uniqueness of such σ is implied by the (Partition) condition. Now the outcome of the phase is determined by the formula b. There are three cases:

-b = b 1 ∧ b 2 : Adam chooses one of subformulas b 1 , b 2 and the play continues with b replaced by the chosen subformula; -b = b 1 ∨ b 2 : dually, Eve chooses one of subformulas; -b = (q, r) ∈ Q×P(C): the phase ends with the result (q k+1 , v k+1 ) := (q, v[r := 0]).

A new phase is starting from this configuration if k+1 < n.

The winner is Eve if q n is accepting (q n ∈ F ), otherwise Adam wins. Formally, a play is a finite sequence of consecutive game positions of the form k, q, v or k, q, b , where k is the phase number, b a boolean formula, q a location and v a valuation. A strategy of Eve is a mapping which assigns to each such sequence ending in Eve's position a next move of Eve. A strategy is winning if Eve wins whenever she applies this strategy. Definition 2.2 Acceptance. The automaton A accepts w iff Eve has a winning strategy in the game G A,w . By L(A) we denote the language of all timed words w accepted by A.

To show the power of alternation we give an example of an automaton for a language not recognizable by standard (i.e. nondeterministic) timed automata (cf. [START_REF] Alur | A theory of timed automata[END_REF]).

Example 2.3. Consider a language consisting of timed words w over a singleton alphabet {a} that contain no pair of letters such that one of them is precisely one time unit later than the other. The alternating automaton for this language has three states q 0 , q 1 , q 2 . State q 0 is initial. The automaton has a single clock x and the following transition rules:

q 0 , a, tt → (q 0 , ∅) ∧ (q 1 , {x}) q 1 , a, x=1 → (q 2 , ∅) q 1 , a, x =1 → (q 1 , ∅) q 2 ,
a, tt → (q 2 , ∅) States q 0 and q 1 are accepting, q 2 is not. In state q 0 , at each input letter, Adam chooses either to stay in q 0 either to to go to q 1 ; In the latter case clock x is reset. Furthermore, the automaton can only quit state q 1 exactly one time unit after entering it. Hence, Adam has a strategy to reach q 2 iff the word is not in the language, i.e., some letter is one time unit after some other.

As one expects, we have the following:

Proposition 2.4. The class of languages accepted by alternating timed automata is effectively closed under all boolean operations: union, intersection and complementation. These operations do not increase the number of clocks of the automaton.

The closure under conjunction and disjunction is straightforward since we permit positive boolean expressions as values of the transition function. Due to the condition (Partition) the automaton ¬A for the complement is obtained from A by exchanging conjunctions with disjunctions in all transitions and exchanging accepting states with non-accepting states.

Definition 2.5. An alternating timed automaton A is called purely universal if the disjunction does not appear in the transition rules δ. Dually, A is purely existential if no conjunction appears in δ.

Clearly, if A is purely universal (purely existential) then ¬A is purely existential (purely universal). It is obvious that every purely existential automaton is a standard nondeterministic timed automaton. The converse requires a proof because of the (Partition) condition.

Proposition 2.6. Every standard nondeterministic automaton is equivalent to a purely existential automaton.

Proof. Transition relation of a nondeterministic timed automaton is usually defined by a finite set δ of rules of the form q, a, σ, q , r ∈ Q × Σ × Φ(C) × Q × P(C). Given such an automaton A, the corresponding purely existential alternating automaton A has the same set Q of states as A, plus one additional state q sink . Automaton A has the same initial state and accepting states as A, the same set of clocks C, and the same input alphabet. The only essential difference is that δ is replaced by δ :

Q × Σ × Φ(C) • → B + (Q × P(C))
, defined as follows.

In fact, we prefer to define δ equivalently as δ :

Q × Σ × Φ(C) • → P(Q × P(C)).
Let σ 1 . . . σ n be all clock constraints appearing in δ. The guards appearing in δ will be σ X , for X ⊆ {1 . . . n}, defined by:

σ X = ∧ i∈X σ i ∧ ∧ i /
∈X ¬σ i . I.e., we consider conjunctions of arbitrary sets of guards σ i . The value δ(q, a, σ) is defined iff σ = σ X for some X, hence δ clearly satisfies the (Partition) condition. The constraints σ X satisfying [σ X ] = ∅ can be safely omitted. We put: δ(q, a, σ X ) = {(q , r) : q, a, σ i , q , r ∈ δ for some i ∈ X}.

If δ(q, a, σ X ) is empty, we put δ(q, a, σ X ) = {(q sink , ∅)}. And finally we put: δ(q sink , a, σ X ) = {(q sink , ∅)}, for any a and σ X .

It is routine now to check that languages accepted by A and A coincide.

In the following sections, we consider emptiness, universality and containment for different classes of alternating timed automata. For clarity, we recall definitions here.

Definition 2.7. For a class C of automata we consider three problems:

-Emptiness: given A ∈ C is L(A) empty.
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006.

Alternating Timed Automata

• 7 -Universality: given A ∈ C does L(A) contain all timed words.

-Containment: given A, B ∈ C does L(A) ⊆ L(B).

It is well known that the universality is undecidable for non-deterministic timed automata [START_REF] Alur | A theory of timed automata[END_REF] with at least two clocks. As a consequence, all three problems are undecidable for alternating timed automata with two clocks. This is why, in the rest of the paper, we focus on automata with one clock only. Proviso:. In the following all automata have one clock.

The automaton from Example 2.3 uses only one clock. This shows that one clock alternating automata can recognize some languages not recognizable by nondeterministic automata with many clocks. The converse is also true:

Theorem 2.8. Classes of languages recognizable by nondeterministic timed automata and by one-clock alternating timed automata are incomparable.

Proof. We show a language acceptable by a deterministic automaton with many clocks but not acceptable by an alternating automaton with one clock.

Consider the timed language over the singleton alphabet {b} consisting of the words containing appearances of the letter b at times t 1 and t 2 , where 0 < t 1 < t 2 < 1, no other b in between 0 and 1 and precisely one b between t 1 + 1 and t 2 + 1. We will show that this language cannot be accepted by an alternating timed automaton with one clock. Obviously it is accepted by a deterministic timed automaton with two clocks.

For a preparation consider a deterministic untimed automaton

B. A sequence b k of k letters b determines a function f B k : Q B → Q B saying
that if started in the state q after reading b k the automaton will end in f B k (q). Clearly the number of such functions is bounded if the number of states is fixed. Thus there are m and l, depending only on the number of states, such that

f B m = f B m+l . Moreover f B m+i = f B
m+l+i for all i > 0. To arrive at a contradiction assume that our language is recognized by an ATA A with n states. Suppose for a moment that all constants in the tests in transition function of the automaton are integers. Let m and l be such that f B m+i = f B m+l+i for all i > 0 and for all deterministic automata B with at most 2 2 2n states. Now consider two words w 1 and w 2 . In w 1 we have b at times 0.3, 0.7, 1.5 and m b's somewhere in the interval (1, 1.3) as well as m b's somewhere in the interval (1.7, 2). Word w 2 is obtained from w 1 by adding l b's somewhere in the interval (1.3, 1.7); but not at point 1.5 of course. We will show that if A accepts w 1 then it also accepts w 2 .

Consider the accepting run of A on w 1 . Look at the configurations in which the automaton reaches at time 1. Let (q, v) be one of them. The value of the clock v can be 0.3, 0.7 or 1. This is because there are only two letters till 1 and the automaton can reset clock only when it reads a letter. We will analyse the three cases one by one.

If v = 1 then it is easy to see that from a configuration (q, v) the automaton has no use for the clock in the interval (1, 2). If not reset, the value of the clock in this interval will be in (1, 2) and the automaton can compare the values only with integers. If the clock is reset then its value will stay in (0, 1) till the end of the interval. Thus from the configuration (q, v) automaton A behaves as an alternating automaton without a clock with additional flag telling whether there was a reset or not. Because it has n states, it is equivalent to a deterministic automaton of at most 2 2 2n states. We have that if it accepts from q the string of 2m + 1 letters b then it also accepts 2m + l + 1 letters b. Thus A has an accepting run from (q, v) in w 2 if it had one in w 1 .

If v = 0.7 then consider the run of A from (q, v) till the time point 1.3. Automaton A has no use of the clock till that point for the same reason as above. It arrives at a set of configurations: some with the value of the clock 1 and some with the value < 0.3. The later are possible because A could reset a clock. Consider the rest of the computation starting from a configuration (q , 1). Once again the clock will not be useful to A in the rest of the word. Hence we will arrive to the same final states on a 1+m and a 1+m+l . Similarly for all the configurations with the values of the clock < .3.

If v = 0.3 then consider the run of A from (q, v) till the time point 1.7. Till that time there was no use of the clock. We get a set of configurations with clock value 1 and the other with clock value < 0.7. The possible configurations with clock value 1 are the same no matter if we have made automaton run on w 1 or on w 2 , for the same reason as before. As the rest of w 1 is the same as the rest of w 2 we are done. On the other hand, when comparing configurations with clock value < 0.7 in runs over w 1 and w 2 , the possible locations are the same but the clock values may differ. But the clock value is irrelevant before time 2, hence again we are done.

In the argument we essentially use the assumption that we compare clocks only with natural numbers. If we allowed to compare with rationals we can get an example of the similar kind by using rescaling. Instead of intervals (0, 1) and (1, 2) we would use smaller intervals that are of the size smaller than the smallest constant used by the automaton.

More precisely, let c = 0 be the smallest positive rational such that the clock is compared in A either to c or to 1-c or to 1+c. We define words w 1 and w 2 as follows. In w 1 we have b at times 0.3c, 0.7c, 1 + 0.5c and m b's somewhere in the interval (1, 1+0.3c) as well as m b's somewhere in the interval (1+0.7c, 1+c). Word w 2 is obtained from w 1 by adding l b's somewhere in the interval (1 + 0.3c, 1 + 0.7c); but not at point 1 + 0.5c. The whole proof works unchanged.

DECIDABILITY

The main result of this section is that the emptiness problem for one-clock alternating timed automata is decidable. Due to closure under boolean operations, this implies the decidability of the universality and the containment problems.

Theorem 3.1. The emptiness problem is decidable for one-clock alternating timed automata.

Corollary 3.2. The containment problem is decidable for one-clock alternating timed automata.

The rest of this section is devoted to the proof of Theorem 3.1. Essentially, we have adapted the method of Ouaknine and Worrell [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF] • 9 for our more general setting. We point out the differences below.

Fix a one-clock alternating timed automaton A = (Q, q 0 , Σ, {x}, F, δ). For readability, assume w.l.o.g. that the boolean conditions appearing in rules of δ are all in disjunctive normal form. In terms of acceptance games this means that each phase consists of a single move of Eve followed by a single move of Adam. Consider a labelled transition system T whose states are finite sets of configurations, i.e., finite sets of pairs (q, v), where q ∈ Q and v ∈ R + . The initial position in T is P 0 = {(q 0 , 0)} and there is a transition P a,t -→ P in T iff P can be obtained from P by the following nondeterministic process:

-First, for each (q, v) ∈ P , do the following:

-let v := v+t, -let b = δ(q, a, σ) for the uniquely determined σ satisfied in v , -choose one of disjuncts of b, say

(q 1 , r 1 ) ∧ . . . ∧ (q k , r k ) (k > 0), -let Next (q,v) = {(q i , v [r i := 0]) : i = 1 . . . k}.
-Then, let P := (q,v)∈P Next (q,v) .

This construction is very similar to the translation from alternating to nondeterministic automata over (untimed) words: we just collect all universal choices in one set. Compared to [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF], the essential difference is that we have to deal with both disjunction and conjunction, while in [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF] only one of them appeared. We treat conjunction similarly to determinization in [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF]. On the other hand, we leave the existential choice, i.e., nondeterminism, essentially unaffected in T .

In what follows we will derive from T a finite-branching transition system H, suitable for the decision procedure. Like in [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF], the degree of the nodes of H will not be bounded but nevertheless finite. This is sufficient for our purposes.

A state {(q 1 , v 1 ), . . . , (q n , v n )} of T is called bad iff all control states q i are accepting (q i ∈ F ). The following proposition characterizes acceptance in A in terms of reachability of bad states in T . It is enough to consider reachability because A accepts only finite words.

Lemma 3.3. A accepts a timed word w iff there is a path in T , labelled by w, from P 0 to a bad state.

Let T be a labelled transition system obtained from T by erasing time information from transition labels, i.e., there is a transition

P a -→ Q in T iff there is P a,t -→ Q in T ,
for some t ∈ R + . Now we cannot talk about particular timed words but still we have the following: Lemma 3.4. L(A) is nonempty if and only if there is a path in T from P 0 to a bad state.

Thus, the (non)emptiness problem for A is reduced to the reachability of a bad state in T . The last difficulty is that even if each state of T is a finite set, there are uncountably many states. The following definition allows to abstract from the precise timing information in states.

Let c max denote the biggest constant appearing in constraints in δ. Let set reg of regions be a partition of R + into 2 • (c max +1) sets as follows:

reg := {{0}, (0, 1), {1}, (1, 2), . . . , (c max -1, c max ), {c max }, (c max , +∞)}.

For v ∈ R + , let reg(v) denote its region; and let fract(v) denote the fractional part of v. Below we work with finite words over the alphabet Λ = P(Q × reg) consisting of finite sets of pairs (q, r), where q ∈ Q is a control state and r ∈ reg is a region. Definition 3.5. For a state P of T we define a word H(P ) from Λ * as the one obtained by the following procedure:

-replace each (q, v) ∈ P by a triple q, reg(v), fract(v) (this yields a finite set of triples) -sort all these triples w.r.t. fract(v) (this yields a finite sequence of triples) -group together triples that have the same value of fract(v), ignoring multiple occurrences (this yields a finite sequence of finite sets of triples) -forget about fract(v), i.e., replace each triple q, reg(v), fract(v) by a pair (q, reg(v)) (this yields a finite sequence of finite sets of pairs, a word in Λ * ).

Example 3.6. To illustrate transformation H, consider P = {(q 1 , 0.5), (q 2 , 1.2), (q 3 , 2.2)}, where q 1 , q 2 , q 3 are locations.

Let c max = 2. Denote regions by r 0 = {0}, r 0,1 = (0, 1), . . . , r 2 = {2}, r 2,+∞ = (2, +∞). First, P is transformed into the set { q 1 , r 0,1 , 0.5 , q 2 , r 1,2 , 0.2 , q 3 , r 2,+∞ , 0.2 }.

We make it into a sorted sequence q 2 , r 1,2 , 0.2 q 3 , r 2,+∞ , 0.2 q 1 , r 0,1 , 0.5 . Then we group together triples with the same fractional part, obtraining a sequence of length two: { q 2 , r 1,2 , 0.2 , q 3 , r 2,+∞ , 0.2 }, { q 1 , r 0,1 , 0.5 }.

Finally we remove the fractional parts and obtain H(P ) = {(q 2 , r 1,2 ), (q 3 , r 2,+∞ )}, {(q 1 , r 0,1 )}. Definition 3.7. Let H be the transition system whose states are words H(P ) for

P a state of T ; a transition W 1 a -→ W 2 is in H if there is a transition P 1 a -→ P 2 in T with H(P 1 ) = W 1 , H(P 2 ) = W 2 . The initial state in H is W 0 = H(P 0 ).
Example 3.8. Assume that the automation from previous example has a rule:

q 3 , a, x>2 → (q 1 , x) ∨ ((q 2 , ∅) ∧ (q 3 , ∅)).
Imagine a transition P a -→ P in T corresponding to P a,0.6 -→ P in T derived from the above rule. There are two possibilities: P = {(q 1 , 1.1), (q 2 , 1.8), (q 1 , 0)} or P = {(q 1 , 1.1), (q 2 , 1.8), (q 2 , 2.8), (q 3 , 2.8)}. Accordingly, there are two transitions

H(P ) a -→ W in H, for W = {(q 1 , r 0 )}{(q 1 , r 1,2 )}{(q 2 , r 1,2 )} or W = {(q 1 , r 1,2 )}{(q 2 ,
r 1,2 ), (q 2 , r 2,+∞ ), (q 3 , r 2,+∞ )}. In each case W = H(P ). Hence, ACM Transactions on Computational Logic, Vol. V, No. N, September 2006.

Alternating Timed Automata

• 11 transitions in H can "simulate" transitions in T . On the other hand, H(P ) has also a transition H(P ) -→ {(q 1 , r 0 )}{(q 1 , r 1,2 )}{(q 2 , r 1,2 ), (q 2 , r 2,+∞ ), (q 3 , r 2,+∞ )} that simulates a posible transition of P = {(q 1 , 0.5), (q 2 , 1.2), (q 3 , 2.2), (q 3 , 6.2)}. Hence, roughly speaking, transitions of H(P ) correspond to the union of all the transitions of all P such that H( P ) = H(P ).

If P is bad and H(P ) = H(P ) then P is bad as well. Hence it is correct to call a state W in H bad if W = H(P ) for a bad state P . Lemma 3.9. L(A) is nonempty iff a bad state is reachable in H from W 0 .

Proof. By Lemma 3.4 we only need to show: a bad state is reachable in T from P 0 iff a bad state is reachable in H from W 0 . Consider a transition system T obtained from T by imposing one additional restriction on transitions: whenever v 1 and v 2 are in the same region, then Next (q,v1) = Next (q,v2) . By T and H denote the transition systems obtained from T instead of T . They have the same states as T and H, respectively, but fewer transitions. Clearly, the additional restriction has no impact on acceptance, i.e., on reachability of a bad state. Hence we have: a bad state is reachable in T from P 0 iff a bad state is reachable in T from P 0 . And also: a bad state is reachable in H from W 0 iff a bad state is reachable in H from W 0 . Now observe that the graph of H, i.e., the set of all pairs (P, H(P )), is a bisimulation between T and H . If P a -→ P then obviously H(P ) a -→ H(P ). If H(P ) a -→ W then there exists P such that P a -→ P and H(P ) = W ; we only need to guess appropriate t and derive P from transition P a,t -→ P in T (clearly t need not be unique).

The bisimulation guarantees that a bad state is reachable in T from P 0 iff a bad state is reachable in H from W 0 . This completes the proof.

At this point, we have reduced emptiness of L(A) to the reachability of a bad state in a countably infinite transition system H. The rest of the proof is quite standard [START_REF] Abdulla | General decidability theorems for infinite state systems[END_REF][START_REF] Finkel | Well structured transition systems everywhere! Theoretical Computer[END_REF]] and exploits the fact that one can put an appropriate well-quasi-order (wqo in short) on states of H. Unfortunately, we are obliged to redo the proofs as we could not find a theorem that fits precisely our setting.

i ≤ n, a i ⊆ b f (i) .
Lemma 3.11 [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF]]. Relation is a wqo, i.e., for arbitrary infinite sequence W 1 , W 2 , . . . of words over Λ, there exist indexes i < j such that W i W j .

The decision procedure for reachability of bad states will work by an exhaustive search through a sufficiently large portion of the whole reachability tree. Thus we need to know that an arbitrarily large part of that tree can be effectively constructed. Roughly, all time delays of an action a from W can be captured by a finite number of cyclic shifts of W with an appropriate change of region.

Lemma 3.12. For each state W in H, its set of successors {W ∈ Λ * : W a -→ W for some a} is finite and effectively computable.

Proof. Recall that a word W represents a finite set of pairs (q, v). The letters are sorted according to the value of fract(v); moreover the letters represent finite sets of pairs in fact, i.e., all the pairs with the same fract(v). Note that all pairs with fract(v) = 0, if any, are represented by the first letter of W ; and the corresponding region is of the form {i} (or (c max , ∞)) in this case. Now imagine a transition W a -→ W in H. This corresponds to some transition P a,t -→ P in T , for some t and some chosen set P of pairs (q, v). Importantly, the same time delay t is applied to all the pairs (q, v). Denote by P the set obtained from P by time delay, i.e., by replacing each (q, v) with (q, v + t); consider this, conceptually, for all t > 0. The corresponding word W in H is obtained from W by an operation similar to a cyclic shift, to the right, repeated as many times as needed. This operation modifies W as follows. Note that the first letter of W contains either only pairs of the form (q, {i}), either only the pairs of the form (q, (i, i + 1)) (and perhaps (c max , ∞) as well). In the first case, change each region {i} in the first letter of W to (i, i + 1) (or to (c max , ∞), if i = c max ). In the second case, remove the right-most letter and put it as the first letter in the word, and change each region (i, i + 1) to {i + 1}.

Hence, the set {W ∈ Λ * : W a -→ W for some a} can be computed by applying the operation defined above an arbitrary number of times (until all regions are (c max , ∞)), yielding W ; and by calculating the effect of performing any transition a from W .

The following observation is proved in the same way as Lemma 15 in [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF].

Lemma 3.13. The inverse of relation is a simulation: whenever

W 1 W 2 and W 2 a -→ W 2 , there is some W 1 such that W 1 a -→ W 1 and W 1 W 2 . Proof. Take W 1 W 2 and suppose W 2 a -→ W 2 .
By definition it means that there is P 2 with H(P 2 ) = W 2 such that there is a transition P 2 a -→ P 2 and H(P 2 ) = W 2 . Since W 1 W 2 it is easy to see that there is P 1 ⊆ P 2 such that W = H(P 1 ); P 1 is obtained by removing from P 2 the pairs that do not end up in W 1 when construction H is applied (cf. Definition 3.5). Now, directly from the definition of the transition system T we have P 1 a -→ P 1 with P 1 ⊆ P 2 . So W 1 a -→ H(P 1 ). As P 1 ⊆ P 2 , we have H(P 1 ) W 2 as required.

The next observation is more specific to our setting but fortunately very easy.

Lemma 3.14 Downward closedness of badness. Whenever W W and W is bad then W is bad as well.

ACM Transactions on Computational Logic, Vol. V, No. N, September 2006.

Alternating Timed Automata

• 13

Proof. Take a letter w i of W . We need to show that q ∈ F for every (q, r) ∈ w i . By the definition of W W we have w i ⊆ w j for some letter w j of W . Hence, (q, r) ∈ w j and q ∈ F as W is bad. Now we are ready to prove the main lemma.

Lemma 3.15. It is decidable whether a bad state is reachable in H from W 0 .

Proof. The reachability tree is the unravelling of H from W 0 . The algorithm constructs a portion t of the tree conforming to the following rule: do not add a node W to t in a situation when among its ancestors there is some W W . Lemma 3.11 guarantees that each path in t is finite. Furthermore, since the degree of each node is finite, t is a finite tree.

We need only to prove that if a bad state is reachable in H from W 0 then t contains at least one bad state. Let W be such a bad state reachable from W 0 in H by a path π of the shortest length. Assume that W is not in t, i.e., there are two other nodes in π, say W 1 and W 2 such that W 1 is an ancestor of W 2 in the reachability tree and W 1 W 2 (i.e., W 2 was not added into t). Since the inverse of is a simulation by Lemma 3.13, the sequence of transitions in π from W 2 to W can be imitated by the corresponding sequence of transitions from W 1 to some other W W . W is bad as well by Lemma 3.14. Moreover, the path leading to W is strictly shorter than π, a contradiction. Theorem 3.1 follows immediately from Lemma 3.15 and Lemma 3.9.

Remark:. In fact, Ouaknine and Worrell showed decidability of containment " L(A) ⊆ L(B)" in a slightly more general case, namely when automaton A has arbitrarily many clocks. Along the same lines one can adapt our proof, assumed that A is an arbitrary nondeterministic timed automaton and B is a one-clock alternating timed automaton. We sketch below the necessary modifications.

If we denote by B a dual of B, i.e., an automaton accepting the complement of L(B), then the containment reduces to emptiness of L(A) ∩ L( B). Compared to the proof above, each state P of T needs to contain additionally information on a configuration of A. Due to the fact that A is purely existential, P will contain precisely one pair (q, v), where q is a state of A and v a valuation of all its clocks. The transition relation P a,t -→ P is adapted so that the delay t before performing an action a is the same in A and B. This guarantees that the facts analogous to Lemma 3.3 and 3.4 hold; but now a state P is bad iff all states of both A and B appearing in P are accepting.

Definition of H is precisely as before, but it needs a preprocessing: the pair (q, v) corresponding to A is split into a number of triples (q, v x , x), one for each clock x of A. The triples are identical on the first component, and v x is the value of clock x. Observe that the number of such triples is the same in each state of H, and equal to the number of clocks in A. An analog of Lemma 3.9 holds: L(A) ∩ L( B) is nonempty iff a bad state is reachable in H.

Finally, Lemma 3.12 and 3.14 hold as well, and the proofs are similar. The proofs of Lemma 3.13 and 3.15 rest unchanged.

• S. Lasota and I. Walukiewicz

LOWER BOUND

In this section we prove the following lower bound result.

Theorem 4.1. The complexity of the emptiness problem for one-clock purely universal alternating timed automata is not bounded by a primitive recursive function.

Since emptiness and universality are dual in the setting of alternating automata, as a direct conclusion we get the following:

Corollary 4.2. The complexity of the universality problem for one-clock purely existential alternating (i.e., nondeterministic) timed automata is not bounded by a primitive recursive function.

This answers the question posed by Ouaknine and Worrell [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF].

The rest of this section contains the proof of Theorem 4.1. The proof is a reduction of the reachability problem for lossy one-channel systems [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]].

Definition 4.3 Channel system. A channel system is given by a tuple S = (Q, q 0 , Σ, ∆), where Q is a finite set of control states,

q 0 ∈ Q is an initial state, Σ is a finite channel alphabet and ∆ ⊆ Q × ({!a : a∈Σ} ∪ {?a : a∈Σ} ∪ { }) × Q is a finite set of transition rules.
A configuration of S is a pair (q, w) of a control state q and a channel content w ∈ Σ * . Transition rules allow the system to pass from one configuration to another. In particular, a rule q, !a, q allows in a state q to write to the channel and to pass to the new state q . Similarly, q, ?a, q means reading from a channel and is allowed in state q only when a is at the end of the channel. The channel is a FIFO, and by convention S writes at the beginning and reads at the end. Finally, a rule q, , q allows for a silent change of control state, without reading or writing.

Formally, there is a (perfect) transition (q, w) γ -→ (q , w ) if one of the following conditions is satisfied:

-γ = q, , q and w = w , or -γ = q, !a, q for some a∈Σ, and w = aw, or -γ = q, ?a, q for some a∈Σ, and w = w a.

The initial configuration is (q 0 , ), i.e., execution of S starts with the empty channel. For technical convenience, we assume w.l.o.g. that there is no rule returning back to the initial state: for each rule q, x, q ∈ ∆, q = q 0 . A lossy channel system differs from the perfect one in only one respect: during the transition step, an arbitrary number of messages stored in the channel may be lost. To define lossy transitions, we need the subsequence ordering on Σ * , denoted by (e.g., tata atlanta). We say that there is a lossy transition from (q, w) to (q , w ), denoted by (q, w) γ =⇒ (q , w ), iff there exists u, u ∈ Σ * such that u w, (q, u) γ -→ (q , u ) and w u . By a lossy computation of a channel system S we mean a finite sequence:

(q 0 , ) γ1 =⇒ (q 1 , w 1 ) γ2 =⇒ (q 2 , w 2 ) . . . γn =⇒ (q n , w n ).
(2)

ACM Transactions on Computational Logic, Vol. V, No. N, September 2006.

Alternating Timed Automata

• 15

Definition 4.4. Lossy reachability problem for channel systems is: given a channel system S and a configuration (q f , w f ), with q f =q 0 , decide whether there is a lossy computation of S ending in (q f , w f ).

Theorem 4.5 [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]]. The lossy reachability problem for channel systems has non-primitive recursive complexity.

The result of [START_REF] Schnoebelen | Verifying lossy channel systems has nonprimitive recursive complexity[END_REF]] was showed for a slightly different model. Namely, during a single transition, a finite sequence of messages was allowed to be read or written to the channel. Clearly, reachability problems in both models are polynomial-time equivalent.

In the sequel we describe a reduction from the lossy reachability for channel systems to the emptiness problem for one-clock purely universal alternating timed automata. Given a channel system S = (Q, q 0 , Σ, ∆), and a configuration (q f , w f ), we effectively construct a purely universal automaton A with a single clock x, and the input alphabet Σ = Q ∪ Σ ∪ ∆. The construction will assure that A accepts precisely correct encodings of lossy computations of S ending in (q f , w f ). A computation as in (2) will be encoded as the following word over Σ:

q n γ n w n q n-1 γ n-1 w n-1 . . . q 1 γ 1 w 1 q 0 , ( 3
)
where

q i ∈ Q, γ i ∈ ∆, w i ∈ Σ * .
Let S be fixed in this section.

It will be convenient here to write timed words in a slightly different way than before. From now on, whenever we write a word w = (a 1 , t 1 )(a 2 , t 2 ) . . . (a n , t n ) we mean that the letter a i appeared t i time units after the beginning of the word. In particular, a i+1 appeared t i+1t i time units after a i . Clearly this is correct only when t i+1 ≥ t i , for i = 1 . . . n-1.

Before the formal definition of encoding of a computation by a timed word we outline shortly the underlying intuition. We will require that the letter q n appears at time 0 and then that each letter q i appears at time ni. Hence, each configuration will be placed in a unit interval. To ensure consistency of the channel contents at consecutive configurations we require that if a message survived during a step i (it was neither read nor written nor lost) then the distance in time between its appearances in the sequences w i and w i-1 should be precisely 1.

We will need a new piece of notation : by (w + 1) we mean the word obtained from w by increasing all t i by one time unit, i.e., (w + 1) = (a 1 , t 1 + 1)(a 2 , t 2 + 1) . . . (a n , t n + 1). Definition 4.6. By a lossy computation encoding ending in (q f , w f ) we mean any timed word over Σ of the form:

(q n , t n )(γ n , t n )v n (q n-1 , t n-1 )(γ n-1 , t n-1 )v n-1 . . . (q 1 , t 1 )(γ 1 , t 1 )v 1 (q 0 , t 0 ), where each v i = (a 1 i , u 1 i ) . . . (a li i , u li i
) is a timed word over Σ. Additionally we require that for each i ≤ n and j = 1, . . . , l i , the following conditions hold: (P1). Structure:

q i ∈ Q, γ i ∈ ∆, a j i ∈ Σ, γ i = q i-1 , x, q i , q n = q f and a 1 n . . . a ln n = w f . (P2). Distribution in time: n-i = t i < t i < u 1 i < u 2 i < . . . < u li i < t i+1 = n-i+1.
• S. Lasota and I. Walukiewicz (P3a). Epsilon move: if

γ i = q i-1 , , q i then (v i + 1) v i-1 . (P3b). Write move: if γ i = q i-1 , !a, q i then either v i = (a, u 1 i )v and v + 1 v i-1 , or (v i + 1) v i-1 .
(P3c). Read move: if γ i = q i-1 , ?a, q i then v i-1 = v (a, t)v for some timed words v , v and t ∈ R + , such that (v i + 1) v .

Lemma 4.7. S has a computation of the form (2) ending in (q n , w n ) = (q f , w f ) if and only if there exists a lossy computation encoding ending in (q f , w f ) as in Definition 4.6.

Our aim is:

Lemma 4.8. A purely universal automaton A can be effectively constructed such that L(A) contains precisely all lossy computation encodings ending in (q f , w f ).

The proof of this lemma will occupy the rest of this section. Automaton A will be defined as a conjunction of four automata, each responsible for some of the conditions from Definition 4.6:

A := A struct ∧ A unit ∧ A strict ∧ A check .
All four automata will be purely universal and will use at most one clock. Automaton A struct verifies condition (P1), automata A unit and A strict jointly check condition (P2), and A check enforces the most involved conditions (P3a) -( P3c).

We omit an obvious definition of A struct . We also omit the construction of the automaton A unit checking that letters from Q appear precisely at times 0, 1, . . . , n. Automaton A strict will accept a timed word iff the first letter is at time 0 and no two consecutive letters appear at the same time. This can be easily achieved by the following rules:

s 0 , Σ, x = 0 → (s, ∅) s, Σ, x > 0 → (s, {x}).
with s 0 an initial state and both s 0 , s as accepting ones. For readability of notation, when no clock is reset, as in the first rule above, we will omit writing it explicitly. Moreover, for conciseness, we implicitly assume that the automaton fails to accept from a state, if no rule is applicable in that state.

The above mentioned automata are not only purely universal but also purely existential, i.e., deterministic. The power of universal choice will be only used in the last automaton A check , that checks for correctness of each transition step of S. While analysing definition of A check we will comfortably assume that an input word meets all conditions verified by the other automata, otherwise the word is anyway not accepted.

The transition rules of A check from the initial state s 0 are as follows:

s 0 , q, tt → s 0 ∧ (s step , {x}), for q ∈ Q \ {q 0 } s 0 , q 0 , tt → s 0 , Σ ∪ ∆, tt → s 0 .
Intuitively, at each q ∈ Q, except at q 0 , an extra automaton is run from the state s step , in order to check correctness of a single step. Symbol on the right-hand side stands for a distinguished state that accepts unconditionally.

ACM Transactions on Computational Logic, Vol. V, No. N, September 2006.

Alternating Timed Automata

• 17 Now the rules s step , γ, . . . → . . . depend on γ = q, x, q . There are three cases, corresponding to conditions (P3a), ( P3b) and (P3c), respectively. I. Case γ = q, ε, q :. s step , q, ε, q , tt → s channel .

In state s channel , the automaton checks the condition (P3a), i.e., whether all consecutive letters from Σ are copied one time unit later. This is done by:

s channel , a, tt → s channel ∧ (s +1 a , {x}), for a ∈ Σ s channel , q, tt → , for q ∈ Q.
Hence, the automaton starts a check from s +1 a at every letter read. Note that this is precisely here where the universal branching is essential. The task of s +1 a is to check that there is letter a one time unit later:

s +1 a , a, x = 1 → s +1 a , Σ, x < 1 → s +1 a .
II. Case γ = q, !a, q :. s step , q, !a, q , tt → s !a .

From state s !a the automaton is responsible for checking the correctness of the operation !a, i.e., condition (P3b):

s !a , a, tt → s channel s !a , b, tt → (s +1 b , {x}) ∧ s channel , for b ∈ Σ \ {a} s !a , q, tt → , for q ∈ Q.
First rule reads simply the letter a and then starts the check from s channel . This is the correct behaviour both when the written message was not forgotten, and when after forgetting it the first message is still a. The second rule deals with the case when the a written to the channel has been lost immediately. The last rule deals with the case when not only the a has been lost, but moreover the channel is empty.

III. Case γ = q, ?a, q :. s step , q, ?a, q , tt → s ?a ∧ (s try?a , {x}).

The behaviour of s ?a is very similar to s channel but additionally it will start a new copy of the automaton in the state s try?a . The goal of s try?a is to check for the letter a at the end of the present configuration.

s ?a , b, tt → s ?a ∧ (s +1 b , {x}) ∧ (s try?a , {x}), for b ∈ Σ s ?a , Q, tt → .
Note the clock reset when entering to s try?a . As we cannot know when the configuration ends we start s try?a at each letter read. If we realize that this was not the end (we see another channel letter) then the check just succeeds. If this was the end (we see a state) then the true check starts from the state s check?a :

s try?a , Σ, tt → s try?a , Q, tt → s check?a .

• S. Lasota and I. Walukiewicz

From s check?a we look for some a that appears more than one time unit later:

s check?a , Σ, x ≤ 1 → s check?a s check?a , a, x > 1 → s check?a , b, x > 1 → s check?a , for b ∈ Σ\{a}.
Automaton A check has no other accepting states but . By the very construction, A satisfies Lemma 4.8. By Lemma 4.7, S has a computation (2) ending in (q f , w f ) if and only if L(A) is nonempty. This completes the proof of Theorem 4.1.

SILENT TRANSITIONS

In this section we point out that by extending the alternating timed automata model with -transitions we lose decidability. It is known that -transitions extend the power of nondeterministic timed automata [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bérard | Characterization of the expressive power of silent transitions in timed automata[END_REF]].

Here we show some evidence that every extension of alternating timed automata with -transitions will have undecidable emptiness problem.

It turns out that there are many possible ways of introducing -transitions to alternating timed automata. To see the issues involved consider the question of whether such an automaton should be allowed to start uncountably many copies of itself or not. Facing these problems we have decided not discuss virtues of different possible definitions but rather to show where the problem is. We will show that the universality problem for purely existential automata with a very simple notion of -transitions is undecidable.

Timed words are written here in the same convention as in previous section: w = (a 1 , t 1 )(a 2 , t 2 ) . . . (a n , t n ) means that the letter a i appeared at time t i since the beginning of the computation.

We consider purely existential (i.e. nondeterministic) automata with one clock. We equip them now with additional -transitions of the form q, , σ → b. The following trick is used to shorten formal definitions.

Definition 5.1. A nondeterministic timed automaton with -transitions over Σ is a nondeterministic timed automaton over the alphabet Σ = Σ ∪ { }.

For convenience, we want to distinguish an automaton A with -transitions over Σ from the corresponding automaton over Σ ; the latter will be denoted A . Given a timed word v over Σ , by |v| we mean the timed word over Σ obtained from w by erasing all (timed) occurrences of . Definition 5.2. A timed word over Σ is accepted by a timed automaton A with -transitions if there is a timed word v over Σ accepted by A such that w = |v| .

Note that according to the definition, an accepting run is always finite. The main result of this section is:

Theorem 5.3. The universality problem for one-clock nondeterministic timed automata with -transitions is undecidable.

The proof is by reduction of the reachability problem for perfect channel systems, defined similarly as lossy reachability in Definition 4.4, but w.r.t. perfect computation of channel systems. Not surprisingly, a perfect computation is any finite • S. Lasota and I. Walukiewicz In state s channel , the automaton searches for a message loss. Here we needtransitions to choose the right moment to move to state s +1 :

s channel , , x > 0 → (s +1 , {x}) s channel , Σ, tt → (s channel , {x})
The task in state s +1 is to wait precisely one time unit and then check for a letter, similarly as state s +1 a in Section 4. Transition from s channel to s +1 is only possible when x > 0. As x is reset at each letter read, this ensures a positive delay between any letter and an -move.

s +1 , Σ, 0 < x < 1 → s +1 s +1 , Σ, x = 1 →
The only way of accepting from s +1 is to consume a number of letters while 0 < x < 1 and finally find a letter at x = 1. Note strictness of the left-hand side inequality in 0 < x < 1. It is crucial here and excludes x = 0, that would mean that some letter occurred in the input word at the moment of the -move that entered into s +1 . This completes our description of the construction of the automaton A as required by Lemma 5.6. Having it we have the automaton A which shows Theorem 5.3.

INFINITE WORDS

In this section we consider one-clock alternating timed automata over infinite words with Büchi acceptance condition. The acceptance game is defined similarly as in Section 2, but it is played over an ω-word (a 1 , t 1 )(a 2 , t 2 ) . . . , where t 1 < t 2 < . . .. Hence each play (q 0 , v 0 ), (q 1 , v 1 ), . . . is infinite. The winner is Eve iff an accepting state appears infinitely often, i.e., q i ∈ F for infinitely many indices i. We do not explain the details since we will only consider nondeterministic automata in this section (i.e., only Eva plays). We prove the following result.

Theorem 6.1. The universality problem for one-clock nondeterministic Büchi timed automata is undecidable.

As a direct corollary, emptiness problem of one-clock alternating Büchi automata is undecidable as well.

To prove Theorem 6.1 we code the halting problem of a Turing machine. We can assume that the Turing machine starts the empty tape and accepts by reaching a unique accepting state q acc . Furthermore, we assume that the machine is deterministic, i.e., we have a transition function δ specifying for each control state q and tape symbol a a triple δ(q, a) = (d, q , b) consisting of a head direction d ∈ {←, •, →}, new state q and letter b to be written onto the tape in place of a.

The idea of the reduction is based on the fact that instead of considering a computation that just stops in an accepting state we will encode existence of a computation that after reaching an accepting state clears the tape with blanks and restarts. Thus the accepting computation is rather a repetitive accepting computation. As the machine is deterministic, the same execution will be essentially replayed infinitely often.

Alternating Timed Automata

• 21

We code a sequence of configurations as before, each configuration should fit in a unit interval. We make our simulation in such a way that the first configuration is already of length sufficient for the whole computation, hence in the simulation of machine steps we will never have to add or remove tape positions.

The nondeterministic automaton we are going to construct will accept the sequences that are not encodings of the repetitive accepting computation of the machine. With one clock we can check that there is a cheating, i.e., letter a in one configuration is changed to b in the next although it should have not. We can also check that a letter disappeared (it was in one configuration and not in the next). What we cannot check directly is that there are new letters in the next configuration, i.e., there can appear new tape positions that were not there before. But if this kind of inserts happen infinitely often then we can find a sequence of tape symbols appearing at times t 1 < t 2 < . . . such that the sequence fract(t 1 ), fract(t 2 ), . . . is either strictly increasing or strictly decreasing. This can be checked by a nondeterministic Büchi automaton with one clock. Hence, we can construct an automaton that does not accept the sequences where there are no cheatings, no disappearances and only finitely many inserts. In such a sequence we have, from some position on, a correct and accepting computation of the Turing machine. Thus, the nondeterministic automaton will not accept some word iff the machine halts, i.e., accepts from the empty tape. Now we will make all these intuitions more formal. Let M be a fixed Turing machine in the rest of this section; by Q and Σ let us denote the set of control states and tape alphabet of M, respectively. Assume that a blank symbol B is in Σ. Given M, we will effectively construct a nondeterministic Büchi automaton A with a single clock x over the input alphabet Σ = Q∪Σ∪Σ×{H}. A letter a, H , for a ∈ Σ, represents a tape symbol a with the head over it. We put Σ H = Σ ∪ Σ×{H}.

The configuration of M is a pair (q, w) consisting of a control state q ∈ Q and a word w ∈ Σ H * representing the tape content. The transition function δ of M gives rise to a relation between configurations, describing the single step of M. We will denote this by qw -→ q w , to say that a single step from configuration (q, w) yields a new configuration (q , w ) and that w and w are of the same length. So we will model computation that does not go outside w with the idea that enough space was allocated in the initial configuration.

This notation assumes a fixed size of tape available, i.e., w and w are of the same length and the head may not move outside w. For convenience, we will also write qv ; q v for timed words v and v if q untime(v) -→ q untime(v ) holds and time-stamps are identical in v and v (note that v and v are of the same length in particular); untime(v) stands for the word v after removing time-stamps. Definition 6.2. By a recurrent accepting computation encoding we mean any timed word w over Σ of the form: (q 0 , t 0 ) v 0 (q 1 , t 1 ) v 1 . . . , such that the following conditions hold:

(P1). Structure: each q i ∈ Q and each v i = (a 1 i , u 1 i ) . . . (a li i , u li i ) is a nonempty finite timed word over Σ H such that precisely one of a 1 i . . . a li i is in Σ×{H}. (P2). Distribution in time: i = t i < u 1 i < u 2 i < . . . < u li i < t i+1 = i+1.
• S. Lasota and I. Walukiewicz (P3). Acceptance: q 0 is the initial state of M, each of a 1 0 . . . a l0 0 is in {B, B, H }, and q i = q acc for infinitely many i.

(P4). Recurrence: whenever q i-1 = q acc , then q i = q 0 and a 1 i , . . . , a li i ∈ {B, B, H }. (P5). Steps: whenever q i-1 = q acc , q i-1 (v i-1 + 1) ; q i v, for some v v i . (P6). Insertions bound: w contains no infinite subsequence (a 0 , u 0 )(a 1 , u 1 ) . . . such that u 0 < u 1 < . . ., a i ∈ Σ H for all i ≥ 0, and the sequence fract(u 0 ), fract(u 1 ), . . . is either strictly increasing or strictly decreasing. Lemma 6.3. Started with the empty tape, the machine M accepts if and only if there exists a recurrent accepting computation encoding as in Definition 6.2.

Proof. Assume M accepts. There is a sequence q 0 w 0 -→ q 1 w 1 . . . -→ q n w n where q n = q acc and w 0 is a finite word over Σ H representing a sufficiently big portion of initially empty tape to store the computation. Hence, there is a recurrent accepting computation encoding obtained by repeating infinitely the word q 0 w 0 q 1 w 1 . . . q n w n ; time-stamps for tape symbols in w 0 , w 1 , . . . can be chosen arbitrarily to satisfy (P2) and (P5).

For the opposite direction, assume that some recurrent accepting computation encoding w exists.

By (P6), it contains only finitely many insertions, where by an insertion we mean a pair (a, t), a ∈ Σ H , appearing in w such that no letter appears at time t -1 in w. Indeed, assume otherwise, i.e., assume that the number of insertions in w is infinite. Build the infinite sequence of all the insertions, in the order they appear in w. The fractional parts fract(t) of all the time-stamps form an infinite sequence of reals in (0..1), with no number appearing twice. Such a sequence has necessarily a subsequence that is either strictly increasing or strictly decreasing -contradiction with (P6).

By (P3) and (P4), w contains infinitely many restarts of the machine. This implies that there is a restart followed by no insertion any more. Hence, from this position on, the encoding simulates the machine faithfully and provides the halting run of the machine.

The undecidability result will follow from the next lemma. Lemma 6.4. A nondeterministic automaton A can be effectively constructed such that L(A) contains precisely all timed words that are not recurrent accepting computation encodings.

The automaton A is a disjunction of six automata, each of them accepting timed words that do not satisfy one of conditions (P1)-(P6), respectively. We omit the automata for (negation of) (P1)-( P4) and focus on the other two conditions only. While analysing the definitions we may assume conveniently that the input word satisfies conditions (P1)-(P4).

Automaton for negation of (P5), in its initial state s 0 , at each letter q ∈ Q read, decides nondeterministically either to check this step, or to keep searching for ACM Transactions on Computational Logic, Vol. V, No. N, September 2006.

Alternating Timed Automata

• 23 another step to check; in the former case, it guesses a move of the head in this step: s 0 , q, tt → s q ← ∨ s q → ∨ s q • ∨ s 0 , for q ∈ Q s 0 , Σ H , tt → s 0 .

To show the idea, we present in detail the transition rules from state s q

• only; but we omit transitions from s q ← and s q → , as they are conceptually similar. In state s q • , the automaton needs to check that the next configuration differs from the configuration determined by a single machine step from the current configuration. The automaton can check tape symbols appearing precisely one unit later that some symbol in the current configuration; hence insertions are pretty allowed.

s q

• , a, tt → (s +1 a , {x}) ∨ s q • , for a ∈ Σ s q

• , a, H , tt → (s +1 b,H , {x}) ∨ s q cont , if δ(q, a) = (•, q , b) s q cont , a, tt → (s +1 a , {x}) ∨ s q cont s q cont , q , tt → , if q = q.

Observe that the automaton fails to accept from s q • if the head move in current configuration is not '•', i.e, the automaton's guess has been incorrect. The task from state s +1 a , for a ∈ Σ H , is merely to check that the letter appearing one unit later is not equal to a, or that there is no such letter at all:

s +1 a , Σ, x < 1 → s +1 a s +1 a , b, x = 1 → , if a = b s +1 a , Σ, x > 1 → .
The only accepting state is . Now we switch to condition (P6). The task is to recognize a strictly increasing or strictly decreasing subsequence as defined in (P6), hence the automaton is a disjunction A inc ∨ A dec . For simplicity of analysis, assume that the input word satisfies all previous conditions (P1)-(P5). In particular, for each letter appearing at time t, say, there is another letter at time t + 1.

As a preparation, consider the following transition rules, from states s and s, respectively:

s, Σ H , tt → s s, Q, x < 1 → s s, Q, x = 1 → (s, {x}) s, Σ H , x < 1 → s s, Σ H , x = 1 → (s, {x}) s, Q, tt → (s, {x})
Imagine that the clock x has been reset at some letter a ∈ Σ H of the input word. Now, starting from state s, the above rules describe scanning of the word in the following cycle: scan all letters in Σ H staying in state s, then on q ∈ Q change the state to s; then scan the following letters in Σ H until x = 1, i.e., until precisely one time unit elapses since the last clock reset; then reset the clock again and change to state s; and so on. Hence, the whole word is conceptually split into segments determined by the clock resets, and each segment is typically scanned in two "phases": first the s-phase and then the s-phase. The transition from s to s can happen when we see a state from Q; thus only at integer times by property (P2). The only small difference appears when one of the phases starts by a clock reset at some letter q ∈ Q; in this case the other phase is degenerate and the bottom-most transition rules for s and s apply. In fact this is the case initially, since for the initial state of A inc and A dec we choose s and s, respectively. Having these rules, definition of A inc and A dec requires only appropriate handling of moments where additional clock resets may be done. In A inc the additional clock resets will be enabled only during s-phase, while in A dec only in s-phase.

We will need a third state s with the following rules:

s , Σ H , tt → s s , Q, tt → s,
enabling to mimic the s-phase, but not enabling for any additional clock reset until some q ∈ Q is observed. State s will be the only accepting state in both A inc and A dec and will be intentionally visited at each consecutive letter belonging to a strictly increasing (or decreasing) subsequence. Now, to complete the definition of A inc , we allow the transition from s to s by replacing the first rule for s by the following rule:

s, Σ H , tt → s ∨ (s , {x}).

Notice that we do not allow to reset clock more than once in one s-phase (by the first rule for s ). But as we have assumed (P1)-( P5), we know that each letter reappears, perhaps not identically, one unit later. Hence we will not miss a strictly increasing subsequence, but only "postpone" capturing its next element to the next s-phase.

Similarly, to complete the definition of A dec , we allow the transition from s to s by replacing the first rule for s by the following one: s, Σ H , x < 1 → s ∨ (s , {x}).

This completes description of automaton A needed for the proof of Lemma 6.4 and hence also the proof of Theorem 6.1.

FINAL REMARKS

In this paper we have explored the possibilities opened by the observation that the universality problem for nondeterministic timed automata is decidable [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF] We have extended this result to obtain a class of timed automata that is closed under boolean operations and that has decidable emptiness problem. We have shown that despite being decidable the problem has prohibitively high complexity. We have also considered the extension of the model with epsilon transitions. The undecidability result for this model points out what makes the basic model decidable and what further extensions are not possible. Finally, maybe somewhat surprisingly, we prove that the universality for 1-clock nondeterministic timed automata but over infinite words is undecidable.

We see several topics for further work:

-Adding event-clocks to the model and/or extending from timed words to trees. It seems that in both cases one would still obtain a decidable model.

  Definition 3.10. Let denote the monotone domination ordering over Λ * induced by the subset inclusion over Λ, defined as follows: a 1 . . . a n b 1 . . . b m iff there exists a strictly increasing function f : {1, . . . , n} → {1, . . . , m} such that for each

ACM Transactions on Computational Logic, Vol. V, No. N, September 2006, Pages 1-26.

ACM Transactions on Computational Logic, Vol. V, No. N, September 2006.

ACKNOWLEDGMENTS

We would like to thank the referees for helpful remarks.

Alternating Timed Automata

• 19 sequence of (perfect) transitions:

(q 0 , ) γ1 -→ (q 1 , w 1 ) γ2 -→ (q 2 , w 2 ) . . . γn -→ (q n , w n ), Theorem 5.4 [START_REF] Brand | On communicating finite-state machines[END_REF]. The perfect reachability problem for channel systems is undecidable, assumed |Σ| ≥ 2. Given a channel system S = (Q, q 0 , Σ, ∆) and a configuration (q f , w f ), we effectively construct a one-clock nondeterministic timed automaton with -transitions A over Σ. Automaton A will accept precisely the complement of the set of all perfect computation encodings ending in (q f , w f ), defined by: Definition 5.5. A perfect computation encoding ending in (q f , w f ) is defined as in Definition 4.6, but with the conditions (P3a) -(P3c) replaced by:

Since each perfect computation encoding is a lossy one, A will be defined as a disjunction, A := ¬A ∨ A, of the complement of the automaton A from the previous section and another automaton A. As automaton ¬A takes care of all timed words that are not lossy computation encodings, it is enough to have: Lemma 5.6. Automaton A accepts precisely these lossy computation encodings ending in (q f , w f ) that are not perfect computation encodings.

This will be enough for correctness of our reduction: A will accept precisely the complement of the set of all perfect computation encodings.

In the rest of this section we sketch the construction of the automaton required by Lemma 5.6.

When defining the behaviour of A we can conveniently assume that the input word is already a lossy computation encoding. The aim of A is to find a loss of a message in the channel. This will be achieved, roughly, via an -rule trying to guess a moment t in time such that there is no message occurrence at time t but there is one at time t+1. Of course, A (and hence A as well) will have a single clock x and the input alphabet is Σ

The transition rules of A from the initial state s 0 are:

Intuitively, at each q ∈ Q, except at q 0 , A chooses either to check correctness of this single step or to skip it. A will have no accepting states but that we will use later. Now the rules s step , γ, . . . → . . . for state s step depend on γ = q, x, q . There are three cases, corresponding to conditions (P3a), ( P3b) and (P3c), respectively. As the rules follow a similar pattern to that in Section 4, we present only the simplest case when γ = q, , q . s step , q, , q , tt → (s channel , {x}).

Alternating Timed Automata

• 25 -Decidability of the universality problem for one-clock co-Büchi automata is still open. -Finding logical characterisations of the languages accepted by alternating timed automata with one clock. Since we have the closure under boolean operations, we may hope to find one. -Finding a different syntax that will avoid the prohibitive complexity of the emptiness problem. There may well be another way of presenting alternating timed automata that will give the same expressive power but for which the algorithmic complexity of the emptiness test will be lower.