and third components give the values of clocks x and y, respectively. This execution corresponds to a delay of 1.3 time units in 0, the firing of transition a (which is enabled because the value of clock x is less than two; clock y is then set to 0), the firing of transition c (which occurs without delay as 1 is urgent), etc.

In the context of verification, several problems are of interest, like the model-checking of safety properties (“Can a distinguished set of states be avoided?”), reachability/liveness properties (“Can/will a distinguished goal state be reached?”), or more involved properties such as response properties (“Is any request eventually granted?”). As a model for real-time systems, these properties can include quantitative constraints, for instance time-bounded reachability, or time-bounded response properties (“Is any request granted within two minutes?”). It is also relevant to compute optimal time bounds for these properties, for example, optimal-time reachability (“What is the minimum time required for reaching a distinguished set of states?”).

The region abstraction. A timed automaton is a syntactical representation of an infinite transition system, since clocks take (nonnegative) real values. However, there is a way to deal with this infinity of configurations by reasoning symbolically: the main theoretical ingredient for solving problems on timed automata is the notion of regions,5 which provide a finite partition-

ing of the state space such that states within a given region are bisimilar, that is, behaviorally indistinguishable.

The precise definition of regions is such that inside a region, integral parts of clock values do not change, and also the ordering of clocks according to their values’ fractional parts stays the same. Special consideration has to be given to the cases where one or more clock values are integers, and finiteness of the region partitioning is ensured by considering as equivalent all clock values that exceed the maximal constant appearing in guards and invariants of the timed automaton in question. In the left part of Figure 2 we show the 44 regions for two clocks x and y with maximal constant equal to two. In this two-clock case, regions can be points (both clocks have integer values), open line segments (one clock has integer value, or their fractional parts are equal), open triangles, or open unbounded rectangles.

From two equivalent configurations (same location, region equivalent valuations), by delaying or by taking a transition, similar regions will be visited and similar behaviors will be possible. Regions are thus a way to finitely abstract the behaviors of a timed automaton. There are finitely many regions, and by considering as abstract configurations pairs of locations and regions, we get a finite automaton, called the region automaton, which preserves many properties including reachability, liveness, and safety.

Hence, verification of those properties on the original timed automaton can be transferred to the finite region automaton and then checked using standard algorithms.

The limits of the region abstraction. Not all properties can be decided on timed automata using the region abstraction, and problems such as checking inclusion (“Are all real-time behaviors of a timed automaton also behaviors of another timed automaton?”) and universality (“Can all real-time behaviors be realized in a given timed automaton?”) are undecidable.

Also, the set of real-time behaviors exhibited by timed automata is not closed under complement, and not all timed automata are determinizable. As a counterexample for these properties, one can use the following timed automaton:

 

:=0

=1

0;

1;

 

It accepts all behaviors with at least two a’s separated by one time unit. It can be shown that no deterministic timed automaton exists with exactly the same behaviors, and also that no timed automaton can implement precisely all complementary behaviors.

Timed automata in practice. The region abstraction is a powerful tool for showing decidability of a number of interesting properties, but unfortunately, the region-based verification algorithms introduced above are

figure 2. The region abstraction is a finite representation of all possible behaviors of the timed automaton. consider the timed automaton on top of the picture, and assume we enter location 1 with clock values (x0, y0) for which 0 < y0 < x0 < 1 (a point in the red triangle, see the picture on the left); as clock y has value strictly less than 1, we have the option to switch to location 2, which would reset clock x and end up in the purple region. We also have the option to delay in 1; in that case, we exit the red triangle and reach the orange line. here again we have two options: switching to 2, or delaying to the yellow clock region. in case we still decide to wait in that region, we reach the green line. from that region on, the transition to 2 is not enabled anymore. this description of the possible behaviors starting from the red region, which has been represented on the picture to the right, does not depend on the precise values of the clocks: region equivalence preserves enough information to encode exactly the behaviors of the underlying timed automaton.