Alternating Timed Automata
Slawomir Lasota Institute of Informatics, Warsaw University and Igor Walukiewicz LaBRI, Universit� Bordeaux-1 e 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. Categories and Subject Descriptors: F.1.2 [Theory of Computation]: Modes of Computation--Alternation and nondeterminism; F.4.3 [Theory of Computation]: Formal Languages-- Decision problems General Terms: Languages, Theory Additional Key Words and Phrases: Alternation, timed automata, emptyness problem 1. 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 [Alur and Dill 1994] 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 [Ouaknine and Worrell 2004] Ouaknine and Worrell has shown that the universality problem is decidable for nondeterministic automata with one
Author's addresses: Slawomir 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 e e 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
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006, Pages 1�26. 2 � S. Lasota and I. Walukiewicz 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 [Ouaknine and Worrell 2004]. 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 -hard) [Alur and Dill 1994]. One solution to this problem is to 1 restrict to deterministic timed automata. Another, is to restrict the reset operation; this gives the event-clock automata model [Alur et al. 1999]. 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 [Schnoebelen 2002]. 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 [Ouaknine and Worrell 2004]. Techniques similar to our decidability proof and to insights of [Ouaknine and Worrell 2004] have been developed eariler in [Abdulla and Jonsson 1998; 2001]. Except for [Dickh�fer and Wilke 1999], it seems that the notion of alternation in o the context of timed automata was not studied before. The reason was probably undecidability of the universality problem. The alternating automata introduced
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. Alternating Timed Automata � 3 in [Dickh�fer and Wilke 1999] run over infinite timed trees and were used to show deo cidability 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 [Torre and Napoli 2001]. Some research (see [Asarin et al. 1998; Cassez et al. 2002; Bouyer et al. 2003; Alur et al. 2004; Bouyer et al. 2004] 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 [Dima 2000; Laroussinie et al. 2004], leading to a lower complexity in some cases. Finally, in [Alur et al. 1993] 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 [Ouaknine and Worrell 2005] and by Abdulla et al [Abdulla et al. 2005]. 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 [Lasota and Walukiewicz 2005]. 2. 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 [Alur and Dill 1994]. 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
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 4 � S. Lasota and I. Walukiewicz (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 [Alur and Dill 1994] 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, q0 , , 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 q0 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 = (a1 , t1 )(a2 , t2 ) . . . (an , tn ) (1) of pairs from � R+ . Each ti describes the amount of time that passed between reading ai-1 and ai , i.e., a1 was read at time t1 , a2 was read at time t1 +t2 , and so on. In Sections 4 and 5 it will be more convenient to use an alternative representation where ti 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
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. Alternating Timed Automata � 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 GA,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 (q0 , v0 ), where v0 : C R+ is a valuation assigning 0 to each clock variable. It consists of n phases. The (k+1)-th phase starts in (qk , vk ), � ends in some configuration (qk+1 , vk+1 ) and proceeds as follows. Let v := vk +tk+1 . � Let be the unique constraint such that v satisfies and b = (qk , ak+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 = b1 b2 : Adam chooses one of subformulas b1 , b2 and the play continues with b replaced by the chosen subformula; --b = b1 b2 : dually, Eve chooses one of subformulas; � --b = (q, r) Q�P(C): the phase ends with the result (qk+1 , vk+1 ) := (q, v[r := 0]). A new phase is starting from this configuration if k+1 < n. The winner is Eve if qn is accepting (qn 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 GA,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. [Alur and Dill 1994]). 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 q0 , q1 , q2 . State q0 is initial. The automaton has a single clock x and the following transition rules: q0 , a, tt (q0 , ) (q1 , {x}) q1 , a, x=1 (q2 , ) q1 , a, x=1 (q1 , ) q2 , a, tt (q2 , ) States q0 and q1 are accepting, q2 is not. In state q0 , at each input letter, Adam chooses either to stay in q0 either to to go to q1 ; In the latter case clock x is reset. Furthermore, the automaton can only quit state q1 exactly one time unit after entering it. Hence, Adam has a strategy to reach q2 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:
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 6 � S. Lasota and I. Walukiewicz 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 qsink . 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 = iX i iX �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 ) = {(qsink , )}. And finally we put: (qsink , a, X ) = {(qsink , )}, 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 [Alur and Dill 1994] 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 t1 and t2 , where 0 < t1 < t2 < 1, no other b in between 0 and 1 and precisely one b between t1 + 1 and t2 + 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 bk of k letters b determines a function fk : QB QB saying that if started in k B the state q after reading b the automaton will end in fk (q). Clearly the number of such functions is bounded if the number of states is fixed. Thus there are m B B and l, depending only on the number of states, such that fm = fm+l . Moreover B B fm+i = fm+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 B B function of the automaton are integers. Let m and l be such that fm+i = fm+l+i 2n for all i > 0 and for all deterministic automata B with at most 22 states. Now consider two words w1 and w2 . In w1 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 w2 is obtained from w1 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 w1 then it also accepts w2 . Consider the accepting run of A on w1 . 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
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 8 � S. Lasota and I. Walukiewicz 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 2n most 22 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 w2 if it had one in w1 . 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 a1+m and a1+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 w1 or on w2 , for the same reason as before. As the rest of w1 is the same as the rest of w2 we are done. On the other hand, when comparing configurations with clock value < 0.7 in runs over w1 and w2 , 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 w1 and w2 as follows. In w1 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 w2 is obtained from w1 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. 3. 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 [Ouaknine and Worrell 2004]
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. Alternating Timed Automata � 9 for our more general setting. We point out the differences below. Fix a one-clock alternating timed automaton A = (Q, q0 , , {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 a,t P0 = {(q0 , 0)} and there is a transition P - 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 (q1 , r1 ) . . . (qk , rk ) --let Next(q,v) = {(qi , v [ri := 0]) : i = 1 . . . k}. --Then, let P :=
(q,v)P (k > 0), 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 [Ouaknine and Worrell 2004], the essential difference is that we have to deal with both disjunction and conjunction, while in [Ouaknine and Worrell 2004] only one of them appeared. We treat conjunction similarly to determinization in [Ouaknine and Worrell 2004]. 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 [Ouaknine and Worrell 2004], the degree of the nodes of H will not be bounded but nevertheless finite. This is sufficient for our purposes. A state {(q1 , v1 ), . . . , (qn , vn )} of T is called bad iff all control states qi are accepting (qi 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 P0 to a bad state. Let T be a labelled transition system obtained from T by erasing time information a,t a from transition labels, i.e., there is a transition P - Q in T iff there is P - 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 P0 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
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 10 � S. Lasota and I. Walukiewicz are uncountably many states. The following definition allows to abstract from the precise timing information in states. Let cmax denote the biggest constant appearing in constraints in . Let set reg of regions be a partition of R+ into 2 � (cmax +1) sets as follows: reg := {{0}, (0, 1), {1}, (1, 2), . . . , (cmax -1, cmax ), {cmax }, (cmax , +)}. 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 = {(q1 , 0.5), (q2 , 1.2), (q3 , 2.2)}, where q1 , q2 , q3 are locations. Let cmax = 2. Denote regions by r0 = {0}, r0,1 = (0, 1), . . . , r2 = {2}, r2,+ = (2, +). First, P is transformed into the set { q1 , r0,1 , 0.5 , q2 , r1,2 , 0.2 , q3 , r2,+ , 0.2 }. We make it into a sorted sequence q2 , r1,2 , 0.2 q3 , r2,+ , 0.2 q1 , r0,1 , 0.5 . Then we group together triples with the same fractional part, obtraining a sequence of length two: { q2 , r1,2 , 0.2 , q3 , r2,+ , 0.2 }, { q1 , r0,1 , 0.5 }. Finally we remove the fractional parts and obtain H(P ) = {(q2 , r1,2 ), (q3 , r2,+ )}, {(q1 , r0,1 )}. Definition 3.7. Let H be the transition system whose states are words H(P ) for a a P a state of T ; a transition W1 - W2 is in H if there is a transition P1 - P2 in T with H(P1 ) = W1 , H(P2 ) = W2 . The initial state in H is W0 = H(P0 ). Example 3.8. Assume that the automation from previous example has a rule: q3 , a, x>2 (q1 , x) ((q2 , ) (q3 , )). Imagine a transition P - P in T corresponding to P - P in T derived from the above rule. There are two possibilities: P = {(q1 , 1.1), (q2 , 1.8), (q1 , 0)} or P = {(q1 , 1.1), (q2 , 1.8), (q2 , 2.8), (q3 , 2.8)}. Accordingly, there are two trana sitions H(P ) - W in H, for W = {(q1 , r0 )}{(q1 , r1,2 )}{(q2 , r1,2 )} or W = {(q1 , r1,2 )}{(q2 , r1,2 ), (q2 , r2,+ ), (q3 , r2,+ )}. In each case W = H(P ). Hence,
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. a a,0.6 Alternating Timed Automata � 11 transitions in H can "simulate" transitions in T . On the other hand, H(P ) has also a transition H(P ) - {(q1 , r0 )}{(q1 , r1,2 )}{(q2 , r1,2 ), (q2 , r2,+ ), (q3 , r2,+ )} � that simulates a posible transition of P = {(q1 , 0.5), (q2 , 1.2), (q3 , 2.2), (q3 , 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 W0 . Proof. By Lemma 3.4 we only need to show: a bad state is reachable in T from P0 iff a bad state is reachable in H from W0 . Consider a transition system T obtained from T by imposing one additional restriction on transitions: whenever v1 and v2 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 P0 iff a bad state is reachable in T from P0 . And also: a bad state is reachable in H from W0 iff a bad state is reachable in H from W0 . Now observe that the graph of H, i.e., the set of all pairs (P, H(P )), is a bisima a ulation between T and H . If P - P then obviously H(P ) - H(P ). If a a H(P ) - W then there exists P such that P - P and H(P ) = W ; we only a,t need to guess appropriate t and derive P from transition P - P in T (clearly t need not be unique). The bisimulation guarantees that a bad state is reachable in T from P0 iff a bad state is reachable in H from W0 . 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 [Abdulla et al. 1996; Finkel and Schnoebelen 2001] 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. Definition 3.10. Let denote the monotone domination ordering over induced by the subset inclusion over , defined as follows: a1 . . . an b1 . . . bm iff there exists a strictly increasing function f : {1, . . . , n} {1, . . . , m} such that for each i n, ai bf (i) . Lemma 3.11 [Higman 1952]. Relation is a wqo, i.e., for arbitrary infinite sequence W1 , W2 , . . . of words over , there exist indexes i < j such that Wi Wj . 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
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 12 � S. Lasota and I. Walukiewicz 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 - 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 (cmax , )) in this case. a Now imagine a transition W - W in H. This corresponds to some transition a,t P - 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 (cmax , ) as well). In the first case, change each region {i} in the first letter of W to (i, i + 1) (or to (cmax , ), if i = cmax ). 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}. a Hence, the set {W : W - W for some a} can be computed by applying the operation defined above an arbitrary number of times (until all regions are (cmax , )), 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 [Ouaknine and Worrell 2004]. Lemma 3.13. The inverse of relation is a simulation: whenever W1 a a and W2 - W2 , there is some W1 such that W1 - W1 and W1 W2 .
a a W2 Proof. Take W1 W2 and suppose W2 - W2 . By definition it means that a there is P2 with H(P2 ) = W2 such that there is a transition P2 - P2 and H(P2 ) = W2 . Since W1 W2 it is easy to see that there is P1 P2 such that W = H(P1 ); P1 is obtained by removing from P2 the pairs that do not end up in W1 when construction H is applied (cf. Definition 3.5). Now, directly from the definition of a a the transition system T we have P1 - P1 with P1 P2 . So W1 - H(P1 ). As P1 P2 , we have H(P1 ) W2 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 is bad then W is bad as well.
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. W and Alternating Timed Automata � 13 Proof. Take a letter wi of W . We need to show that q F for every (q, r) wi . By the definition of W W we have wi wj for some letter wj of W . Hence, (q, r) wj 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 W0 . Proof. The reachability tree is the unravelling of H from W0 . 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 W0 then t contains at least one bad state. Let W be such a bad state reachable from W0 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 W1 and W2 such that W1 is an ancestor of W2 in the reachability tree and W1 W2 (i.e., W2 was not added into t). Since the inverse of is a simulation by Lemma 3.13, the sequence of transitions in from W2 to W can be imitated by the corresponding sequence of transitions from W1 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. a,t The transition relation P - 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, vx , x), one for each clock x of A. The triples are identical on the first component, and vx 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.
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 14 � S. Lasota and I. Walukiewicz 4. 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 [Ouaknine and Worrell 2004]. 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 [Schnoebelen 2002]. Definition 4.3 Channel system. A channel system is given by a tuple S = (Q, q0 , , ), where Q is a finite set of control states, q0 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 (q0 , ), 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 = q0 . 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: (q0 , ) = (q1 , w1 ) = (q2 , w2 ) . . . = (qn , wn ).
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 1 2 n (2) Alternating Timed Automata � 15 Definition 4.4. Lossy reachability problem for channel systems is: given a channel system S and a configuration (qf , wf ), with qf =q0 , decide whether there is a lossy computation of S ending in (qf , wf ). Theorem 4.5 [Schnoebelen 2002]. The lossy reachability problem for channel systems has non-primitive recursive complexity. The result of [Schnoebelen 2002] 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, q0 , , ), and a configuration (qf , wf ), 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 (qf , wf ). A computation as in (2) will be encoded as the following word over : qn n wn qn-1 n-1 wn-1 . . . q1 1 w1 q0 ,
(3) where qi Q, i , wi . 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 = (a1 , t1 )(a2 , t2 ) . . . (an , tn ) we mean that the letter ai appeared ti time units after the beginning of the word. In particular, ai+1 appeared ti+1 - ti time units after ai . Clearly this is correct only when ti+1 ti , 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 qn appears at time 0 and then that each letter qi appears at time n - i. 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 wi and wi-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 ti by one time unit, i.e., (w + 1) = (a1 , t1 + 1)(a2 , t2 + 1) . . . (an , tn + 1). Definition 4.6. By a lossy computation encoding ending in (qf , wf ) we mean any timed word over of the form: (qn , tn )(n , tn )vn (qn-1 , tn-1 )(n-1 , tn-1 )vn-1 . . . (q1 , t1 )(1 , t1 )v1 (q0 , t0 ), where each vi = (a1 , u1 ) . . . (ali , uli ) is a timed word over . Additionally we i i i i require that for each i n and j = 1, . . . , li , the following conditions hold: (P1). Structure: qi Q, i , aj , i = qi-1 , x, qi , qn = qf and a1 . . . aln = wf . n n i (P2). Distribution in time: n-i = ti < ti < u1 < u2 < . . . < uli < ti+1 = n-i+1. i i i
ACM Transactions on Computational Logic, Vol. V, No. N, September 2006. 16 � S. Lasota and I. Walukiewicz (P3a). Epsilon move: if i = qi-1 , , qi then (vi + 1) vi-1 . (P3b). Write move: if i = qi-1 , !a, qi then either vi = (a, u1 )v and v + 1 i vi-1 , or (vi + 1) vi-1 . (P3c). Read move: if i = qi-1 , ?a, qi then vi-1 = v (a, t)v for some timed words v , v and t R+ , such that (vi + 1) v . Lemma 4.7. S has a computation of the form (2) ending in (qn , wn ) = (qf , wf ) if and only if there exists a lossy computation encoding ending in (qf , wf ) 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 (qf , wf ). 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 := Astruct Aunit Astrict Acheck . All four automata will be purely universal and will use at most one clock. Automaton Astruct verifies condition (P1), automata Aunit and Astrict jointly check condition (P2), and Acheck enforces the most involved conditions (P3a) � (P3c). We omit an obvious definition of Astruct . We also omit the construction of the automaton Aunit checking that letters from Q appear precisely at times 0, 1, . . . , n. Automaton Astrict 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: s0 , , x = 0 (s, ) s, , x > 0 (s, {x}). with s0 an initial state and both s0 , 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 Acheck , that checks for correctness of each transition step of S. While analysing definition of Acheck 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 Acheck from the initial state s0 are as follows: s0 , q, tt s0 (sstep , {x}), s0 , q0 , tt s0 , , tt s0 . for q Q \ {q0 } Intuitively, at each q Q, except at q0 , an extra automaton is run from the state sstep , 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 sstep , , . . . . . . depend on = q, x, q . There are three cases, corresponding to conditions (P3a), (P3b) and (P3c), respectively. I. Case = q, , q :. sstep , q, , q , tt schannel . In state schannel , the automaton checks the condition (P3a), i.e., whether all consecutive letters from are copied one time unit later. This is done by: schannel , a, tt schannel (s+1 , {x}), for a a schannel , q, tt , for q Q. Hence, the automaton starts a check from s+1 at every letter read. Note that this a is precisely here where the universal branching is essential. The task of s+1 is to a check that there is letter a one time unit later: s+1 , a, x = 1 a s+1 , , x < 1 s+1 . a a II. Case = q, !a, q :. sstep , q, !a, q , tt s!a . From state s!a the automaton is responsible for