Computing Accumulated Delays in Real-time Systems.
We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number the duration of the run which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.
Introduction
Over the past decade, model checking [CE81, QS81] has emerged as a powerful tool for the automatic
verification of finite-state systems. Recently the model-checking paradigm has been extended to
real-time systems [ACD93, HNSY94, AFH96]. Thus, given the description of a finite-state system
together with its timing assumptions, there are algorithms that test whether the system satisfies
a specification written in a real-time temporal logic. A typical property that can be specified in
real-time temporal logics is the following time-bounded causality property:
A response is obtained whenever a ringer has been pressed continuously for 2 seconds.
Standard real-time temporal logics [AH92], however, have limited expressiveness and cannot specify
some timing properties we may want to verify of a given system. In particular, they do not allow
us to constrain the accumulated satisfaction times of state predicates. As an example, consider the
following duration-bounded causality property:
A response is obtained whenever a ringer has been pressed, possibly intermittently, for
a total duration of 2 seconds. ( )
A preliminary version of this paper appeared in the Proceedings of the Fifth International Conference on
Computer-Aided Verification (CAV 93), Springer-Verlag LNCS 818, pp. 181-193, 1993.
y Bell Laboratories, Murray Hill, New Jersey, U.S.A.
z Department of Computer Science, University of Crete, and Institute of Computer Science, FORTH, Greece.
Partially supported by the BRA ESPRIT project REACT.
x Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, U.S.A. Partially
supported by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the
NSF grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056, and by the ARPA grant
NAG2-892.
To specify this duration property, we need to measure the accumulated time spent in the state
that models "the ringer is pressed." For this purpose, the concept of duration operators on state
predicates is introduced in the Calculus of Durations [CHR91]. There, an axiom system is given
for proving duration properties of real-time systems.
Here we address the algorithmic verification problem for duration properties of real-time sys-
tems. We use the formalism of timed automata [AD94] for representing real-time systems. A timed
automaton operates with a finite control and a finite number of fictitious time gauges called clocks,
which allow the annotation of the control graph with timing constraints. The state of a timed
automaton includes, apart from the location of the control, also the real-numbered values of all
clocks. Consequently, the state space of a timed automaton is infinite, and this complicates its
analysis. The basic question about a timed automaton is the following time-bounded reachability
problem:
Given an initial state oe, a final state - , and an interval I , is there a run of the automaton
starting in state oe and ending in state - such that the total elapsed time of the run is
in the interval I? (y)
The solution to this problem relies on a partition of the infinite state space into finitely many regions,
which are connected with transition and time edges to form the region graph of the timed automaton
[AD94]. The states within a region are equivalent with respect to many standard questions. In
particular, the region graph can be used for testing the emptiness of a timed automaton [AD94], for
checking time-bounded branching properties [ACD93], for testing the bisimilarity of states [Cer92],
and for computing lower and upper bounds on time delays [CY91]. Unfortunately, the region graph
is not adequate for checking duration properties such as the duration-bounded causality property
( ); that is, of two runs that start in different states within the same region, one may satisfy the
duration-bounded causality property, whereas the other one does not. Hence a new technique is
needed for analyzing duration properties.
To introduce the concept of durations in a timed automaton, we associate with every finite
run a nonnegative real number, which is called the duration of the run. The duration of a run is
defined inductively using a duration measure, which is a function that maps the control locations
to nonnegative integers: the duration of an empty run is 0; and the duration measure of a location
gives the rate at which the duration of a run increases while the automaton control resides in
that location. For example, a duration measure of 0 means that the duration of the run stays
unchanged (i.e., the time spent in the location is not accumulated), a duration measure of 1 means
that the duration of the run increases at the rate of time (i.e., the time spent in the location
is accumulated), and a duration measure of 2 means that the duration of the run increases at
twice the rate of time. The time-bounded reachability problem (y) can now be generalized to the
duration-bounded reachability problem:
Given an initial state oe, a final state - , a duration measure, and an interval I , is there
a run of the automaton starting in state oe and ending in state - such that the duration
of the run is in the interval I?
We show that the duration-bounded reachability problem is Pspace-complete, and we provide an
optimal solution. Our algorithm can be used to verify duration properties of real-time systems that
are modeled as timed automata, such as the duration-bounded causality property ( ).
Let us briefly outline our construction. Given a region R, a final state - , and a path in the
region graph from R to - , we show that the lower and upper bounds on the durations of all runs
that start at some state in R and follow the chosen path can be written as linear expressions over
the variables that represent the clock values of the start state. In a first step, we provide a recipe
for computing these so-called bound expressions. In the next step, we define an infinite graph,
the bounds graph, whose vertices are regions tagged with bound expressions that specify the set of
possible durations for any path to the final state. In the final step, we show that the infinite bounds
graph can be collapsed into a finite graph for solving the duration-bounded reachability problem.
2 The Duration-bounded Reachability Problem
Timed automata
Timed automata are a formal model for real-time systems [Dil89, AD94]. Each automaton has a
finite set of control locations and a finite set of real-valued clocks. All clocks proceed at the same
rate, and thus each clock measures the amount of time that has elapsed since it was started. A
transition of a timed automaton can be taken only if the current clock values satisfy the constraint
that is associated with the transition. When taken, the transition changes the control location of
the automaton and restarts one of the clocks.
Formally, a timed automaton A is a triple (S; X; E) with the following components:
ffl S is a finite set of locations ;
ffl X is a finite set of clocks ;
ffl E is a finite set of transitions of the form (s; t; '; x), for a source location s 2 S, a target
location t 2 S, a clock constraint ', and a clock x 2 X . Each clock constraint is a positive
boolean combination of atomic formulas of the form y - k or y ! k or k - y or k ! y, for a
clock y 2 X and a nonnegative integer constant k 2 N.
A configuration of the timed automaton A is fully described by specifying the location of the control
and the values of all clocks. A clock valuation c 2 R X is an assignment of nonnegative reals to the
clocks in X . A state oe of A is a pair (s; c) consisting of a location s 2 S and a clock valuation c.
We write \Sigma for the (infinite) set of states of A. As time elapses, the values of all clocks increase
uniformly with time, thereby changing the state of A. Thus, if the state of A is (s; c), then after
time assuming that no transition occurs, the state of A is (s; c is the
clock valuation that assigns c(x) + ffi to each clock x. The state of A may also change because of
a transition (s; t; '; x) in E. Such a transition can be taken only in a state whose location is s
and whose clock valuation satisfies the constraint '. The transition is instantaneous. After the
transition, the automaton is in a state with location t and the new clock valuation is c[x := 0]; that
is, the clock x associated with the transition is reset to the value 0, and all other clocks remain
unchanged.
The possible behaviors of the timed automaton A are defined through a successor relation on
the states of A:
Transition successor For all states (s; c) 2 \Sigma and transitions (s; t; '; x) 2 E, if c satisfies ', then
(s; c) 0
Time successor For all states (s; c) 2 \Sigma and time increments
A state (t; d) is a successor of the state (s; c), written (s; c) ! (t; d), iff there exists a nonnegative
real ffi such that (s; c) ffi
d). The successor relation defines an infinite graph K(A) on the state
space \Sigma of A. The transitive closure !   of the successor relation ! is called the reachability
relation of A.
s
(y - 2; y)

Figure

1: Sample timed automaton
Example 1 A sample timed automaton is shown in Figure 1. The automaton has four locations
and two clocks. Each edge is labeled with a clock constraint and the clock to be reset. A state of
the automaton contains a location and real-numbered values for the clocks x and y. Some sample
pairs in the successor relation are shown below:
(s; 0;
0):Depending on the application, a timed automaton may be augmented with additional components
such as initial locations, accepting locations, transition labels for synchronization with other timed
automata, and atomic propositions as location labels. It is also useful to label each location with a
clock constraint that limits the amount of time spent in that location [HNSY94]. We have chosen a
very simple definition of timed automata to illustrate the essential computational aspects of solving
reachability problems. Also, the standard definition of a timed automaton allows a (possibly empty)
set of clocks to be reset with each transition. Our requirement that precisely one clock is reset with
each transition does not affect the expressiveness of timed automata.
Clock regions and the region graph
Let us review the standard method for analyzing timed automata. The key to solving many
verification problems for a timed automaton is the construction of the so-called region graph [AD94].
The region graph of a timed automaton is a finite quotient of the infinite state graph that retains
enough information for answering certain reachability questions.
Suppose that we are given a timed automaton A and an equivalence relation - = on the states
\Sigma of A. For oe 2 \Sigma, we write for the equivalence class of states that contains the state
oe. The successor relation ! is extended to -equivalence classes as follows: define
there is a state oe 0 2 nonnegative real ffi such that oe 0 ffi
nonnegative reals " ! ffi, we have (oe The quotient graph of A with respect to
the equivalence relation - =, written is a graph whose vertices are the -equivalence classes
and whose edges are given by the successor relation ! . The equivalence relation - = is stable iff
there is a state - 0 2
is back stable iff whenever oe ! - , then for all states - there is a state oe 0 2
. The quotient graph with respect to a (back) stable equivalence relation can be used for
solving the reachability problem between equivalence classes: given two -equivalence classes R 0
and R f , is there a state oe 2 R 0 and a state - 2 R f such that oe !   -? If the equivalence relation
is (back) stable, then the answer to the reachability problem is affirmative iff there is a path from
R 0 to R f in the quotient graph
The region graph of the timed automaton A is a quotient graph of A with respect to the
equivalence relation defined below. For x 2 X , let m x be the largest constant that the
clock x is compared to in any clock constraint of A. For denote the integral part of ffi,
and let -
denote the fractional part of ffi (thus,
We freely use constraints like -
for a clock x and a nonnegative integer constant k (e.g., a clock valuation c satisfies the
constraint bxc - k iff bc(x)c - k). Two states (s; c) and (t; d) of A are region-equivalent, written
(s; c) - (t; d), iff the following four conditions hold:
1.
2. for each clock x 2 X , either
3. for all clocks x; y 2 X , the valuation c satisfies -
the valuation d satisfies -
4. for each clock x 2 X , the valuation c satisfies - the valuation d satisfies -
A (clock) region R ' \Sigma is a -equivalence class of states. Hence, a region is fully specified by
a location, the integral parts of all clock values, and the ordering of the fractional parts of the
clock values. For instance, if X contains three clocks, x, y, and z, then the region
contains all states (s; c) such that c satisfies
z ! 1. For the region R, we write [s;
z], and we say
that R has the location s and satisfies the constraints etc. There are only finitely many
regions, because the exact value of the integral part of a clock x is recorded only if it is smaller than
. The number of regions is bounded by jSj is the number
of clocks. The region graph R(A) of the timed automaton A is the (finite) quotient graph of A
with respect to the region equivalence relation -. The region equivalence relation - is stable as
well as back-stable [AD94]. Hence the region graph can be used for solving reachability problems
between regions, and also for solving time-bounded reachability problems [ACD93].
It is useful to define the edges of the region graph explicitly. A region R is a boundary region
iff there is some clock x such that R satisfies the constraint -
region that is not a boundary
region is called an open region. For a boundary region R, we define its predecessor region pred(R)
to be the open region Q such that for all states (s; c) 2 Q, there is a time increment ffi 2 R such
that (s; c and for all nonnegative reals Similarly, we define
the successor region succ(R) of R to be the open region Q 0 such that for all states (s; c) 2 Q
there is a time increment ffi 2 R such that (s; and for all nonnegative reals
we have (s; . The state of a timed automaton belongs to a boundary region R only
instantaneously. Just before that instant the state belongs to pred(R), and just after that instant
the state belongs to succ(R). For example, for the boundary region R given by
pred(R) is the open region
and succ(R) is the open region
z]:
The edges of the region graph R(A) fall into two categories:
Transition edges If (s; c) 0
then there is an edge from the region [s; c] - to the region [t; d] - .
Time edges For each boundary region R, there is an edge from pred(R) to R, and an edge from
R to succ(R).
In addition, each region has a self-loop, which can be ignored for solving reachability problems.
Duration measures and duration-bounded reachability
A duration measure for the timed automaton A is a function p from the locations of A to the
nonnegative integers. A duration constraint for A is of the form
R
is a duration
measure for A and I is a bounded interval of the nonnegative real line whose endpoints are integers
may be open, half-open, or closed).
Let p be a duration measure for A. We extend the state space of A to evaluate the integral
R
along the runs of A. An extended state of A is a pair (oe; ") consisting of a state oe of A and a
nonnegative real number ". The successor relation on states is extended as follows:
Transition successor For all extended states (s; c; ") and all transitions (s; t; '; x) such that
c satisfies ', define (s; c; '') 0
Time successor For all extended states (s; c; ") and all time increments
(s; c; ") ffi
We consider the duration-bounded reachability problem between regions: given two regions R 0 and
R f of a timed automaton A, and a duration constraint
R
I for A, is there a state oe 2 R 0 , a state
nonnegative real I such that (oe; We refer to this duration-bounded
reachability problem using the tuple
R
Example 2 Recall the sample timed automaton from Figure 1. Suppose that the duration measure
p is defined by 1. Let the initial region R 0 be the singleton
let the final region R f be f(s; 0)g. For the duration constraint
R
the answer to the duration-bounded reachability problem is in the affirmative, and the
following sequence of successor pairs is a justification (the last component denotes the value of the
integral R
(s; 0; 0;
On the other hand, for the duration constraint R
the answer to the duration-bounded
reachability problem is negative. The reader can verify that if (s; 0; 0;
2. 2
If the duration measure p is the constant function 1 (i.e., locations s), then
the integral
R
measures the total elapsed time, and the duration-bounded reachability problem
between regions is called a time-bounded reachability problem. In this case, if (oe;
some I , then for all states oe 0 2 [oe] - there is a state - 0 2 [- and a real number I such that
Hence, the region graph suffices to solve the time-bounded reachability problem.
This, however, is not true for general duration measures.
3 A Solution to the Duration-bounded Reachability Problem
Bound-labeled regions and the bounds graph
Consider a timed automaton A, two regions R 0 and R f , and a duration measure p. We determine
the set I of possible values of ffi such that (oe; To compute
the lower and upper bounds on the integral
R
along a path of the region graph, we refine the graph
by labeling all regions with expressions that specify the extremal values of the integral.
We define an infinite graph with vertices of the form (R; L; l; U; u), where R is a region, L and
U are linear expressions over the clock variables, and l and u are boolean values. The intended
meaning of the bound expressions L and U is that in moving from a state (s; c) 2 R to a state
in the final region R f , the set of possible values of the integral
R
p has the infimum L and the
supremum U , both of which are functions of the current clock values c. If the bit l is 0, then the
infimum L is included in the set of possible values of the integral, and if l is 1, then L is excluded.
Similarly, if the bit u is 0, then the supremum U is included in the set of possible values of R
and if u is 1, then U is excluded. For example, if then the left-closed right-open
interval [L; U) gives the possible values of the integral R
p.
The bound expressions L and U associated with the region R have a special form. Suppose
that is the set of clocks and that for all states (s; c) 2 R, the clock valuation c
is the clock with the smallest fractional part in R, and
x n is the clock with the largest fractional part. The fractional parts of all n clocks partition the
unit interval into represented by the expressions e
x
x n .
A bound expression for R is a positive linear combination of the expressions e that is, a
bound expression for R has the form a 0 are nonnegative integer
constants. We denote bound expressions by (n + 1)-tuples of coefficients and write (a
the bound expression a . For a bound expression e and a clock valuation c,
we to denote the result of evaluating e using the clock values given by c. When time
advances, the value of a bound expression changes at the rate a 0 \Gamma a n . If the region R satisfies
the constraint -
is a boundary region), then the coefficient a 0 is irrelevant, and if R
then the coefficient a i is irrelevant. Henceforth, we assume that all irrelevant
coefficients are set to 0.
A bound-labeled region (R; L; l; U; u) of the timed automaton A consists of a clock region R of
A, two bound expressions L and U for R, and two bits l; u 2 f0; 1g. We construct B p;R f
(A), the
bounds graph of A for the duration measure p and the final region R f . The vertices of B p;R f (A) are
the bound-labeled regions of A and the special vertex R f , which has no outgoing edges. We first
define the edges with the target R f , and then the edges between bound-labeled regions.
The edges with the target R f correspond to runs of the automaton that reach a state in R f
without passing through other regions. Suppose that R f is an open region with the duration
measure a (i.e., a for the location s of R f ). The final region R f is reachable from a state
(s; c) 2 R f by remaining in R f for at least 0 and at most
units. Since the integral
R
p increases at the rate a, the lower bound on the integral value over all states (s; c) 2 R f is 0,
z -
x
a 1 a 2 a 3 a 1 a 2 a 3 a 1 + a

Figure

2:
and the upper bound is a
While the lower bound 0 is a possible value of the integral, if
a ? 0, then the upper bound is only a supremum of all possible values. Hence, we add an edge in
the bounds graph to R f from (R f ; L; 0; U; u) for
if
If R f is a boundary region, no time can be spent in R f , and both bounds are 0. In this case, we
add an edge to R f from (R f ; L; 0; U;
Now let us look at paths that reach the final region R f by passing through other regions. For
each edge from R to R 0 in the region graph R(A), the bounds graph B p;R f (A) has exactly one edge
to each bound-labeled region of the form (R bound-labeled region of the
form (R; L; l; U; u). First, let us consider an example to understand the determination of the lower
bound L and the corresponding bit l (the upper bound U and the bit u are determined similarly).
Suppose that and that the boundary region R 1 , which satisfies
labeled with the lower bound L and the bit l 1 . This means that starting from a
state (s; c) 2 R 1 , the lower bound on the integral R
reaching some state in R f is
Consider the open predecessor region R 2 of R 1 , which satisfies
x. Let a be the duration
measure of R 2 . There is a time edge from R 2 to R 1 in the region graph. We want to compute the
lower-bound label L 2 for R 2 from the lower-bound label L 1 of R 1 . Starting in a state (s; c) 2 R 2 ,
the state (s; c reached after time
Furthermore, from the state (s; c) 2 R 2 the integral R
p has the value [[a
before entering
the region R 1 . Hence, the new lower bound is
and the label L 2 is (a 1 ; a 2 ; a 3 ; a 1 +a). See Figure 2. Whether the lower bound L 2 is a possible value
of the integral depends on whether the original lower bound L 1 is a possible value of the integral
starting in R 1 . Thus, the bit l 2 labeling R 2 is the same as the bit l 1 labeling R 1 .
Next, consider the boundary region R 3 such that R 2 is the successor region of R 3 . The region
x, and there is a time edge from R 3 to R 2 in the region graph. The reader
can verify that the updated lower-bound label L 3 of R 3 is the same as L 2 , namely (a 1 ; a 2 ; a 3 ; a 1 +a),
which can be simplified to (0; a region. See Figure 3. The
updated bit l 3 of R 3 is the same as l 2 .
z - x
y
a 1 a 2 a 1 + a
a 3 a 2 a 3 a 1 + a

Figure

3: (0 ! -
z -
x
immediate:
delayed:
a 2 a 3 a 1 + a
a 2
a 2
a 3 a 3
a 3 a 3

Figure

4:
The process repeats if we consider further time edges, so let us consider a transition edge from
region R 4 to region R 3 , which resets the clock y. We assume that the region R 4 is open with
duration measure b, and that R 4 satisfies
x. Consider a state (t; d) 2 R 4 . Suppose
that the transition happens after time ffi; then
. If the state after the transition is
(s; c) 2 R 3 , then
ffi. The lower bound L 4 corresponding
to this scenario is the value of the integral before the transition, which is b \Delta ffi, added to the value
of the lower bound L 3 at the state (s; c), which is
z
To obtain the value of the lower bound L 4 at the state (t; d), we need to compute the infimum over
all choices of ffi , for
. Hence, the desired lower bound is
z
After substituting
simplifies to
z
The infimum of the monotonic function in ffi is reached at one of the two extreme points. When
(i.e., the transition occurs immediately), then the value of L 4 at (t; d) is
z
When
d (i.e., the transition occurs as late as possible), then the value of L 4 at
(t; d) is
z
y), the lower-bound label L 4 for R 4
is (a 2 ; a 3 ; a 3 ; a 4 ), where a 4 is the minimum of a 1 + a and a 2 Figure 4. Finally, we need to
x
a 2 a 3 a 3 a 4
a 2 a 3 a 4

Figure

5:
deduce the bit l 4 , which indicates whether the lower bound L 4 is a possible value of the integral.
If a 1 then the lower bound is obtained with possible for R 4 iff L 3
is possible for R 3 ; so l 4 is the same as l 3 . Otherwise, if a 1 then the lower bound is
obtained with ffi approaching
d , and L 4 is possible iff both l 3 is possible for R 3 ; so
l
We now formally define the edges between bound-labeled regions of the bounds graph B p;R f
(A).
Suppose that the region graph R(A) has an edge from R to R 0 , and let a be the duration measure
of R. Then the bounds graph has an edge from (R; L; l; U; u) to (R iff the bound
expressions
and the bits l, u, l 0 , and u 0 are related as follows. There are various cases to consider, depending
on whether the edge from R to R 0 is a time edge or a transition edge:
Time edge 1 R 0 is a boundary region and is an open region: let 1 - k - n be the
largest index such that R 0 satisfies - x
for all we have a
i+k and b
for all
a
Time edge 2 R is a boundary region and R is an open region:
a
for all
Transition edge 1 R 0 is a boundary region, R is an open region, and the clock with the k-th
smallest fractional part in R is reset:
for all we have a
if a 0
a then a
if a 0
a and a ? 0 then
a and a ? 0 then
Transition edge 2 Both R and R 0 are boundary regions, and the clock with the k-th smallest
fractional part in R is reset:
for all we have a
for all k - i - n, we have a
This case is illustrated in Figure 5.
This completes the definition of the bounds graph B p;R f (A).
Reachability in the bounds graph
Given a state oe = (s; c), two bound expressions L and U , and two bits l and u, we define the
(bounded) interval I(oe; L; l; U; u) of the nonnegative real line as follows: the left endpoint is
the right endpoint is [[U then the interval is left-closed, else it is left-open; if
then the interval is right-closed, else it is right-open. The following lemma states the fundamental
property of the bounds graph B p;R f (A).
A be a timed automaton, let p be a duration measure for A, and let R f be a region
of A. For every state oe of A and every nonnegative real ffi , there is a state - 2 R f such that
in the bounds graph B p;R f
(A), there is path to R f from a bound-labeled region
(R;
Proof. Consider a state oe of A and a nonnegative real ffi. Suppose (oe;
Then, by the definition of the region graph R(A), we have a sequence
of successors of extended states with oe
region graph contains an edge from the region R i+1 containing oe i+1 to the region R i containing
oe i . We claim that there exist bound-labeled regions such that (1) for all
the region component of B i is R i , (2) the bounds graph B p;R f (A) has an edge from B 0 to R f and
from B i+1 to B i for all
This claim is proved by induction on i, using the definition of the edges in
the bounds graph.
Conversely, consider a sequence of bound-labeled regions B such that the bounds graph
has an edge from B 0 to R f and from B i+1 to B i for all
(R We claim that for all
there exists - 2 R f with (oe; This is again proved by induction on i, using the definition
of the edges in the bounds graph. 2
For a bound-labeled region denote the union S
oe2R I(oe; L; l; U; u) of
intervals. It is not difficult to check that the set I(B) is a bounded interval of the nonnegative real
line with integer endpoints. The left endpoint ' of I(B) is the infimum of all choices of
clock valuations c that are consistent with R; that is, Rg. Since all irrelevant
coefficients in the bound expression L are 0, the infimum ' is equal to the smallest nonzero coefficient
in L (the left end-point is 0 if all coefficients are 0). Similarly, the right endpoint of I(B) is the
supremum of [[U all choices of c that are consistent with R, and this supremum is equal
to the largest coefficient in U . The type of the interval I(B) can be determined as follows. Let
ffl If a then I(B) is left-closed, and otherwise I(B) is left-open.
then I(B) is right-closed, and otherwise I(B) is
right-open.
For instance, consider the region R that satisfies
z. Let
is the open interval (1; 5), irrespective of the values of l and u.
A be a timed automaton, let
R
I be a duration constraint for A, and let R 0
be two regions of A. There are two states oe 2 R 0 and - 2 R f and a real number I such that
in the bounds graph B p;R f
(A), there is path to R f from a bound-labeled region B
with region component R 0 and I(B) " I 6= ;.
Hence, to solve the duration-bounded reachability problem
R
we construct the
portion of the bounds graph B p;R f (A) from which the special vertex R f is reachable. This can be
done in a backward breadth-first fashion starting from the final region R f . On a particular path
through the bounds graph, the same region may appear with different bound expressions. Although
there are infinitely many distinct bound expressions, the backward search can be terminated within
finitely many steps, because when the coefficients of the bound expressions become sufficiently large
relative to I , then their actual values become irrelevant. This is shown in the following section.
Collapsing the bounds graph
Given a nonnegative integer constant m, we define an equivalence relation - =m over bound-labeled
regions as follows. For two nonnegative integers a and b, define a - =m b iff either a = b, or both
m. For two bound expressions e = (a
iff for all
. For two bound-labeled regions
iff the following four conditions hold:
2.
3. either l some coefficient in L 1 is greater than m;
4. either some coefficient in U 1 is greater than m.
The following lemma states that the equivalence relation - =m on bound-labeled regions is back
stable.
Lemma 3 If the bounds graph B p;R f (A) contains an edge from a bound-labeled region B 1 to a bound-
labeled region B 0
, then there exists a bound-labeled region B 2 such that B 1
and the bounds graph contains an edge from B 2 to B 0
.
Proof. Consider two bound-labeled regions B 0
2 such that B 0- =m B 0
. Let R 0 be the clock
region of B 0
1 and of B 0
R be a
clock region such that the region graph R(A) has an edge from R to R 0 . Then there is a unique
bound-labeled region such that the bounds graph B p;R f
(A) has an edge
from B 1 to B 0
1 , and there is a unique bound-labeled region such that the
bounds graph has an edge from B 2 to B 0
2 . It remains to be shown that B 1
There are 4 cases to consider according to the rules for edges of the bounds graph. We consider
only the case corresponding to Transition edge 2. This corresponds to the case when R 0 is a
boundary region, R is an open region, and the clock with the k-th smallest fractional part in R is
reset. Let the duration measure be a in R. We will establish that L 1
some coefficient in L 1 is greater than m; the case of upper bounds is similar.
According to the
rule, for all
2 , we have a 0
It follows that for
We have
a
a). We have 4 cases to consider. (i) a
n and
n . Since a 0
n , we have a n
. In this case, l
1 and l
2 . If l 0
2 , we have
boundary region). Each
coefficient a 0
or a j , and thus some coefficient of L 1 also exceeds
m. (ii) a
a. In this case, we have a 0
It follows that all the values a 0
exceed m. Hence, a
and b n ? m. Since at least one coefficient of L 1 is at least m, there is no requirement that l
(indeed, they can be different). The cases (iii) a
n , and (iv) a
a and
a have similar analysis. 2
Since the equivalence relation - =m is back stable, for checking reachability between bound-labeled
regions in the bounds graph B p;R f (A), it suffices to look at the quotient graph [B p;R f
(A)]- =m . The
following lemma indicates a suitable choice for the constant m for solving a duration-bounded
reachability problem.
Lemma 4 Consider two bound-labeled regions B 1 and B 2 and a bounded interval I ' R with integer
endpoints. If B 1
for the right endpoint m of I, then I "
Proof. Consider bound-labeled regions
that
. It is easy to check that the left end-points of I(B 1 ) and I(B 2 ) are either equal or
both exceed m (see the rules for determining the left end-point). We need to show that when the
left end-points are at most m, either both I(B 1 ) and I(B 2 ) are left-open or both are left-closed. If
this is trivially true. Suppose l 1 we know that some coefficient of L 1 and of L 2
exceeds m. Since the left end-point is m or smaller, we know that both L 1 and L 2 have at least
two nonzero coefficients. In this case, both the intervals are left-open irrespective of the bits l 1 and
l 2 . A similar analysis of right end-points shows that either both the right end-points exceed m, or
both are at most m, are equal, and both the intervals are either right-open or right-closed. 2
A bound expression e is m-constrained, for a nonnegative integer m, iff all coefficients in e are
at most m + 1. Clearly, for every bound expression e, there exists a unique m-constrained bound
expression fl(e) such that e - =m fl(e). A bound-labeled region m-constrained
iff (1) both L and U are m-constrained, (2) if some coefficient of L is m+ 1, then l = 0, and (3) if
some coefficient of U is m for every bound-labeled region B, there exists
a unique m-constrained bound-labeled region fl(B) such that B - =m fl(B). Since no two distinct
m-constrained bound-labeled regions are - =m -equivalent, it follows that every - =m -equivalence class
contains precisely one m-constrained bound-labeled region. We use the m-constrained bound-
labeled regions to represent the - =m -equivalence classes.
The number of m-constrained expressions over n clocks is (m+2) n+1 . Hence, for a given region
R, the number of m-constrained bound-labeled regions of the form (R; L; l; U; u) is 4 \Delta (m+2) 2(n+1) .
From the bound on the number of clock regions, we obtain a bound on the number of m-constrained
bound-labeled regions of A, or equivalently, on the number of - =m -equivalence classes of bound-
labeled regions.
Lemma 5 Let A be a timed automaton with location set S and clock set X such that n is the number
of clocks, and no clock x is compared to a constant larger than m x . For every nonnegative integer
m, the number of m-constrained bound-labeled regions of A is at most
Consider the duration-bounded reachability problem
R
be the
right endpoint of the interval I . By Lemma 5, the number of m-constrained bound-labeled regions
is exponential in the length of the problem description. By combining Lemmas 2, 3, and 4, we
obtain the following exponential-time decision procedure for solving the given duration-bounded
reachability problem.
Theorem be the right endpoint of the interval I ' R. The answer to the duration-
bounded reachability problem
R
affirmative iff there exists a finite sequence
of m-constrained bound-labeled regions of A such that
1. the bounds graph B p;R f
(A) contains an edge to R f from some bound-labeled region B with
2. for all the bounds graph B p;R f
(A) contains an edge to B i from some bound-labeled
region B with
3. and the clock region of B k is R 0 .
Hence, when constructing, in a backward breadth-first fashion, the portion of the bounds graph
(A) from which the special vertex R f is reachable, we need to explore only m-constrained
bound-labeled regions. For each m-constrained bound-labeled region B i , we first construct all
predecessors of B i . The number of predecessors of B i is finite, and corresponds to the number
of predecessors of the clock region of B i in the region graph R(A). Each predecessor B of B i
that is not an m-constrained bound-labeled region is replaced by the - =m -equivalent m-constrained
region fl(B). The duration-bounded reachability property holds if a bound-labeled region B with
found. If the search terminates otherwise, by generating no new m-constrained
bound-labeled regions, then the answer to the duration-bounded reachability problem is negative.
The time complexity of the search is proportional to the number of m-constrained bound-labeled
regions, which is given in Lemma 5. The space complexity of the search is Pspace, because the
representation of an m-constrained bound-labeled region and its predecessor computation requires
only space polynomial in the length of the problem description.
Corollary 1 The duration-bounded reachability problem for timed automata can be decided in
Pspace.
The duration-bounded reachability problem for timed automata is Pspace-hard, because already
the (unbounded) reachability problem between clock regions is Pspace-hard [AD94].
We solved the duration-bounded reachability problem between two specified clock regions. Our
construction can be used for solving many related problems. First, it should be clear that the
initial and/or final region can be replaced either by a specific state with rational clock values, or
by a specific location (i.e., a set of clock regions). For instance, suppose that we are given an
initial state oe, a final state - , a duration constraint
R
I , and we are asked to decide whether
I . Assuming oe and - assign rational values to all clocks,
we can choose an appropriate time unit so that the regions [oe] - and [- are singletons. It follows
that the duration-bounded reachability problem between rational states is also solvable in Pspace.
A second example of a duration property we can decide is the following. Given a real-time
system modeled as a timed automaton, and nonnegative integers m, a, and b, we sometimes want
to verify that in every time interval of length m, the system spends at least a and at most b
accumulated time units in a given set of locations. For instance, for a railroad crossing similar to
the one that appears in various papers on real-time verification [AHH96], our algorithm can be
used to check that "in every interval of 1 hour, the gate is closed for at most 5 minutes." The
verification of this duration property, which depends on various gate delays and on the minimum
separation time between consecutive trains, requires the accumulation of the time during which the
gate is closed.
As a third, and final, example, recall the duration-bounded causality property ( ) from the
introduction. Assume that each location of the timed automaton is labeled with atomic propositions
such as q, denoting that the ringer is pressed, and r, denoting the response. The duration measure
is defined so that is a label of s, and otherwise. The labeling of the locations
with atomic propositions is extended to regions and bound-labeled regions. The desired duration-
bounded causality property, then, does not hold iff there is an initial region R 0 , a final region R f
labeled with r, and a bound-labeled region (R ;, and in
the bounds graph B p;R f , there is a path from B to R f that passes only through regions that are
not labeled with r.
The duration-bounded reachability problem has been studied, independently, in [KPSY93] also.
The approach taken there is quite different from ours. First, the problem is solved in the case of
discrete time, where all transitions of a timed automaton occur at integer time values. Next, it is
shown that the cases of discrete (integer-valued) time and dense (real-valued) time have the same
answer, provided the following two conditions are met: (1) the clock constraints of timed automata
use only positive boolean combinations of non-strict inequalities (i.e., inequalities involving - and -
and (2) the duration constraint is one-sided (i.e., it has the form R
N). The first requirement ensures that the runs of a timed automaton are closed under
digitization (i.e., rounding of real-numbered transition times relative to an arbitrary, but fixed
fractional part ffl 2 [0; 1) [HMP92]). The second requirement rules out duration constraints such
as
R
R
3. The approach of proving that the discrete-time and the dense-time
answers to the duration-bounded reachability problem coincide gives a simpler solution than ours,
and it also admits duration measures that assign negative integers to some locations. However, both
requirements (1) and (2) are essential for this approach. We also note that for timed automata
with a single clock, [KPSY93] gives an algorithm for checking more complex duration constraints,
such as R
R
different duration measures p and p 0 .
Instead of equipping timed automata with duration measures, a more general approach extends
timed automata with variables that measure accumulated durations. Such variables, which are
called integrators or stop watches, may advance in any given location either with time derivative
1 (like a clock) or with time derivative 0 (not changing in value). Like clocks, integrators can be
reset with transitions of the automaton, and the constraints guarding the automaton transitions
can test integrator values. The reachability problem between the locations of a timed automaton
with integrators, however, is undecidable [ACH single integrator can
cause undecidability [HKPV95]. Still, in many cases of practical interest, the reachability problem
for timed automata with integrators can be answered by a symbolic execution of the automaton
In contrast to the use of integrators, whose real-numbered values are part of the automaton state,
we achieved decidability by separating duration constraints from the system and treating them as
properties. This distinction between strengthening the model and strengthening the specification
language with the duration constraints is essential for the decidability of the resulting verification
problem. The expressiveness of specification languages can be increased further. For example,
it is possible to define temporal logics with duration constraints or integrators. The decidability
of the model-checking problem for such logics remains an open problem. For model checking a
given formula, we need to compute the characteristic set, which contains the states that satisfy the
formula. In particular, given an initial region R 0 , a final state - , and a duration constraint
R
we need to compute the set Q 0 ' R 0 of states oe 2 R 0 for which there exists a real number
such that (oe; Each bound-labeled region (R u) from which R f is reachable in
the bounds graph B p;R f contributes the subset foe 2 R 0 j I(oe; L; l; U; u) " I 6= ;g to Q 0 . In general,
there are infinitely many such contributions, possibly all singletons, and we know of no description
of Q 0 that can be used to decide the model-checking problem. By contrast, over discrete time, the
characteristic sets for formulas with integrators can be computed [BES93]. Also, over dense time,
the characteristic sets can be approximated symbolically [AHH96].

Acknowledgements

. We thank Sergio Yovine for a careful reading of the manuscript.



--R

Model checking in dense real time.

A theory of timed automata.
The benefits of relaxing punctuality.
Logics and models of real time: a survey.
Automatic symbolic verification of embedded systems.
On model checking for real-time properties with durations
Design and synthesis of synchronization skeletons using branching-time temporal logic
Decidability of bisimulation equivalence for parallel timer processes.
A calculus of durations.
Minimum and maximum delay problems in real-time systems
Timing assumptions and verification of finite-state concurrent systems
What's decidable about hybrid automata?
What good are digital clocks?
Symbolic model checking for real-time systems
Integration graphs: a class of decidable hybrid systems.
Specification and verification of concurrent systems in CESAR.
--TR

--CTR
Nicolas Markey , Jean-Franois Raskin, Model checking restricted sets of timed paths, Theoretical Computer Science, v.358 n.2, p.273-292, 7 August 2006
Yasmina Abdeddam , Eugene Asarin , Oded Maler, Scheduling with timed automata, Theoretical Computer Science, v.354 n.2, p.272-300, 28 March 2006
real-time systems;duration properties;formal verification;model checking