Optimal Paths in Weighted Timed Automata?

Rajeev Alur1,2 , Salvatore La Torre1,3 , and George J. Pappas1

1
University of Pennsylvania
2
Bell Labs
3
Università degli Studi di Salerno
{alur,pappasg}@[Link], latorre@[Link]

Abstract. We consider an optimal-reachability problem for a timed au-

tomaton with respect to a linear cost function which results in a weighted
timed automaton. Our solution to this optimization problem consists of
reducing it to a (parametric) shortest-path problem for a finite directed
graph. The directed graph we construct is a refinement of the region au-
tomaton due to Alur and Dill. We present an exponential time algorithm
to solve the shortest-path problem for weighted timed automata starting
from a single state, and a doubly-exponential time algorithm to solve
this problem starting from a zone of the state space.

1 Introduction

Timed automata [AD94] are widely accepted as a formalism to model the be-
haviour of real-time systems: a discrete transition graph is equipped with a finite
set of clock variables which are used to express timing constraints. Automated
analysis of timed automata relies on the construction of a finite quotient of the
infinite space of clock valuations. In particular, this construction is suitable to
perform reachability analysis. Given two states s and t of a timed automaton A,
the reachability problem can be stated as the problem of determining if there
exists a run of A from s to t. Reachability is a core problem in system verification
and directly applies to the verification of safety properties.
In the theory of timed automata there are many decision problems which are
undecidable, and decidability is in general hard. In this paper we are interested in
an optimal-reachability problem for timed automata. Time-optimal reachability
was first considered in [CY91], where the problem of computing lower and upper
bounds on time delays in timed automata was solved. Minimal-time reachability
is also considered in [NTY00]. In [ACH93], a weight w is associated with each
location q such that w gives the cost of a unit of time spent in q. Then, given
a cost interval I and two states s and t, the decision problem “is t reachable
from s at a cost c ∈ I?” (duration-bounded reachability) is addressed and solved.
?
This work is partially supported by the DARPA/ITO MoBIES grant F33615-00-C-
1707, the NSF Career award CCR97-34115, the SRC award 99-TJ-688, the MURST
grant TOSCA, the DARPA JFACC grant N66001-99-C-8510, and the University of
Pennsylvania Research Foundation.

M.D. Di Benedetto, A. Sangiovanni-Vincentelli (Eds.): HSCC 2001, LNCS 2034, pp. 49–62, 2001.
c Springer-Verlag Berlin Heidelberg 2001
50 R. Alur, S. La Torre, and G.J. Pappas

Here we solve a more general optimal-reachability problem, that has been inde-
pendently solved also in [BHF+ ]. We consider weighted timed automata, that is
timed automata with weights (different costs) on both locations and transitions.
The cost of a run is given by the sum of costs of the taken switches plus the sum
of the costs associated with the visited locations multiplied for the time spent in
each of them. Our optimization problem, which we call optimal-run problem, can
be formalized as a tuple containing a weighted timed automaton, a source zone
and a target zone. If the source zone contains only a state of the automaton, we
refer to this problem as the single-source optimal-run problem.
Our solution to the optimal-run problem consists of two main steps: first we
reduce the optimal-run problem to a shortest-path problem in directed graphs,
then we solve the latter. The first step is obtained by constructing a finite graph
which is a refinement of the region automaton [AD94]. Each clock region is split
into several disjoint subregions relatively to a starting state and to sequences
of resets that may occur in “potential” optimal runs. This construction is pa-
rameterized on the differences of two consecutive fractional parts from the clock
valuation of the starting state. When we consider a general source zone, we leave
unspecified these parameters and the above construction reduces the optimal-run
problem for weighted timed automata to a parametric shortest-path problem in
directed graphs. We give a fix-point computation algorithm to solve this prob-
lem, so obtaining a doubly-exponential time algorithm solving the optimal-run
problem. In case the input automaton has only one clock variable, this result can
be improved to a single exponential by adapting to our case the algorithm given
in [KO81,YTO91] for solving a particular case of parametric shortest-path prob-
lem. In case the source zone is a singleton we substitutes the parameters with
the actual values from the starting state, and thus our optimization problem
is reduced to a standard shortest-path problem. Using Dijkstra’s algorithm, we
obtain an exponential time algorithm for the single-source optimal-run problem.
The optimal-reachability problem is strictly related to other decision prob-
lems, and in particular to the problem of synthesizing an optimal controller.
The optimal-control synthesis problem can be informally stated as the prob-
lem of designing a control which is able to drive, at a minimum cost, the sys-
tem into a given target zone. In the literature, control synthesis problems have
been considered in the context of discrete automata [Chu62,Tho95], timed au-
tomata [AMP95,MPS95,AM99], linear hybrid automata [WT97], and general
hybrid systems [LTS99,SPS00]. The design of an optimal control for hybrid sys-
tems is not trivial and in general is undecidable. The approach presented in
this paper, can be adapted to solve the optimal-control synthesis problem for
weighted timed automata. We observe that this generalizes the results obtained
in [AM99] on the synthesis of a time-optimal controller for a timed automaton.
The rest of the paper is organized as follows. In section 2, we define the
optimal-run problems and we give some examples. In section 3, we introduce
a graph construction to reduce the optimal-run problems to the corresponding
shortest-path problems in directed graphs. In section 4, we present our solutions
to the single-source optimal-run problem and to the general case.
 Optimal Paths in Weighted Timed Automata 51

2 Preliminaries

In this section we define the single-source and the parametric optimal-run prob-
lems. We start introducing some notation and the definition of timed automaton.
Given a set C of n variables, a k-zone is a subset of Rn that can be obtained
as a boolean combination of inequalities of the form x ≤ y + c, x < y + c, x ≤ c,
and x < c where x, y ∈ C and c ∈ {0, 1, . . . , k}. We denote by True the clock
constraint which is true for any clock values. We denote by Z(C) the set of all
the k-zones, for all k ∈ N. A function λ : Rn −→ Rn is called a reset function if
it is equal to the identity on some of the coordinates and zero on the others. We
denote by Λn the set of all reset functions over Rn . A timed automaton 1 A is a
tuple (Q, C, ∆, Inv) where:

– Q is a finite set of locations;

– C is a finite set of n clock variables;
– ∆ is a finite subset of Q × Z(C) × Λn × Q;
– Inv : Q −→ Z(C) maps each location q to its invariant Inv(q).

A state is a tuple (q, ν) where q ∈ Q and ν ∈ Rn . We denote by S = Q×Rn the

0 0 0
set of states for A. A discrete step is (q, ν)−→ e (q , ν ) where e = (q, δ, λ, q ) ∈ ∆,
t
ν satisfies δ, ν 0 = λ(ν), and ν 0 satisfies Inv(q 0 ). A time step is (q, ν) −→ (q, ν 0 )
where ν 0 = ν + t, t ≥ 0, and ν + t0 satisfies Inv(q) for all 0 ≤ t0 ≤ t.
t 0 0 t 00 00 0 0
A step is (q, ν)−→ e (q , ν ) where (q, ν) −→ (q, ν ) and (q, ν )−→ e (q , ν ), for
00 n
some ν ∈ R , that is a transition e taken after spending some time t in
the current location. A run r of a timed automaton A is a finite sequence
t1 t2 tk−1 tk
(q0 , ν0 )−→e1 (q1 , ν1 )−→
e2 . . . e−→
k−1
(qk−1 , νk−1 )−→ (qk , νk ). We say that r starts at
(q0 , ν0 ) and ends at (qk , νk ). The definition of r allows time to be spent after tak-
ing the last transition ek−1 . A weighted timed automaton is a timed automaton
A with the following cost functions:

– J s : ∆ −→ N (switch cost), and

– J d : Q −→ N (duration cost).

Given a run r of A and cost functions J s , and J d , we associate costs to r as

follows:
Pk
– J s (r) = i=1 J s (ei ), and
Pk−1
– J d (r) = i=0 ti · J d (qi ).

The total cost associated to a run r is then J(r) = J s (r) + J d (r). We are inter-
ested in determining optimal-cost runs for a timed automaton. In the following
examples we informally introduce some notions that we will formalize in the rest
of the section.
1
The standard definition of timed automata requires also an acceptance condition
and a symbol alphabet. Since we are not interested in studying languages accepted
by timed automata we omit these features here.
52 R. Alur, S. La Torre, and G.J. Pappas

Example 1. Consider the timed automaton defined in Figure 1 such that J d (0) =
3, J d (1) = 1, and the switch costs are all 1. Suppose that we start from state
s = (0, x, y) for 0 ≤ x, y < 2 and we want to reach a state in location 2.
Possible minimal-cost runs from s to a state s0 = (2, x0 , y 0 ) are either r1 =
t1 t2 t3
(0, x, y)−→
e1 (1, x1 , y1 )−→
e3 (2, x + 2 − y, 2), or r2 = (0, x, y)−→
e2 (2, 2, y + 2 − x)
for t3 = (2 − x) (obviously, staying in location 2 longer might only increase the
overall cost). According to the cost function J, the cost of r1 is J s (r1 )+J d (r1 ) =
2+3t1 +(2−y−t1 ) = 4−y+2t1 and the cost of r2 is J s (r2 )+J d (r2 ) = 1+3(2−x) =
7−3x. Clearly, J(r1 ) is minimized when t1 = 0, that is the transition from 0 to 1
is taken immediately. Moreover, assuming t1 = 0, J(r1 ) ≤ J(r2 ) if y ≥ 3(x − 1),
and J(r1 ) > J(r2 ), otherwise. Thus, a minimal-cost run from s to a state in
location 2 depends on the clock valuation of state s.

0
x=2
e2
y<2 e1

e3 2

1 y=2

Fig. 1. A timed automaton with more than an optimal run from a same location.

Example 2. Consider the timed automaton defined in Figure 2 such that J d (0) =
1, J d (1) = 2, and the switch costs are all 1. Suppose that we start from
state s = (0, x) for 0 ≤ x < 2 and we want to reach a state in location
2. Possible minimal-cost runs from s to a state s0 = (2, x0 ) are given by
t t0
rt = (0, x)−→e1 (1, x1 )−→
e2 (2, 2). Notice that rt is a run parameterized by t,
where t is the time at which the first edge is taken. Thus J(rt ) = J s (rt )+J d (rt ) =
2+t+2(2−t−x) = 6−t−2x. Hence the cost of rt is minimized if t is maximized.
Since t < (2 − x) must hold, the optimal cost for a run starting at s is (4 − x),
but none of the runs starting at s has such a cost. In fact, for any actual run rt
there exists a ξ > 0 such that t = (2 − x − ξ), and J(rt ) = (4 − x + ξ). Vice-versa,
for any ξ > 0 there exists a run r such that J(r) = (4 − x + ξ). Clearly, there
is not a minimal-cost run but we can determine a run whose cost is arbitrarily
close to the optimal one.

Now we formalize the notion of optimal cost, optimal run, and approximation
of an optimal run. Given a timed automaton A, a state s, and a target zone T ,
an optimal cost for a run from s to T is a J ∗ such that J ∗ ≤ J(r) for any run r
from s to a state in T , and for any ξ > 0 there is a run r such that J(r) ≤ J ∗ + ξ.
 Optimal Paths in Weighted Timed Automata 53

x<2 x=2
0 1 2
e1 e2

Fig. 2. A timed automaton with no optimal runs from a location.

If there exists a run r∗ such that J(r∗ ) = J ∗ , then r∗ is said to be an optimal

run. As shown in Example 2, sometimes an optimal run from a state s to a
target zone T does not exist. In these cases, we are interested in a family R
of runs such that all the runs coincide on the sequence of switches and for any
ξ ∈ R+ there exists a run r ∈ R such that J(r) < J ∗ + ξ, where J ∗ is the optimal
cost over all runs from s to T . That is we can determine a sequence of runs in
R whose costs are arbitrarily close to J ∗ . We call such a family of runs R an
approximation of an optimal run. Given a timed automaton A, a source zone S,
and a target zone T , we consider the problem of determining an optimal run from
a given state s ∈ S to T , if one exists, or an approximation of an optimal run,
otherwise. We call this problem a single-source optimal-run problem. We also
consider a more general problem, a zone optimal-run problem, defined as the
problem of determining a symbolic representation of the solution to the single-
source optimal-run problem for all states in S. In Example 1, if we consider as
target region all the states in location 2 and as only source state (0, 0, 0), then a
solution to the corresponding instance of the single-source optimal-run problem
is r1 with t1 = 0. As observed in Example 1, if we consider as source zone the set
of states (0, x, y) such that 0 ≤ x, y ≤ 1, then the solution of the corresponding
instance of the zone optimal-run problem is r1 with t1 = 0 if y ≥ 3(x − 1), and
r2 , otherwise.
We end this section with an example on an air-traffic control problem that
we will use subsequently in the paper.

Example 3. Consider the timed automaton in Figure 3. It models a scenario in

which two aircraft send a landing request to an airport, and our goal is to allow
both the aircraft to land safely and at minimum cost. Safety requires that only
one aircraft at a time must be acknowledged for landing, thus there are two
possible choices: aircraft 1 waits for the landing of aircraft 2 to be completed,
or vice-versa. There are costs c1 and c2 to pay for forcing respectively aircraft
1 and aircraft 2 to wait. Moreover, there is also a cost, expressed by wi , which
is related to the time spent waiting. Alternatively, aircraft i can make, at a cost
c0i , a maneuver that allows to spend wi0 instead of wi per each time unit. This
maneuver takes at least time 1. Since it is realistic to reduce the time a runway
stays unused, we penalize this event by a cost c0 per time unit. Finally, we
assume that the landing of each aircraft takes at least time 1 since the related
acknowledgement was issued by the control tower.
54 R. Alur, S. La Torre, and G.J. Pappas

c0 w2
x2> 1
c 2 : x 1< 1, x 2< 1 w’2
W2
Start W’
x 1 := 0 x 1< 2 2
c’2 : x 2 := 0
c1
x 1< 1 x 2 := 0
x 2< 1 x 1> 1

w1 c 0 + w2
W1
L2
x 2< 2

c’1 x2> 1 1 < x 2< 2

x 1> 1
x 1 := 0 x 1> 1
c0 +w
1
w’1 1 < x 1< 2
W’
1 L1 Target
x2> 1

Fig. 3. An air-traffic control problem.

3 The Graph Construction

In this section we give the graph construction underlying the reduction of the
single-source optimal-run problem to the shortest-path problem and the zone
optimal-run problem to a parametric shortest-path problem. The obtained graph
is a refinement of the region automaton [AD94] of a timed automaton, in the
sense that each vertex v carries more information than a region. This additional
information mainly concerns the sequence of resets needed to reach v from a
starting vertex, and the construction preserves the transitions of the region au-
tomaton. Via this construction we emphasize the states of the timed automaton
that might be visited in some optimal runs. We start by recalling the concepts
of labelled directed graph and region automaton, then we describe our graph
construction.
Let Θ be a set of real-valued parameters, we denote by D the set of linear
expressions over Θ. Given an alphabet Σ, a D-labelled directed graph G is a pair
(V, E), where V is a set of vertices, and E ⊆ V ×D×V is a set of D-labelled edges.
f1 f2 fn−1 fn
A path π from v0 to vn in G is a sequence v0 −→ v1 −→ . . . −→ vn−1 −→ vn
fi−1
such that vi−1 −→ vi ∈ E for i = 1, . . . , n. For a path π, the cost of π is given by
P n 0
i=1 fi . A path π from v to v is a shortest path if π is the path with minimum
cost among those connecting v to v 0 . Notice that varying the values of parameters
in Θ the shortest path of a graph may change, that is to different valuations of
parameters may correspond different sets of shortest paths in the graph.
Consider now a timed automaton A. By definition its set of states is infinite.
However, they can be partitioned in a finite number of equivalence classes, called
regions, which are defined by a location and a clock region. Denoted by cx the
 Optimal Paths in Weighted Timed Automata 55

largest constant in clock constraints involving the clock variable x, a clock region
is described by:

– a constraint of type c − 1 < x < c, x > cx , or x = c for each clock variable

x and c ≤ cx ;
– the ordering of the fractional parts of the clock variables x such that x < cx .

Thus a clock region denotes a set of clock valuations. Given a clock valuation
ν, [ν] denotes the clock region containing ν. A state (q, ν) belongs to a region
hq 0 , αi if q = q 0 and ν ∈ α. A clock region α is said to be open if for any clock
variable x and c ≤ cx , x = c does not hold in α. Otherwise α is said to be
a boundary clock region. These definitions apply to regions in an obvious way.
The key property of this equivalence, is that all the valuations belonging to a
region satisfy the same set of clock constraints from the given timed automaton.
Consistently we say that a clock region α satisfies a constraint δ if ν satisfies δ
for any ν ∈ α. A clock region α0 is said to be a time-successor of a clock region
α if and only if for any ν ∈ α there is a d ∈ <+ such that ν + d ∈ α0 . The region
automaton of A is a transition system defined by:

– the set of states R(S) = {hq, αi | q ∈ Q and α is a clock region for A};
– the transition rules R(∆) such that: (hq, αi, hq 0 , α0 i) ∈ R(∆) if and only if
(q, λ, δ, q 0 ) ∈ ∆ and there is a time-successor α00 of α such that α00 satisfies δ
and α0 = [λ → 0]α00 .

We denote the region automaton corresponding to A as R(A). For the sake of

simplicity, in the following when no confusion can arise we refer to the value of
a clock variable x by x itself. With x we denote the fractional part of a clock
variable x. Let s = (q, ν) be a state of A and (0 ≈1 x01 ≈2 . . . ≈N x0N ≈N +1 1)
be the ordering of the fractional parts of the region containing a clock valuation
ν (notice that ≈i is either = or <). With ϑ(s) = (ϑ1 , . . . , ϑN +1 ) we denote the
differences between consecutive values in the above ordering, that is ϑ1 = x01 ,
ϑN +1 = 1 − x0N , and ϑi = x0i − x0i−1 for i = 2, . . . , N . In the following we
will use (ϑ1 , . . . , ϑN +1 ) to denote these differences in the starting state. The
graph we are going to define is parameterized over (ϑ1 , . . . , ϑN +1 ). Moreover,
for i, j ≤ N , we denote by I(i, j) the set of integers {i, . . . , j − 1}, if i < j, and
{i, . . . , N } ∪ {1, . . . , j − 1}, otherwise.
The region automaton does not carry enough information to solve our op-
timization problems. Thus we define a labelled directed graph whose vertices
correspond to “sub-states” of the region automaton. For a given state hq, α0 i
of the region automaton, a sub-state hq, αi is such that α is a convex region
contained in α0 . Denoted by (0 ≈1 x01 ≈2 . . . ≈h x0h ≈h+1 1) the ordering of the
fractional parts in a clock region α0 , we consider sub-regions α of α0 such that
for some of the ≈i ’s which are equal to <, the difference between x0i−1 and x0i is
very close to 0. Thus we represent α by α0 and specifying in the ordering of the
fractional parts if a < is relative to a “small” difference (denoted by < ∼ ) or to a
“large” difference (denoted by <). We call each such sub-region α a boundary
sub-region. Intuitively, the reason we are interested in boundary sub-regions is
that the cost functions we consider are linear, and their infimum over a given
56 R. Alur, S. La Torre, and G.J. Pappas

region is reached on the boundary. Thus optimal runs leave open regions from
states which are arbitrarily close to their boundaries. As a consequence optimal
runs visit also states characterized by having clocks values either with arbitrarily
close fractional parts or with fractional parts which reflects the starting state and
the reset history of the computation. For this reason, we add to each boundary
sub-region a tuple of indices (i1 , . . . , ik ) from {1, . . . , n + 1} such that: k is the
number of large differences in the ordering of the fractional parts, il corresponds
to the l-th large difference in the ordering of the fractional parts, and there exists
a d ∈ {1, . . . , k} such that id+h < id+h+1 for h = 0, . . . , k − 1, where the sums
(d + h + 1) and (d + h) are modulo k. We call such tuples distance tuples, since
they are used to store the difference between two consecutive fractional parts
when this difference is “large” (i.e., they are not arbitrarily close). We define the
set of vertices V as the set of tuples hq, α, (i1 , . . . , ik )i where q is a location, α is
a boundary sub-region, and (i1 , . . . , ik ) P is a distance tuple from {1, . . . , n + 1}.
For a vertex hq, α, (i1 , . . . , ik )i, the sum l∈I(ik ,i1 ) ϑl gives the time to leave the
region since this subregion is entered.
The set of edges E contains three types of edges: immediate switches, time
edges and delayed switches. Informally, immediate switches correspond to tran-
sitions taken in the current state, time edges correspond to letting time elapse
until the next region is reached, and delayed switches correspond to transitions
taken at the “beginning” or at the “end” of the closest open region (this region
if it is an open region, the next otherwise).
Given two vertices v = hq, α, (i1 , . . . , ih )i and v 0 = hq 0 , β, (j1 , . . . , jk )i), there
J s (e)
is an immediate switch v −→ v 0 if there exists a transition e of R(A) from hq, α0 i
to hq 0 , β 0 i, where α0 and β 0 are respectively the regions of R(A) containing α and
β, and the sequence (j1 , . . . , jk ) is obtained from (i1 , . . . , ih ) by deleting all the
indices il such that all the clocks between the l-th and the (l + 1)-th large
differences (in the ordering of the fractional parts of α0 ) are reset in e.
Consider a vertex v = hq, α, (i1 , . . . , ih )i and let (0 ≈1 y 1 ≈2 . . . ≈k y k ≈k+1
1) be the ordering of the fractional parts in α. If we assume that α(yk ) + 1 is not
larger than the largest constant in the timing constraints involving yk (i.e., when
time elapses the first integer value reached by yk is at most this constant), we
c
add to E a time edge v −→ v 0 for v 0 = hq, β, (j1 , . . . , jh0 )i where β is the closest
time-successor of α such that the conditions expressed by one of the rows of the
following Table 1 are satisfied (where (0 ≈01 y 01 ≈2 . . . ≈0k y 0k ≈k+1 1) denotes
the ordering of the fractional parts in β, and l = 2, . . . , k):
≈1 ≈k+1 ≈01 ≈02 ≈0l+1 (j1 , . . . , jh0 ) Pc
1. < < = < ≈l (ih , i2 , . . . , ih−1 ) J d (q) l∈I(ih ,i1 ) ϑl
P
2. <
∼ or = < = < ≈l (ih , i1 , . . . , ih−1 ) J d (q) l∈I(ih ,i1 ) ϑl
3. < <
∼ = < ≈l (i1 , . . . , ih ) 0
4. ∼ or = <
<
∼ = <
∼ ≈l (i1 , . . . , ih ) 0

In the other case, time edges are defined in the same way except for the
fact that the clock yk does not appear in the ordering of the fractional parts of
v 0 since it has reached its highest constant. To see an example of a time edge,
 Optimal Paths in Weighted Timed Automata 57

consider a vertex v = hq, 0 < x < y < z < 1, (1, 2, 3, 4)i. By row 1 of the above
table we have a time edge from v to hq, 0 < x < y < 1 ∧ z = 1, (4, 2, 3)i. The
distance tuple (4, 2, 3) captures the fact that time (1 − z) has elapsed and thus
the distance in time from x to 0 is increased by (1 − z), the fractional part of z
is now 0, and all the other distances stay unchanged.
c
Given a vertex v ∈ V as above, we add to E a delayed switch v −→ v 00 for
J s (e)
any vertex v 00 ∈ V such that there exists an immediate switch v 0 −→ v 00 and
c = c0 + J s (e), where v 0 = hq, β, (j1 , . . . , jh0 )i and β is the closest time-successor
of α such that the conditions expressed by one of the rows of the following Table
2 are satisfied (where (0 ≈01 y 01 ≈2 . . . ≈0k y 0k ≈k+1 1) denotes the ordering of the
fractional parts in β, and l = 2, . . . , k):
≈1 ≈k+1 ≈01 ≈0l ≈0k+1 (j1 , . . . , jh0 ) Pc
0

1. < < < ≈l ∼ (ih , i2 , . . . , ih−1 ) J d (q) l∈I(ih ,i1 ) ϑl

<
P
2. <
∼ < < ≈l < ∼ (ih , i1 , . . . , ih−1 ) J d (q) l∈I(ih ,i1 ) ϑl
3. = < < ≈
∼ l < (i1 , . . . , ih ) P0
4. = < < ≈l < ∼ (i ,
h 1 i , . . . , i h−1 ) J d (q) l∈I(ih ,i1 ) ϑl
5. = < ∼ <
∼ ≈ l <∼ (i 1 , . . . , ih ) 0
For a given tuple of parameters ϑ = (ϑ1 , . . . , ϑN +1 ), we denote by GA (ϑ) the
D-labelled directed graph (V, E). We recall that for our purposes ϑ represents the
differences between the fractional parts of two consecutive clocks in the ordering
of the fractional parts in the starting state. The construction of GA (ϑ) is general
in the sense that it does not depend on the particular source and target zones of
the problem, but only on the timed automaton. This allows us to use it for solving
both the single-source optimal-run problem (for a fixed ϑ) and the zone optimal-
run problem (ϑ belongs to a convex set). As an example of application of the
above construction, we discuss a fragment of the graph GA (ϑ) for the weighted
timed automaton modelling the air-traffic control problem from Example 3 (see
Figure 4). For the sake of simplicity, we have marked with 1, . . . , 5 the vertices
of GA (ϑ) in Figure 4, and we refer to them by these numbers. Consider vertex
1. Since in the timed automaton from Figure 3 there is a transition from W1 to
W10 resetting clock x1 , we have in GA (ϑ) an immediate switch from 1 to 2. Edges
from 1 to 3 and from 1 to 4 are delayed switches obtained by the same transition
above and respectively rows 3 and 4 of Table 2. The edge from 1 to 5 is a time
edge and is defined by row 2 of Table 1. Notice that for a given state s = (q, ν), we
have corresponding vertices of GA (ϑ(s)) of form hq, α, (i1 , . . . , ik )i, where ν ∈ α.
Moreover, each edge is labelled by the actual cost of the corresponding “activity”
in A, that is for immediate switches we have just the cost of the A transition,
for time edges the cost of spending the time upto the end of the current region
in the current A location, and for delayed switches the cost corresponding to the
A transition plus the cost for the time spent in the current location before that
the transition is taken. We have the following lemma.

Lemma 1. Given a timed automaton A, the size of GA (ϑ) is exponential in the

length of clock constraints of A.
58 R. Alur, S. La Torre, and G.J. Pappas

W’ x2= 0 2
1 c’1 1
x1= 0
W1 x2= 0
(1)
0 < x 1< 1
(1,2) c’1

W’
1 x1= 0
w1 (θ 2+ θ3 ) c’1 + x 2 >~ 0
3
w1 (θ 2+ θ3 )
(1,2)
W1
W’ x1= 0
0 < x 2 < x 1< 1 1

0 < x 2< 1
(2,1)
(2,1)
5
4

Fig. 4. A fragment of GA (ϑ) for the weighted timed automaton in Example 3.

Proof. In [AD94] the authors proved that the size of the region automaton is
O(|A| 2|δ(A)| ), where |δ(A)| denotes the length of the clock constraints. A sim-
ple counting argument gives that the number of ways to substitute < with < ∼
in the ordering of the fractional parts of a clock region is at most 2n+1 and
the number of tuples of indices we use to represent the relative differences be-
tween the fractional parts is at most n2n . Thus the size of GA (ϑ) is at most
O(|A| n 22n+1 2|δ(A)| ), and since n = O(|δ(A)|), it is exponential in the length of
the clock constraints.

4 Optimal-Runs in Weighted Timed Automata

4.1 Single-Source Case
In this section we prove that the single-source optimal-run problem in timed
automata can be reduced to the shortest path problem in a weighted directed
graph. To see this we introduce first some notation. Let s0 be a state (q0 , ν0 )
of a weighted timed automaton A and ϑ(s0 ) = (ϑ1 , . . . , ϑN0 +1 ), we denote by
g(s0 ) the vertex
q0 , α0 , (i0,1 , . . . , i0,N0 ) of GA (ϑ(s0 )) such that ν0 ∈ α0 and
i0,j is the j-th largest distance in the ordering of the fractional parts in α0 .
c1
Given a positive real ξ << 1 and a path π =
q0 , α0 , (i0,1 , . . . , i0,N0 ) −→
c2 ch

q1 , α1 , (i1,1 , . . . , i1,N1 ) −→ . . . −→
qh , αh , (ih,1 , . . . , ih,Nh ) in GA (ϑ(s0 )), we
denote by Rπ (ξ) the set of runs of A starting at s0 and obtained by replac-
tj cj+1 ck
ing with (qj , νj )−→ ej (qk , νk ) each portion
qj , αj , (ij,1 , . . . , ij,Nj ) −→ . . . −→

qk , αk , (ik,1 , . . . , ik,Nk ) of π such that:
cj−1
–
qj−1 , αj−1 , (ij−1,1 , . . . , ij−1,Nj−1 ) −→
qj , αj , (ij,1 , . . . , ij,Nj ) is either an
immediate or a delayed switch;
cl+1
– for l = j . . . , k − 2,
ql , αl , (il,1 , . . . , il,Nl ) −→

ql+1 , αl+1 , (il+1,1 , . . . , il+1,Nl+1 ) is a time edge;
 Optimal Paths in Weighted Timed Automata 59

c
k
– hqk−1 , αk−1 , (ik−1,1 , . . . , ik−1,Nk−1 )i −→ hqk , αk , (ik,1 , . . . , ik,Nk )i is either an
immediate or a delayed switch. Let tj = τ 0 + τ 00 and νj + τ 0 ∈ αk−1 . In the
case of an immediate switch τ 00 = 0, while in the other case τ 00 is such that:
– if the delayed switch is obtained by rows 1 and 2 of Table 2, then νj +tj ∈
αk−1 and the largest fractional part in νj + tj is greater than (1 − ξ);
– otherwise, denoted as α0 the time-successor of αk−1 which is first entered
by letting time elapse from a valuation in αk−1 , it holds that νj +tj ∈ α0 ,
moreover if the delayed switch is obtained by rows 4 and 5 of Table 2,
the largest meaningful fractional part in νj + tj is greater than (1 − ξ),
and if the delayed switch is obtained by rows 3 and 5 of Table 2, the
smallest meaningful fractional part in νj + tj is less than ξ;
ck−1
– ej is the transition corresponding to hqk−1 , αk−1 , (ik−1,1 , . . . , ik−1,Nk−1 )i −→
hqk , αk , (ik,1 , . . . , ik,Nk )i.

In the following we assume that ξ is a positive real number such that ξ << 1.
By the definition of GA (ϑ) and Rπ (ξ), we have the following lemma.
Lemma 2. Given a timed automaton A and a state s = (q, ν) of A, if π is a
path of GA (ϑ(s)) from g(s) of cost cπ then Rπ (ξ) is a set of runs of A such that
for any ε > 0 there exists an r ∈ Rπ (ξ) such that cπ ≤ J(r) < cπ + ε.
To complete our reduction we need the following lemma.
Lemma 3. Given a run r of A from a state s to a target zone T , there exists
a path π of GA (ϑ(s)) from g(s) to a vertex corresponding to a state in T such
that the cost of π is not larger than J(r).

Proof. The interesting case is when transitions in r are from states that do not
belong to any of the subregions encoded by GA (ϑ(s)) vertices. Assume that A
in run r takes a transition e from an open region α after spending some time in
it, and e is the first transition in r with this property. Clearly, upto e, r has a
corresponding path π in GA (ϑ(s)) whose cost is not more than J(r). We observe
that by definition there must be two delayed transitions e1 and e2 of GA (ϑ(s))
corresponding respectively to the cases e is taken as soon as α is entered and
e is taken just before leaving α. Moreover, consider two A runs r1 and r2 that
differ from r only for the fact that in r1 A takes e after an arbitrarily short time
spent in α, while in r2 A takes e after an arbitrarily short time before leaving
α. Clearly, J(r) ≥ min{J(r1 ), J(r2 )} holds. Thus we can add to π the transition
corresponding to the run ri with the least cost between r1 and r2 . Applying
iteratively this argument, we determine a path π in GA (ϑ(s)) of cost c ≤ J(r).

As a direct consequence of Lemmas 2 and 3, we have the following theorems.

Theorem 1. Given a timed automaton A, a state s of A, a target zone T , π

is a shortest path of GA (ϑ(s)) starting from g(s) to a vertex corresponding to a
state in T if and only if Rπ (ξ) is an approximation of an optimal run of A from
s to T .
60 R. Alur, S. La Torre, and G.J. Pappas

Theorem 2. Given a timed automaton A, a state s of A, a target zone T , there

exists an optimal run of A from s to T if and only if for a shortest path π of
GA (ϑ(s)) from g(s) to a vertex corresponding to a state in T there exists a run
r ∈ Rπ (ξ), such that the cost of π is equal to J(r). Moreover, r is an optimal
run of A from s to T .

Given a timed automaton A, a source state s, and a target zone T , the

following algorithm solves the single-source optimal-run problem:

1. Let G be the graph obtained from GA (ϑ(s)) by collapsing all the vertices
corresponding to a state in T in a single vertex vt .
2. Solve the single-source shortest-path problem on G from g(s).
3. Let π be a shortest path from vs to vt . Output2 Rπ (ξ) and the cost of π.

Theorem 3. The single-source optimal-run problem can be solved in time ex-

ponential in the size of the timed automaton.

4.2 The Algorithm for the General Case

In this section we consider the zone optimal-run problem. We give an exponential

time algorithm to solve this problem for timed automata with at most 1 clock
and a fix-point algorithm in doubly-exponential time, for the general case.
We start considering the general case. Since we want to solve the problem
of determining the optimal runs from any state of the source zone S to a state
of a target zone T , for parameters ϑ in GA (ϑ) we consider only values given
by ϑ = ϑ(s) for a state in s ∈ S. Thus it holds that ϑ1 + . . . + ϑN +1 = 1
PN
and we can eliminate a parameter by the substitution ϑN +1 = 1 − i=1 ϑi .
From now on, we will assume that ϑ(s) is the tuple (ϑ1 , . . . , ϑN ) and GA (ϑ(s))
PN
is the graph obtained after the substitution ϑN +1 = 1 − i=1 ϑi . The algo-
rithm that we are giving, labels the vertices of GA (ϑ) with sets of linear ex-
pressions on ϑ = (ϑ1 , . . . , ϑN ). The meaning of these expressions is that given
a state s ∈ S the minimum over these expressions gives the optimal cost of
a run from s. An expression is a first-degree polynomial in ϑ1 , . . . , ϑN , and
PN
(1 − i=1 ϑi ) with integer coefficients. That is, an expression has the form
PN
f (ϑ) = a0 + a1 ϑ1 + . . . + aN ϑN + aN +1 (1 − i=1 ϑi ), where a0 , . . . , aN +1 are
nonnegative integer constants. We denote expressions by (N + 2)-tuples of co-
efficients and write (a0 , . . . , aN +1 ) for the above expression f (ϑ). We denote by
≺ the natural extension to tuples of the total ordering < over reals. Moreover,
let f, f 0 be two expressions, and v, v 0 be two vertices of GA (ϑ), (f, v) ≺ (f 0 , v 0 )
if and only if f ≺ f 0 . A set X of tuples of type (f, v), for an expression f and a
vertex v, is said to be minimized (with respect to ≺) if for any (f, v), (f 0 , v 0 ) ∈ X,
(f, v) and (f 0 , v 0 ) are not comparable with respect to ≺.
2
This step needs a further refinement to distinguish between an approximate solution
and an optimal solution. It is not entirely straightforward, but it can be handled at
the same complexity. We defer the reader to the full version of the paper.
 Optimal Paths in Weighted Timed Automata 61

The algorithm we present computes a labelling function l that maps any

vertex u of GA (ϑ) to a minimized set of pairs (f, v) for which there exist a path
π and a state s ∈ S such that:
– π is a shortest path of GA (ϑ(s)) from u to a vertex corresponding to T ,
– the first edge e of π connects u to v, and
– the cost of π is given by f (ϑ(s)).
We can summarize our algorithm in the following steps:
1. Initialize l by assigning l(u) = {(0, . . . , 0, u)} for u corresponding to a state
in T , and l(u) = ∅ for all remaining vertices.
2. repeat
l0 ← l; l ← Update(l’)
until l0 = l
3. Output l.
We just need to specify the function Update. Consider an edge e a vertex
u = hq, α, (i1 , . . . , ih )i. We have the following cases:
– e is an immediate switch from u to v: for (a0 , . . . , aN +1 , v 0 ) ∈ l0 (v), define
(a00 , . . . , a0N +1 , v) such that a00 = a0 + ce , and a0i = ai for i = 1, . . . , (N + 1),
where ce is the cost of e;
– e is a time edge from u to v: for any (a0 , . . . , aN +1 , v 0 ) ∈ l0 (v), define
(a00 , . . . , a0N +1 , v) such that if e is obtained by rows 1 and 2 of Table 1 and
i ∈ I(ih , i1 ), then a0i = ai + J d (q), otherwise a0i = ai ;
– the edge e is a delayed switch from u to v: for any (a0 , . . . , aN +1 , v 0 ) ∈ l0 (v),
define (a00 , . . . , a0N +1 , v) such that if e is obtained by rows 1, 2 and 4 of Table
2 and i ∈ I(ih , i1 ), then a0i = ai + J d (q), otherwise a0i = ai .
Let l00 (u) be the set of all the tuples generated for u. After executing l ←
Update(l0 ), l(u) contains the set obtained deleting from l0 (u) ∪ l00 (u) all the
tuples (f, v) such that f 0 ≺ f for some (f 0 , v 0 ) ∈ l0 (u) ∪ l00 (u). Moreover, once
the function l is output, it is easy to determine the optimal cost and generate
the corresponding solution from l and the graph GA (ϑ), given ϑ. We observe
that each of the tuples (f, v) belonging to l(u) corresponds to a path from u to
a target vertex. Thus the cardinality of l(u) is bounded above by the number of
simple paths in GA (ϑ). Hence we have the following theorem.
Theorem 4. The zone optimal-run problem can be solved in doubly-exponential
time.
If we restrict to timed automata with just one clock variable, it is possible to
solve the zone optimal-run problem in singly exponential time. We consider the
algorithm given in [KO81,YTO91] to solve a particular shortest-path problem
with only a parameter ϑ and edge costs given by (c − ϑ), for constants c. This
algorithm runs in polynomial time and can be modified in order to obtain a
polynomial time algorithm to solve the parametric shortest-path problem with
edge costs given by a first-degree polynomial of ϑ (ϑ ∈ [0, 1]).
Theorem 5. The zone optimal-run problem for automata with one clock vari-
able can be solved in exponential time.
62 R. Alur, S. La Torre, and G.J. Pappas

References
ACH93. R. Alur, C. Courcoubetis, and T.A. Henzinger. Computing accumulated
delays in real-time system. In Proc. of the Fifth International Conference on
Computer-Aided Verification, CAV’93, LNCS 697, pages 181 – 193, 1993.
AD94. R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer
Science, 126:183 – 235, 1994.
AM99. E. Asarin and O. Maler. As soon as possible: Time optimal control for timed
automata. In Proc. of the 2nd International Workshop on Hybrid Systems:
Computation and Control, LNCS 1569, pages 19 – 30, 1999.
AMP95. E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete
and timed systems. In Proc. of the 2nd International Workshop on Hybrid
Systems, LNCS 999, pages 1 – 20, 1995.
BHF+ . G. Behrman, T. Hune, A. Fehnker, K. Larsen, P. Pettersson, R. Romijn, and
F. Vaandrager. Minimum-cost reachability for priced timed automata. In
this Volume.
Chu62. A. Church. Logic, arithmetic, and automata. In Proc. of the International
Congress of Mathematics, pages 23–35, 1962.
CY91. C. Courcoubetis and M. Yannakakis. Minimum and maximum delay prob-
lems in real-time systems. In Proc. of the 3rd International Conference on
Computer Aided Verification, LNCS 575, pages 399 – 409, 1991.
KO81. R. M. Karp and J. R. Orlin. Parametric shortest path algorithm with an
application to cyclic staffing. Discrete Applied Math., 3:37 – 45, 1981.
LTS99. J. Lygeros, C. Tomlin, and S.S. Sastry. Controllers for reachability specifica-
tions for hybrid systems. Automatica, 35(3):349–370, March 1999.
MPS95. O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers
for timed systems. In Proc. of the 12th Annual Symposium on Theoretical
Aspects of Computer Science, STACS’95, LNCS 900, pages 229 – 242, 1995.
NTY00. P. Nierbert, S. Tripakis, and S. Yovine. Minimum-time reachability for timed
automata. In Proc. of the 8-th IEEE Mediterranean Conference on Control
and Automation, 2000.
SPS00. O. Shakernia, G. J. Pappas, and S. Sastry. Decidable controller synthesis
for classes of linear systems. In Proc. of the 3rd International Workshop on
Hybrid Systems: Computation and Control, HSCC’00, LNCS 1790, pages 407
– 420, 2000.
Tho95. W. Thomas. On the synthesis of strategies in infinite games. In Ernst W.
Mayr and Claude Puech, editors, 12th Annual Symposium on Theoretical
Aspects of Computer Science, STACS’95, LNCS 900, pages 1 – 13, 1995.
WT97. H. Wong-Toi. The synthesis of controllers for linear hybrid automata. In
Proc. of the 36th IEEE CDC, San Diego, CA, December 1997.
YTO91. N. E. Young, R. Tarjan, and J. Orlin. Faster parametric shortest path and
minimum balance algorithms. Networks, 21 (2):205 – 221, 1991.