A Theory of Timed Automata

A Theory of Timed Automata

¹

Rajeev Alur 2 David L. Dill 3

Computer Science Department, Stanford University Stanford, CA 94305.

Abstract. We propose timed (nite) automata to model the behavior of real- time systems over time. Our denition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using nitely many real- valued clocks. A timed automaton accepts timed words | innite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Buchi and Muller acceptance con- ditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata:

both problems are undecidable (¹¹-hard) in the nondeterministic case and PSPACE- complete in the deterministic case. Finally, we discuss the application of this theory to automatic verication of real-time requirements of nite-state systems.

Keywords: Real-time systems, automatic verication, formal languages and au- tomata theory.

1Preliminary versions of this paper appear in theProceedings of the 17th International Colloquium on Automata, Languages, and Programming(1990), and in theProceedings of the REX workshop \Real-time:

theory in practice"(1991).

2Current address: AT&T Bell Laboratories, 600 Mountain Avenue, Room 2D-144, Murray Hill, NJ 07974.

3Supported by the National Science Foundation under grant MIP-8858807, and by the United States Navy, Oce of the Chief of Naval Research under grant N00014-91-J-1901. This publication does not necessarily re ect the position or the policy of the U.S. Government, and no ocial endorsement of this work should be inferred.

1 Introduction

Modal logics and!-automata forqualitative temporal reasoning about concurrent systems have been studied in great detail (selected references: [36, 32, 16, 28, 47, 44, 37, 11]).

These formalisms abstract away from time, retaining only the sequencing of events. In the linear time model, it is assumed that an execution can be completely modeled as a sequence of states or system events, called anexecution trace(or justtrace). Thebehavior of the system is a set of such execution sequences. Since a set of sequences is a formal language, this leads naturally to the use of automata for the specication and verication of systems. When the systems are nite-state, as many are, we can use nite automata, leading to eective constructions and decision procedures for automatically manipulat- ing and analyzing system behavior. The universal acceptance of nite automata as the canonical model of nite-state computation can be attributed to the robustness of the model and the appeal of its theory. In particular, a variety of competing formalisms | nondeterministic Buchi automata, deterministic and nondeterministic Muller automata,

!-regular expressions, modal formulas of (extended) temporal logic, and second-order for- mulas of the monadic theory of one successor (S1S) | have the same expressiveness, and dene the class of !-regular languages [7, 9, 33, 46, 42]. Consequently many verication theories are based on the theory of !-regular languages.

Although the decision to abstract away from quantitative time has had many ad- vantages, it is ultimately counterproductive when reasoning about systems that must interact with physical processes; the correct functioning of the control system of airplanes and toasters depends crucially upon real-time considerations. We would like to be able to specify and verify models of real-time systems as easily as qualitative models. Our goal is to modify nite automata for this task and develop a theory of timed nite automata, similar in spirit to the theory of !-regular languages. We believe that this should be the rst step in building theories for the real-time verication problem.

For simplicity, we discuss models that consider executions to be innite sequences of events, not states (the theory with state-based models diers only in details). Within this framework, it is possible to add timing to an execution trace by pairing it with a sequence of times, where the i'th element of the time sequence gives the time of occurrence of the i'th event. At this point, however, a fundamental question arises: what is the nature of time?

Modeling time

One alternative, which leads to the discrete-time model, requires the time sequence to be a monotonically increasing sequence of integers. This model is appropriate for certain kinds of synchronous digital circuits, where signal changes are considered to have changed exactly when a clock signal arrives. One of the advantages of this model is that it can be transformed easily into an ordinary formal language. Each timed trace can be expanded into a trace where the times increase by exactly one at each step, by inserting a special silent event as many times as necessary between events in the original trace. Once this transformation has been performed, the time of each event is the same as its position, so the time sequence can be discarded, leaving an ordinary string. Hence, discrete time behaviors can be manipulated using ordinary nite automata. Of course, in physical

1

processes events do not always happen at integer-valued times. The discrete-time model requires that continuous time be approximated by choosing some xed quantuma priori, which limits the accuracy with which physical systems can be modeled.

The ctitious-clock model is similar to the discrete time model, except that it only requires the sequence of integer times to be non-decreasing. The interpretation of a timed execution trace in this model is that events occur in the specied order at real-valued times, but only the (integer) readings of the actual times with respect to a digital clock are recorded in the trace. This model is also easily transformed into a conventional formal language. First, add to the set of events a new one, called tick. The untimed trace corresponding to a timed trace will include all of the events from the timed trace, in the same order, but with t^i+1?tⁱ number of ticks inserted between the i'th and the (i+1)'th events (note that this number may be 0). Once again, it is conceptually simple to manipulate these behaviors using nite automata, but the compensating disadvantage is that it represents time only in an approximate sense.

We prefer a dense-time model, in which time is a dense set, because it is a more natural model for physical processes operating over continuous time. In this model, the times of events are real numbers, which increase monotonically without bound. Dealing with dense time in a nite-automata framework is more dicult than the other two cases, because it is not obvious how to transform a set of dense-time traces into an ordinary formal language. Instead, we have developed a theory of timed formal languages and timed automata to support automated reasoning about such systems.

Overview

To augment nite!-automata with timing constraints, we propose the formalism of ^timed automata. Timed automata accept timed words | innite sequences in which a real- valued time of occurrence is associated with each symbol. A timed automaton is a nite automaton with a nite set of real-valued clocks. The clocks can be reset to 0 (indepen- dently of each other) with the transitions of the automaton, and keep track of the time elapsed since the last reset. The transitions of the automaton put certain constraints on the clock values: a transition may be taken only if the current values of the clocks satisfy the associated constraints. With this mechanism we can model timing properties such as \the channel delivers every message within 3 to 5 time units of its receipt". Timed automata can capture several interesting aspects of real-time systems: qualitative fea- tures such as liveness, fairness, and nondeterminism; and quantitative features such as periodicity, bounded response, and timing delays.

We study timedautomata from the perspective of formal language theory. We consider both deterministic and nondeterministic varieties, and for acceptance criteria we consider both Buchi and Muller conditions. We show that nondeterministic timed automata are closed under union and intersection, but surprisingly, not under complementation. The closure properties for the deterministic classes are similar to their untimed counterparts:

deterministic timed Muller automata are closed under all Boolean operations, whereas deterministictimedBuchi automata are closed under only the positive Boolean operations.

These results imply that, unlike the untimed case, deterministic timed Muller automata are strictly less expressive than their nondeterministic counterparts.

We study a variety of decision problems for the dierent types of timed automata. The 2

main positive result is an untiming construction for timed automata. Due to the real- valued clock variables, the state space of a timed automaton is innite, and the untiming algorithm constructs a nite quotient of this space. This is used to prove that the set of untimed words consistent with the timing constraints of a timed automaton forms an

!-regular set. It also leads to a PSPACE decision procedure for testing emptiness of the language of a timed automaton. We also show that the dual problem of testing whether a timed automaton accepts all timed words (i.e., the universality question) is undecidable (¹¹-hard) for nondeterministic automata. This also implies the undecidability of the language inclusion problem. However, both these problems can be solved in PSPACE for the deterministic versions.

Finally, we show how to apply the theory of timed automata to prove correctness of nite-state real-time systems. We give a PSPACE verication algorithm to test whether a system modeled as a product of timed automata satises its specication given as a deterministic timed Muller automaton.

Related work

Dierent ways of incorporating timing constraints in the qualitative models of a system have been proposed recently, however, no attempt has been made to develop a theory of timed languages and no algorithms for checking real-time properties in the dense-time model have been developed.

Perhaps the most standard way of introducing timing information in a process model is by associating lower and upper bounds with transitions. Examples of these include timed Petri nets [38], timed transition systems [35, 21], timed I/O automata [31], and Modecharts [25]. In a timed automaton, unlike these other models, a bound on the time taken to traverse a path in the automaton, not just the timeintervalbetween the successive transitions, can be directly expressed. Our model is based on an earlier model proposed by Dill that employs timers [13]. A model similar to Dill's was independently proposed and studied by Lewis [30]. He denes state-diagrams, and gives a way of translating a circuit description to a state-diagram. A state-diagram is a nite-state machine where every edge is annotated with a matrix of intervals constraining various delays. Lewis also develops an algorithm for checking consistency of the timing information for a special class of state-diagrams; the ones for which there exists a constantK such that at most K transitions can happen in a time interval of unit length. Our untiming construction does not need the latter assumption, and has a better worst-case complexity. We note that the decidability and lower bound results presented here carry over to his formalism also.

There have been a few attempts to extend temporal logics with quantitative time [6, 24, 26, 35, 17, 5, 20]. Most of these logics employ the discrete-time or the ctitious- clock semantics. In the case of the dense-time model the only previously known result is an undecidability result: in [5] it is shown that the satisability problem for a real-time extension of the linear-timetemporal logic PTL is undecidable (¹¹-hard) in the dense-time model.

3

a

a a,b

S0 S₁

Figure 1: Buchi automaton accepting (a + b)^a^!

2

^!

-automata

In this section we will brie y review the relevant aspects of the theory of !-regular lan- guages.

The more familiar denition of a formal language is as a set of nite words over some given (nite) alphabet (see, for example, [23]). As opposed to this, an!-language consists of innite words. Thus an!-language over a nite alphabet  is a subset of ^! | the set of all innite words over . !-automata provide a nite representation for certain types of!-languages. An !-automaton is essentially the same as a nondeterministic nite-state automaton, but with the acceptance condition modied suitably so as to handle innite input words. Various types of!-automata have been studied in the literature [7, 33, 9, 42].

We will mainly consider two types of !-automata: Buchi automata and Muller automata.

A transition table ^Ais a tuple^h;S;S⁰;Eⁱ, where  is an input alphabet, S is a nite set of automaton states, S^{0 } S is a set of start states, and E ^ S^S^ is a set of edges. The automaton starts in an initial state, and if ^hs;s⁰;a^{i 2}E then the automaton can change its state froms to s⁰ reading the input symbol a.

For a word  = ¹²::: over the alphabet , we say that r : s^{0 ?!1} s^{1 ?!2} s^{2 ?!3}

is a run of^A over , provided s^{0 2}S⁰, and ^hs^i?1;sⁱ;ⁱⁱ²E for all i^1. For such a run, the set inf(r) consists of the states s²S such that s = sⁱ for innitely many i^0.

Dierent types of !-automata are dened by adding an acceptance condition to the denition of the transition tables. ABuchi automaton ^Ais a transition table^h;S;S⁰;Eⁱ with an additional set F ^S of accepting states. A run r of ^A over a word ²^! is an accepting run i inf(r)^\F⁶=^;. In other words, a run r is accepting i some state from the set F repeats innitely often along r. The language L(^A) accepted by ^A consists of the words ²^! such that ^A has an accepting run over.

Example 2.1

Consider the 2-state automaton of Figure 1 over the alphabet^fa;b^g. The state s⁰ is the start state and s¹ is the accepting state. Every accepting run of the automaton has the form

r : s^{0 ?!1} s<sup>0 ?!2


?n!</sup> s^{0 ?a!} s^{1 ?a!} s^{1 ?a!}

with ^{i 2 f}a;b^g for 1 ^ i ^ n for some n ^ 1. The automaton accepts all words with only a nite number of b's; that is, the language L⁰ = (a + b)^a^!.

4

a a

b

b

S0 S₁

Figure 2: Deterministic Muller automaton accepting (a + b)^a^!

An !-language is called !-regular i it is accepted by some Buchi automaton. Thus the language L⁰ of Example 2.1 is an !-regular language.

The class of !-regular languages is closed under all the Boolean operations. Language intersection is implemented by a product construction for Buchi automata [9, 47]. There are known constructions for complementing Buchi automata [41, 40].

When Buchi automata are used for modeling nite-state concurrent processes, the verication problem reduces to that of language inclusion. The inclusion problem for

!-regular languages is decidable. To test whether the language of one automaton is contained in the other, we check for emptiness of the intersection of the rst automaton with the complement of the second. Testing for emptiness is easy; we only need to search for a cycle that is reachable from a start state and includes at least one accepting state.

In general, complementing a Buchi automaton involves an exponential blow-up in the number of states, and the language inclusion problem is known to be PSPACE-complete [41]. However, checking whether the language of one automaton is contained in the language of a deterministic automaton can be done in polynomial time [27].

A transition table ^A=^h;S;S⁰;Eⁱis deterministic i (i) there is a single start state, that is, ^jS^0j = 1, and (ii) the number of a-labeled edges starting at s is at most one for all states s ² S and for all symbols a ² . Thus, for a deterministic transition table, the current state and the next input symbol determine the next state uniquely.

Consequently, a deterministic automaton has at most one run over a given word. Unlike the automata on nite words, the class of languages accepted by deterministic Buchi automata is strictly smaller than the class of !-regular languages. For instance, there is no deterministic Buchi automaton which accepts the language L⁰ of Example 2.1. Muller automata (dened below) avoid this problem at the cost of a more powerful acceptance condition.

A Muller automaton ^A is a transition table ^h;S;S⁰;Eⁱ with an acceptance family

F 2^S. A run r of ^A over a word ² ^! is an accepting run i inf(r)^2F. That is, a run r is accepting i the set of states repeating innitely often along r equals some set in

F. The language accepted by^A is dened as in case of Buchi automata.

The class of languages accepted by Muller automata is the same as that accepted by Buchi automata, and also equals that accepted by deterministic Muller automata.

Example 2.2

The deterministic Muller automaton of Figure 2 accepts the language L⁰ consisting of all words over^fa;b^gwith only a nite number of b's. The Muller acceptance family is^ffs^1gg. Thus every accepting run can visit the states⁰ only nitely often.

5

Thus deterministicMuller automata form a strong candidate for representing!-regular languages: they are as expressive as their nondeterministic counterpart, and they can be complemented in polynomial time. Algorithms for constructing the intersection of two Muller automata and for checking language inclusion are known [10].

3 Timed automata

In this section we dene timed words by coupling a real-valued time with each symbol in a word. Then we augment the denition of!-automata so that they accept timed words, and use them to develop a theory of timed regular languages analogous to the theory of

!-regular languages.

3.1 Timed languages

We dene timed words so that a behavior of a real-time system corresponds to a timed word over the alphabet of events. As in the case of the dense-time model, the set of nonnegative real numbers,^R, is chosen as the time domain. A word  is coupled with a time sequence  as dened below:

Denition 3.1

Atime sequence  = ^12


is an innite sequence of time values^{i 2R} with ⁱ > 0, satisfying the following constraints:

1. Monotonicity:  increases strictly monotonically; that is, ⁱ < ⁱ⁺¹ for all i^1.

2. Progress: For everyt ^2R, there is somei^1 such that ⁱ > t.

A timed word over an alphabet  is a pair (;) where  = ¹²::: is an innite word over  and  is a time sequence. Atimed language over  is a set of timed words over .

If a timed word (;) is viewed as an input to an automaton, it presents the symbol

ⁱ at time ⁱ. If each symbol ⁱ is interpreted to denote an event occurrence then the corresponding componentⁱ is interpreted as the time of occurrence of ⁱ. Under certain circumstances it may be appropriate to allow the same time value to be associated with many consecutive events in the sequence. To accommodate this possibility one could use a slightly dierent denition of timed words by requiring a time sequence to increase only monotonically (i.e., require^{i i+1} for alli^1). All our results continue to hold in this alternative model also.

Let us consider some examples of timed languages.

Example 3.2

Let the alphabet be ^fa;b^g. Dene a timed language L¹ to consist of all timed words (;) such that there is no b after time 5:6. Thus the language L¹ is given by L¹ = ^f(;)^j8i:((ⁱ> 5:6) ^! (ⁱ =a))^g:

Another example is the language L² consisting of timed words in whicha and b alter- nate, and for the successive pairs of a and b, the time dierence between a and b keeps increasing. The language L² is given as

L² = ^f((ab)^!;) ^j8i:((^2i?2i?1)< (^2i+2?2i+1))^g: 6

a, x:=0

b, (x<2)?

S0

S1

Figure 3: Example of a timed transition table

The language-theoretic operations such as intersection, union, complementation are dened for timed languages as usual. In addition we dene the Untime operation which discards the time values associated with the symbols, that is, it considers the projection of a timed trace (;) on the rst component.

Denition 3.3

For a timed language L over , Untime(L) is the !-language consisting of  ²^! such that (;)² L for some time sequence .

For instance, referring to Example 3.2, Untime(L¹) is the!-language (a + b)^a^!, and Untime(L²) consists of a single word (ab)^!.

3.2 Transition tables with timing constraints

Now we extend transition tables to timed transition tables so that they can read timed words. When an automaton makes a state-transition, the choice of the next state depends upon the input symbol read. In case of a timed transition table, we want this choice to depend also upon the time of the input symbol relative to the times of the previously read symbols. For this purpose, we associate a nite set of (real-valued) clocks with each transition table. A clock can be set to zero simultaneously with any transition. At any instant, the reading of a clock equals the time elapsed since the last time it was reset.

With each transition we associate a clock constraint, and require that the transition may be taken only if the current values of the clocks satisfy this constraint. Before we dene the timed transition tables formally, let us consider some examples.

Example 3.4

Consider the timed transition table of Figure 3. The start state is s⁰. There is a single clock x. An annotation of the form x := 0 on an edge corresponds to the action of resetting the clockx when the edge is traversed. Similarly an annotation of the form (x < 2)? on an edge gives the clock constraint associated with the edge.

The automaton starts in state s⁰, and moves to state s¹ reading the input symbol a.

The clock x gets set to 0 along with this transition. While in state s¹, the value of the clock x shows the time elapsed since the occurrence of the last a symbol. The transition from state s¹ to s⁰ is enabled only if this value is less than 2. The whole cycle repeats when the automaton moves back to state s⁰. Thus the timing constraint expressed by this transition table is that the delay betweena and the following b is always less than 2;

more formally, the language is

f((ab)^!;) ^j8i:(²ⁱ< ^2i?1+ 2)^g: 7

a b c (x<1)?

d, (y>2)?

x:=0 y:=0

S0

S1 S₂

S3

Figure 4: Timed transition table with 2 clocks

Thus to constrain the delay between two transitions e¹ ande², we require a particular clock to be reset on e¹, and associate an appropriate clock constraint with e². Note that clocks can be set asynchronously of each other. This means that dierent clocks can be restarted at dierent times, and there is no lower bound on the dierence between their readings. Having multiple clocks allows multiple concurrent delays, as in the next example.

Example 3.5

The timed transition table of Figure 4 uses two clocksx and y, and accepts the language

L³ = ^f((abcd)^!;) ^j8j:((^4j+3 < ^4j+1+ 1) ^{^} (^4j+4 > ^4j+2+ 2))^g:

The automaton cycles among the states s⁰, s¹, s² and s³. The clock x gets set to 0 each time it moves from s⁰ to s¹ reading a. The check (x < 1)? associated with the c-transition from s² to s³ ensures that c happens within time 1 of the preceding a. A similar mechanism of resetting another independent clocky while reading b and checking its value while reading d, ensures that the delay between b and the following d is always greater than 2.

Notice that in the above example, to constrain the delay betweena and c and between b and d the automaton does not put any explicit bounds on the time dierence between a and the following b, or c and the following d. This is an important advantage of having multiple clocks which can be set independently of each other. The above language L³ is the intersection of the two languages L¹³ and L²³ dened as

L¹³ = ^f((abcd)^!;)^{j 8}j:(^4j+3< ^4j+1 + 1)^g; L²³ = ^f((abcd)^!;)^{j 8}j:(^4j+4> ^4j+2 + 2)^g:

Each of the languages L¹³ and L²³ can be expressed by an automaton which uses just one clock; however to express their intersection we need two clocks.

We remark that the clocks of the automaton do not correspond to the local clocks of dierent components in a distributed system. All the clocks increase at the uniform rate counting time with respect to a xed global time frame. They are ctitious clocks invented to express the timing properties of the system. Alternatively, we can consider the automaton to be equipped with a nite number of stop-watches which can be started and checked independently of one another, but all stop-watches refer to the same clock.

8

3.3 Clock constraints and clock interpretations

To dene timed automata formally, we need to say what type of clock constraints are allowed on the edges. The simplest form of a constraint compares a clock value with a time constant. We allow only the Boolean combinations of such simple constraints. Any value from ^Q, the set of nonnegative rationals, can be used as a time constant. Later, in Section 5.5, we will show that allowing more complex constraints, such as those involving addition of clock values, leads to undecidability.

Denition 3.6

For a set X of clock variables, the set (X) of clock constraints  is dened inductively by

 := x^ c^jc^ x^j: ^j^{1^}²; where x is a clock in X and c is a constant in ^Q.

Observe that constraints such as

true

, (x = c), x²[2;5) can be dened as abbrevia- tions.

A clock interpretation  for a set X of clocks assigns a real value to each clock; that is, it is a mapping from X to ^R. We say that a clock interpretation  for X satises a clock constraint  over X i  evaluates to true using the values given by .

Fort^2R, +t denotes the clock interpretation which maps every clock x to the value

(x) + t, and the clock interpretation t
 assigns to each clock x the value t
(x). For Y ^ X, [Y ^7! t] denotes the clock interpretation for X which assigns t to each x ²Y , and agrees with  over the rest of the clocks.

3.4 Timed transition tables

Now we give the precise denition of timed transition tables.

Denition 3.7

A timed transition table ^A is a tuple ^h;S;S⁰;C;Eⁱ, where

  is a nite alphabet,

 S is a nite set of states,

 S^{0 }S is a set of start states,

 C is a nite set of clocks, and

 E^ S^S^^2^C(C) gives the set of transitions. An edge ^hs;s⁰;a;;ⁱ represents a transition from state s to state s⁰ on input symbola. The set

 ^ C gives the clocks to be reset with this transition, and  is a clock constraint over C.

Given a timed word (;), the timed transition table^A starts in one of its start states at time 0 with all its clocks initialized to 0. As time advances, the values of all clocks change, re ecting the elapsed time. At timeⁱ, ^A changes state froms to s⁰ using some transition of the form ^hs;s⁰;ⁱ;;ⁱ reading the input ⁱ, if the current values of clocks satisfy. With this transition the clocks in  are reset to 0, and thus start counting time with respect to the time of occurrence of this transition. This behavior is captured by dening runs of timed transition tables. A run records the state and the values of all the clocks at the transition points. For a time sequence = ^12::: we dene ⁰ = 0.

9

Denition 3.8

A runr, denoted by (s;), of a timed transition table^h;S;S⁰;C;Eⁱover a timed word (;) is an innite sequence of the form

r : ^hs⁰;^{0i ?!1} 1

hs¹;^{1i ?!2} 2

hs²;^{2i ?!3} 3

with s^{i 2}S and ^{i 2}[C ^{! R}], for all i^0, satisfying the following requirements:

 Initiation: s⁰² S⁰, and ⁰(x) = 0 for all x²C.

 Consecution: for alli^ 1, there is an edge in E of the form ^hs^i?1;sⁱ;ⁱ;ⁱ;ⁱⁱ such that (^i?1+^i?i?1) satisesⁱ and ⁱ equals [^{i 7!}0](^i?1+^{i ?i?1}).

The setinf(r) consists of those states s²S such that s = sⁱ for innitely manyi^0.

Example 3.9

Consider the timed transition table of Example 3.5. Consider a timed word (a;2) ^! (b;2:7) ^! (c;2:8) ^! (d;5) ^!

Below we give the initial segment of the run. A clock interpretation is represented by listing the values [x;y].

hs⁰;[0;0]^{i ?a!}

2

hs¹;[0;2]^{i ?!b}

2:7

hs²;[0:7;0]^{i ?c!}

2:8

hs³;[0:8;0:1]^{i ?d!}

5

hs⁰;[3;2:3]ⁱ


Along a run r = (s;) over (;), the values of the clocks at time t between ⁱ and

ⁱ⁺¹are given by the interpretation (ⁱ+t^?i). When the transition from statesⁱ to sⁱ⁺¹ occurs, we use the value (ⁱ +^i+1?i) to check the clock constraint; however, at time

ⁱ⁺¹, the value of a clock that gets reset is dened to be 0.

Note that a transition table^A =^h;S;S⁰;Eⁱcan be considered to be a timed transition table^A0. We choose the set of clocks to be the empty set, and replace every edge^hs;s⁰;aⁱ by^hs;s⁰;a;^;;

true

ⁱ. The runs of^A0are in an obvious correspondence with the runs of ^A.

3.5 Timed regular languages

We can couple acceptance criteria with timed transition tables, and use them to dene timed languages.

Denition 3.10

A timed Buchi automaton (in short TBA) is a tuple ^h;S;S⁰;C;E;Fⁱ, where ^h;S;S⁰;C;Eⁱ is a timed transition table, and F^S is a set of accepting states.

A run r = (s;) of a TBA over a timed word (;) is called an accepting run i inf(r)^\F⁶=^;.

For a TBA ^A, the language L(^A) of timed words it accepts is dened to be the set

f(;)^{j A} has an accepting run over (;)^g.

In analogy with the class of languages accepted by Buchi automata, we call the class of timed languages accepted by TBAs timed regular languages.

10

b

a

b,(x<2)?

a, x:=0 a, x:=0

S1 S₀

S2 S₃

Figure 5: Timed Buchi automaton accepting L^crt

Denition 3.11

A timed language L is a timed regular language i L = L(^A) for some TBA^A.

Example 3.12

The language L³ of Example 3.5 is a timed regular language. The timed transition table of Figure 4 is coupled with the acceptance set consisting of all the states.

For every!-regular language L over , the timed language^f(;)^j ²L^g is regular.

A typical exampleof a nonregular timed language is the languageL²of Example 3.2. It requires that the time dierence between the successive pairs ofa and b form an increasing sequence.

Another nonregular language is ^f(a^!;)^j8i:(ⁱ= 2ⁱ)^g.

The automaton of Example 3.13 combines the Buchi acceptance condition with the timing constraints to specify an interesting convergent response property:

Example 3.13

The automaton of Figure 5 accepts the timed language L^crt over the alphabet ^fa;b^g.

L^crt = ^f((ab)^!;)^j9i:⁸j^i:(^2j < ^2j?1+ 2)^g:

The start state is s⁰, the accepting state is s², and there is a single clock x. The automaton starts in state s⁰, and cycles between the states s⁰ and s¹ for a while. Then, nondeterministically, it moves to state s² setting its clock x to 0. While in the cycle between the states s² and s³, the automaton resets its clock while reading a, and ensures that the nextb is within 2 time units. Interpreting the symbol b as a response to a request denoted by the symbola, the automaton models a system with aconvergent response time; the response time is \eventually" always less than 2 time units.

The next example shows that timed automata can specify periodic behavior also.

Example 3.14

The automaton of Figure 6 accepts the following language over the al- phabet ^fa;b^g.

f(;)^j8i:⁹j:(^j = 3i ^{^} ^j =a)^g

The automaton has a single state s⁰, and a single clock x. The clock gets reset at regular intervals of period 3 time units. The automaton requires that whenever the clock equals 3 there is an a symbol. Thus it expresses the property that a happens at all time values that are multiples of 3.

11

a,b,(x<3)?

a,(x=3)?,x:=0 S₀

Figure 6: Timed automaton specifying periodic behavior

3.6 Properties of timed regular languages

The next theorem considers some closure properties of timed regular languages.

Theorem 3.15

The class of timed regular languages is closed under (nite) union and intersection.

Proof. Consider TBAs ^Ai = ^h;Sⁱ;Sⁱ⁰;Cⁱ;Eⁱ;Fⁱⁱ, i = 1;2;:::n. Assume without loss of generality that the clock sets Cⁱ are disjoint. We construct TBAs accepting the union and intersection of L(^Ai).

Since TBAs are nondeterministicthe case of union is easy. The required TBA is simply the disjoint union of all the automata.

Intersection can be implemented by a trivial modication of the standard product construction for Buchi automata [9]. The set of clocks for the product automaton ^A is

[

iCⁱ. The states of^Aare of the form^hs¹;:::sⁿ;kⁱ, where eachs^{i 2}Sⁱ, and 1^k ^n. The i-th component of the tuple keeps track of the state of^Ai, and the last component is used as a counter for cycling through the accepting conditions of all the individual automata.

Initially the counter value is 1, and it is incremented from k to (k + 1) (modulo n) i the current state of the k-th automaton is an accepting state. Note that we choose the value of n mod n to be n.

The initial states of ^A are of the form ^hs¹;:::sⁿ;1ⁱ where each sⁱ is a start state of

A

i. A transition of ^A is obtained by coupling the transitions of the individual automata having the same label. Let ^fhsⁱ;s⁰ⁱ;a;ⁱ;ⁱⁱ²E^{i j}i = 1;:::n^g be a set of transitions, one per each automaton, with the same label a. Corresponding to this set, there is a joint transition of ^A out of each state of the form^hs¹;:::sⁿ;kⁱ labeled with a. The new state is ^hs⁰¹;:::s⁰ⁿ;jⁱ with j = (k + 1) mod n if s^{k 2}F^k, and j = k otherwise. The set of clocks to be reset with this transition is ^[iⁱ, and the associated clock constraint is^{^i}ⁱ.

The counter value cycles through the whole range 1;:::n innitely often i the ac- cepting conditions of all the automata are met. Consequently, we dene the accepting set for ^A to consist of states of the form ^hs¹;:::sⁿ;nⁱ, wheresⁿ²Fⁿ.

In the above product construction, the number of states of the resulting automaton is n
^ijS^ij. The number of clocks is ^ijC^ij, and the size of the edge set isn
^ijE^ij. Note that ^jE^j includes the length of the clock constraints assuming binary encoding for the constants.

12

b (x=1)?

a,x:=0

y:=0

a,(x=1)?,x:=0

b,(y<1)?,y:=0

S₀ S₁ S₂ S₃

Figure 7: Timed automaton accepting Lconverge

Observe that even for the timed regular languages arbitrarily many symbols can occur in a nite interval of time. Furthermore, the symbols can be arbitrarily close to each other. Consider the following example.

Example 3.16

The language accepted by the automaton in Figure 7 is

Lconverge = ^f((ab)^!;) ^j8i:(^2i?1=i ^{^} (^2i?2i?1 > ^2i+2?2i+1))^g:

Every word accepted by this automaton has the property that the sequence of time dierences between a and the following b is strictly decreasing. A sample word accepted by the automaton is

(a;1) ^! (b;1:5) ^! (a;2) ^! (b;2:25) ^! (a;3) ^! (b;3:125) ^!

This example illustrates that the model of reals is indeed dierent from the discrete- time model. If we require all the time values ⁱ to be multiples of some xed constant , however small, the language accepted by the automaton of Figure 7 will be empty.

On the other hand, timed automata do not distinguish between the set of reals ^R and the set of rationals ^Q. Only the denseness of the underlying domain plays a crucial role.

In particular, Theorem 3.17 shows that if we require all the time values in time sequences to be rational numbers, the untimed language Untime[L(^A)] of a timed automaton ^A stays unchanged.

Theorem 3.17

LetL be a timed regular language. For every word , ²Untime(L) i there exists a time sequence  such that ^{i 2Q} for all i^ 1, and (;)²L.

Proof. Consider a timed automaton^A, and a word. If there exists a time sequence

 with all rational time values such that (;)²L(^A), then clearly, ²Untime[L(^A)].

Now suppose for an arbitrary time sequence, (;)²L(^A). Let ^2Q be such that every constant appearing in the clock constraints of ^A is an integral multiple of . Let

⁰⁰ = 0, and⁰ = 0. Ifⁱ =^j+n for some 0^j < i and n ^2N, then choose ⁱ⁰=^j0+n.

Otherwise choose ^{i0 2 Q} such that for all 0 ^ j < i, for all n ^{2 N}, (^i0?j0) < n i (^{i ? j}) < n. Note that because of the denseness of ^Q such a choice of ⁱ⁰ is always possible.

Consider an accepting run r = (s;) of ^A over (;). Because of the construction of

⁰, if a clock x is reset at the i-th transition point, then its possible values at the j-th 13

a,(x<5)? a,(x<2)?

b,x:=0 c,x:=0

S1 S₀

S2

Figure 8: Timed Muller automaton

transition point along the two time sequences, namely, (^{j ?i}) and (^j0?i0), satisfy the same set of clock constraints. Consequently it is possible to construct an accepting run r⁰ = (s;⁰) over (;⁰) which follows the same sequence of edges asr. In particular, choose

⁰⁰ =⁰, and if thei-th transition along r is according to the edge ^hs^i?1;sⁱ;ⁱ;ⁱ;ⁱⁱ, then setⁱ⁰= [^{i 7!}0](^i?10 +^i0?i?10 ). Consequently, ^A accepts (;⁰).

3.7 Timed Muller automata

We can dene timed automata with Muller acceptance conditions also.

Denition 3.18

A timed Muller automaton (TMA) is a tuple ^h;S;S⁰;C;E;^Fi, where

h;S;S⁰;C;Eⁱ is a timed transition table, and ^{F }2^S species an acceptance family.

A run r = (s;) of the automaton over a timed word (;) is an accepting run i inf(r)^2F.

For a TMA ^A, the language L(^A) of timed words it accepts is dened to be the set

f(;)^{j A} has an accepting run over (;)^g.

Example 3.19

Consider the automaton of Figure 8 over the alphabet ^fa;b;c^g. The start state iss⁰, and the Muller acceptance family consists of a single set^fs⁰;s^2g. So any accepting run should cycle between statess⁰ ands¹ only nitely many times, and between states s⁰ and s² innitely many times. Every word (;) accepted by the automaton satises: (1)²(a(b+c))^(ac)^!, and (2) for alli^1, the dierence (^2i?1?2i?2) is less than 2 if the (2i)-th symbol is c, and less than 5 otherwise.

Recall that untimed Buchi automata and Muller automata have the same expressive power. The following theorem states that the same holds true for TBAs and TMAs. Thus the class of timed languages accepted by TMAs is the same as the class of timed regular languages. The proof of the following theorem closely follows the standard argument that an !-regular language is accepted by a Buchi automaton i it is accepted by some Muller automaton.

Theorem 3.20

A timed language is accepted by some timed Buchi automaton i it is accepted by some timed Muller automaton.

Proof. Let ^A = ^h;S;S⁰;C;E;Fⁱ be a TBA. Consider the TMA ^A0 with the same timed transition table as that of^A, and with the acceptance family^F =^fS^0 S : S^0\F⁶=

;g. It is easy to check that L(^A) =L(^A0). This proves the \only if" part of the claim.

14

In the other direction, given a TMA, we can construct a TBA accepting the same language using the simulation of Muller acceptance condition by Buchi automata. Let

A be a TMA given as ^h;S;S⁰;C;E;^Fi. First note that L(^A) = ^[F2FL(^AF) where

A

F = ^h;S;S⁰;C;E;^fF^gi, so it suces to construct, for each acceptance set F, a TBA

A 0

F which accepts the language L(^AF). Assume F = ^fs¹;:::s^kg. The automaton ^A0F uses nondeterminism to guess when the set F is entered forever, and then uses a counter to make sure that every state in F is visited innitely often. States of ^A0F are of the form ^hs;iⁱ, where s ² S and i ^{2 f}0;1;:::k^g. The set of initial states is S^{0 f}0^g. The automaton simulates the transitions of ^A, and at some point nondeterministically sets the second component to 1. For every transition ^hs;s⁰;a;;ⁱ of ^A, the automaton ^A0F has a transition ^hhs;0ⁱ;^hs⁰;0ⁱ;a;;ⁱ, and, in addition, if s^{0 2} F it also has a transition

hhs;0ⁱ;^hs⁰;1ⁱ;a;;ⁱ.

While the second component is nonzero, the automaton is required to stay within the set F. For every ^A-transition ^hs;s⁰;a;;ⁱ with both s and s⁰ in F, for each 1 ^ i ^ k, there is an ^A0F-transition ^hhs;iⁱ;^hs⁰;jⁱ;a;;ⁱ wherej = (i+1) mod k, if s equals sⁱ, else j = i. The only accepting state is ^hs^k;kⁱ.

4 Checking emptiness

In this section we develop an algorithm for checking the emptiness of the language of a timed automaton. The existence of an innite accepting path in the underlying transition table is clearly a necessary condition for the language of an automaton to be nonempty.

However, the timing constraints of the automaton rule out certain additional behaviors.

We will show that a Buchi automaton can be constructed that accepts exactly the set of untimed words that are consistent with the timed words accepted by a timed automaton.

4.1 Restriction to integer constants

Recall that our denition of timed automata allows clock constraints which involve com- parisons with rational constants. The following lemmashows that, for checking emptiness, we can restrict ourselves to timed automata whose clock constraints involve only integer constants. For a timed sequence and t^2Q, lett
 denote the timed sequence obtained by multiplying all ⁱ byt.

Lemma 4.1

Consider a timed transition table ^A, a timed word (;), and t^2Q. (s;) is a run of ^A over (;) i (s;t
) is a run of ^At over (;t
), where ^At is the timed transition table obtained by replacing each constant d in each clock constraint labeling the edges of ^A by t
d.

Proof. The lemma can be proved easily from the denitions using induction.

Thus there is an isomorphism between the runs of ^A and the runs of^At. If we choose t to be the least common multiple of denominators of all the constants appearing in the clock constraints of^A, then the clock constraints for^Atuse only integer constants. In this translation, the values of the individual constants grow at most with the product of the denominators of all the original constants. We assume binary encoding for the constants.

15

Let us denote the length of the clock constraints of ^A by^j(^A)^j. It is easy to prove that

j(^At)^jis bounded by ^j(^A)^j2. Observe that this result depends crucially on the fact that we encode constants in binary notation; if we use unary encoding then ^j(^At)^j can be exponential in^j(^A)^j.

Observe that L(^A) is empty i L[^At] is empty. Hence, to decide the emptiness of L(^A) we consider ^At. Also Untime[L(^A)] equals Untime[L(^At)]. In the remainder of the section we assume that the clock constraints use only integer constants.

4.2 Clock regions

At every point in time the future behavior of a timed transition table is determined by its state and the values of all its clocks. This motivates the following denition:

Denition 4.2

For a timed transition table ^h;S;S⁰;C;Eⁱ, an extended state is a pair

hs;ⁱ wheres ²S and is a clock interpretation for C.

Since the number of such extended states is innite (in fact, uncountable), we cannot possibly build an automaton whose states are the extended states of ^A. But if two extended states with the same^A-state agree on the integral parts of all clock values, and also on the ordering of the fractional parts of all clock values, then the runs starting from the two extended states are very similar. The integral parts of the clock values are needed to determine whether or not a particular clock constraint is met, whereas the ordering of the fractional parts is needed to decide which clock will change its integral part rst. For example, if two clocksx and y are between 0 and 1 in an extended state, then a transition with clock constraint (x = 1) can be followed by a transition with clock constraint (y = 1), depending on whether or not the current clock values satisfy (x < y).

The integral parts of clock values can get arbitrarily large. But if a clock x is never compared with a constant greater thanc, then its actual value, once it exceeds c, is of no consequence in deciding the allowed paths.

Now we formalize this notion. For any t^2R, fract(t) denotes the fractional part of t, and ^bt^c denotes the integral part of t; that is, t =^bt^c+fract(t). We assume that every clock in C appears in some clock constraint.

Denition 4.3

Let^A =^h;S;S⁰;C;Eⁱ be a timed transition table. For each x²C, let c^x be the largest integer c such that (x ^ c) or (c ^ x) is a subformula of some clock constraint appearing in E.

The equivalence relation ^ is dened over the set of all clock interpretations for C;

^⁰ i all the following conditions hold:

1. For all x ² C, either ^b(x)^c and ^b⁰(x)^c are the same, or both (x) and ⁰(x) are greater than c^x.

2. For all x;y²C with(x) ^c^x and (y)^c^y,fract((x))^fract((y)) i fract(⁰(x))^fract(⁰(y)).

3. For all x²C with(x) ^c^x, fract((x)) = 0 i ^fract(⁰(x)) = 0.

A clock region for ^A is an equivalence class of clock interpretations induced by ^. 16