BRICS Basic Research in Computer Science

(1)

B R ICS R S -01-3 B eh rman n et a l.: M in imu m -Cost Reach a b ility for Priced T imed A u tomata

BRICS

Basic Research in Computer Science

Minimum-Cost Reachability for Priced Timed Automata

Gerd Behrmann Ansgar Fehnker Thomas S. Hune Kim G. Larsen Paul Pettersson Judi Romijn

Frits W. Vaandrager

BRICS Report Series RS-01-3

(2)

Copyright c 2001, Gerd Behrmann & Ansgar Fehnker &

Thomas S. Hune & Kim G. Larsen & Paul Pettersson & Judi Romijn & Frits W.

Vaandrager.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications.

Copies may be obtained by contacting:

BRICS

Department of Computer Science University of Aarhus

Ny Munkegade, building 540 DK–8000 Aarhus C

Denmark

Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk ftp://ftp.brics.dk

This document in subdirectory RS/01/3/

(3)

Minimum-Cost Reachability for Priced Timed Automata

^?

Gerd Behrmann¹, Ansgar Fehnker^3†, Thomas Hune², Kim Larsen¹ Paul Pettersson^4‡, Judi Romijn³, and Frits Vaandrager³

1 Basic Research in Computer Science, Aalborg University, E-mail:{behrmann,kgl}@cs.auc.dk.

2 Basic Research in Computer Science, Aarhus University, E-mail:baris@brics.dk.

3 Computing Science Institute, University of Nijmegen, E-mail:{ansgar,judi,fvaan}@cs.kun.nl.

4 Department of Computer Systems, Information Technology, Uppsala University, E-mail:paupet@docs.uu.se.

Abstract. This paper introduces the model oflinearly priced timed au- tomataas an extension of timed automata, with prices on both transitions and locations. For this model we consider the minimum-cost reachability problem: i.e. given a linearly priced timed automaton and a target state, determine the minimum cost of executions from the initial state to the target state. This problem generalizes the minimum-time reachability problem for ordinary timed automata. We prove decidability of this problem by offering an algorithmic solution, which is based on a combination of branch-and-bound techniques and a new notion of priced regions. The latter allows symbolic representation and manipulation of reachable states together with the cost of reaching them.

Keywords:Timed Automata, Verification, Data Structures, Algorithms, Optimization.

1 Introduction

Recently, real-time verification tools such as Uppaal [13], Kronos [6] and HyTech [10], have been applied to synthesize feasible solutions to static job- shop scheduling problems [8, 12, 17]. The basic common idea of these works is to reformulate the static scheduling problem as a reachability problem that can be solved by the verification tools. In this approach, the timed automata [3] based modeling languages of the verification tools serve as the basic input language

?This work is partially supported by the European Community Esprit-LTR Project 26270 VHS (Verification of Hybrid Systems).

† Research supported by Netherlands Organization for Scientific Research (NWO) under contract SION 612-14-004.

‡ Research partly sponsored by the AIT-WOODDES Project No IST-1999-10069.

(4)

in which the scheduling problem is described. These modeling languages have proven particularly well-suited in this respect, as they allow for easy and flexible modeling of systems, consisting of several parallel components that interact in a time-critical manner and constrain each other’s behavior in a multitude of ways.

In this paper we introduce the model oflinearly priced timed automataand offer an algorithmic solution to the problem of determining the minimum cost of reaching a designated set of target states. This result generalizes previous results on computation of minimum-time reachability and accumulated delays in timed automata, and should be viewed as laying a theoretical foundation for algorithmic treatments of more general optimization problems as encountered in static scheduling problems.

As an example consider the very simple static scheduling problem represented by the timed automaton in Fig. 1 from [16], which contains 5 ’tasks’

{A, B, C, D, E}. All tasks are to be performed precisely once, except task C, which should be performedat leastonce. The order of the tasks is given by the timed automaton, e.g. taskB must not commence before taskAhas finished. In addition, the timed automaton specifies three timing requirements to be satisfied: the delay between the start of the first execution of taskCand the start of the execution ofEshould be at least 3 time units; the delay between the start of the last execution ofC and the start ofD should be no more than 1 time unit;

and, the delay between the start of B and the start of D should be at least 2 time units, each of these requirements are represented by a clock in the model.

Using a standard timed model checker we are able to verify that location E of

A x:= 0 B y:= 0 C D E

z:= 0 x≥2

y≤1 z≥3

y:= 0

Fig. 1.Timed automata model of scheduling example.

the timed automaton is reachable. This can be demonstrated by a trace leading to the location¹:

(A,0,0,0)−→^τ −−→⁽¹⁾ (B,1,1,1)−→^τ −−→⁽¹⁾ (C,2,1,1)−→^τ −−→⁽²⁾ (D,4,3,3)−→^τ (E,4,3,3) (1) The above trace may be viewed as a feasible solution to the original static scheduling problem. However, given an optimization problem, one is often not satisfied with an arbitrary feasible solution but insist on solutions which areopti- malin some sense. When modeling a problem like this one using timed automata

1 Here a quadruple (X, v^x, v^y, v^z) denotes the state of the automaton in which the control location is X and wherevx, vy and vz give the values of the three clocks x,y andz. The transitions labelled τ are actual transitions in the model, and the transitions labelled(d) represents a delay ofdtime units.

(5)

A B1 C D

β 1

1

1 E

0 0 0 0

x:= 0

y:= 0 z:= 0

x≥2

y≤1 z≥3

y:= 0 α

Fig. 2.A linearly priced timed automaton.

an obvious notion of optimality is that of minimum accumulated time. For the timed automaton of Fig. 1 the trace of (1) has an accumulated time-duration of 4. This, however, is not optimal as witnessed by the following alternative trace, which by exploiting the looping transition on C reaches E within a total of 3 time-units²:

(A,0,0,0)−→^τ −→^τ −−→⁽²⁾ (C,2,2,2)−→^τ (C,2,0,2)−→^τ −−→⁽¹⁾ (D,3,1,3)−→^τ (E,3,1,3) (2) In [4] algorithmic solutions to the minimum-time reachability problem and the more general problem of controller synthesis has been given using a backward fix-point computation. In [16] an alternative solution based on forward reachability analysis is given, and in [5] an algorithmic solution is offered, which applies branch-and-bound techniques to prune parts of the symbolic state-space which are guaranteed not to contain optimal solutions. In particular, by introducing an additional clock for accumulating time-elapses, the minimum-time reachability problem may be dealt with using the existing efficient data structures (e.g.

DBMs [7], CDDs [14] and DDDs [15]) already used in the real-time verification tools Uppaal and Kronos for reachability. The results of the present paper also extends the work in [2] which provides an algorithm for computing the accumulated delay in a timed automata.

In this paper, we provide the basis for dealing with more general optimization problems. In particular, we introduce the model of linearly priced timed automata, as an extension of timed automata with priceson both transitions and locations: the price of a transition gives the cost for taking it and the price on a location specifies the costper time-unit for staying in that location. This model can capture not only the passage of time, but also the way that e.g. tasks with different prices for use per time unit, contributes to the total cost. Figure 2 gives a linearly priced extension of the timed automaton from Fig. 1. Here, the price of locationDis set toβand the price on all other locations is set to 1 (thus simply accumulating time). The price of the looping transition onCis set toα, whereas all other transitions are free of cost (price 0). Now for (α, β) = (1,3) the costs of the traces (1) and (2) are 8 and 6, respectively (thus it is cheaper to actually exploit the looping transition). For (α, β) = (2,2) the costs of the two traces are both 6, thus in this case it is immaterial whether the looping

2 In fact, 3 is the minimum time for reachingE.

(6)

transition is taken or not. In fact, the optimal cost of reachingEwill in general be the minimum of 2 + 2∗β and 3 +α, and the optimal trace will include the looping transition onC depending on the particular values ofαandβ.

In this paper we deal with the problem of determining the minimum cost of reaching a given location for linearly priced timed automata. In particular, we offer an algorithmic solution to this problem³. In contrast to minimum-time reachability for timed automata, the minimum-cost reachability problem for linearly priced timed automata requires the development of new data structures for symbolic representation and the manipulation of reachablesetsof statesto- gether with the cost of reaching them. In this paper we put forward one such data structure, namely a priced extension of the fundamental notion of clock regionsfor timed automata [3].

The remainder of the paper is structured as follows: Section 2 formally introduces the model of linearly priced timed automata together with its semantics.

Section 3 develops the notion of priced clock regions, together with a number of useful operations on these. The priced clock regions are then used in Sec- tion 4 to give a symbolic semantics capturing (sufficiently) precisely the cost of executions and used as a basis for an algorithm solution to the minimum-cost problem. Finally, in Section 5 we give some concluding remarks.

2 Linearly Priced Timed Automata

In this section, we introduce the model of linearly priced timed automata, which is an extension of timed automata [3] with prices on both locations and transitions. Dually, linearly priced timed automata may be seen as a special type of linear hybrid automata [9] or multirectangular automata [9] in which the accu- mulation of prices (i.e. the cost) is represented by a single continuous variable.

However, in contrast to known undecidability results for these classes, minimum- cost reachability is computable for linearly priced timed automata. An intuitive explanation for this is that the additional (cost) variable does not influence the behavior of the automata.

Let C be a finite set of clocks. Then B(C) is the set of formulas obtained as conjunctions of atomic constraints of the form x ./ n where x ∈ C, n is natural number, and ./ ∈ {<,≤,=,≥, >}. Elements of B(C) are called clock constraintsoverC. Note that for each timed automaton that has constraints of the formx−y ./ c, there exists a strongly bisimilar timed automaton with only constraints of the formx ./ c. Therefore, the results in this paper are applicable to automata having constraints of the typex−y ./ cas well.

Definition 1 (Linearly Priced Timed Automaton). A Linearly Priced Timed Automaton (LPTA) over clocksCand actionsActis a tuple(L, l₀, E, I, P) where L is a finite set of locations, l₀ is the initial location, E ⊆L× B(C)× Act× P(C)×Lis the set of edges,I:L→ B(C)assigns invariants to locations,

3 Thus settling an open problem given in [4].

(7)

A B C

3 1 4

x <= 2 xx >:= 01

5 1

Fig. 3.An example LPTA.

andP : (L∪E)→Nassigns prices to both locations and edges. In the case of (l, g, a, r, l⁰)∈E, we writel−−−→^g,a,r l⁰.

Formally, clock values are represented as functions calledclock assignments fromC to the non-negative realsR_≥0. We denote byR^C the set of clock assignments for C ranged over by u, u⁰ etc. We define the operation u⁰ = [r 7→ 0]u to be the assignment such that u⁰(x) = 0 ifx∈rand u(x) otherwise, and the operationu⁰ =u+dto be the assignment such thatu⁰(x) =u(x) +d. Also, a clock valuationusatisfies a clock constraintg,u∈g, ifu(x)./ nfor any atomic constraintx ./ ning. Notice that the set of clock valuations satisfying a guard is always a convex set.

The semantics of a LPTAAis defined as a transition system with the state- space L×R^C, with initial state (l₀, u₀) (whereu₀ assigns zero to all clocks in C), and with the following transition relation:

– (l, u)−−−→⁽^d⁾^,p (l, u+d) ifu+d∈I(l), andp=P(l)∗d.

– (l, u)−−→^a,p (l⁰, u⁰) if there existsg,rsuch thatl−−−→^g,a,r l⁰,u∈g,u⁰= [r7→0]u, u⁰∈I(l⁰) andp=P((l, g, a, r, l⁰)).

Note that the transitions are decorated with two labels: a delay-quantity or an action, together with the cost of the particular transition. For determining the cost, the price of a location gives the cost rate of staying in that location (per time unit), and the price of a transition gives the cost of taking that transition.

In the remainder, states and executions of the transition system for LPTA A will be referred to as states and executions ofA.

Definition 2 (Cost). Let α = (l₀, u₀) −−−→^a¹^,p¹ (l₁, u₁). . . −−−−→^aⁿ^,pⁿ (ln, un) be a finite execution of LPTAA. Thecostofα,cost(α), is the sumΣi∈{1,...,n}pi.

For a given state(l, u), the minimal cost of reaching(l, u),mincost((l, u)), is the infimum of the costs of finite executions ending in(l, u). Similarly, the min- imal cost of reaching a locationlis the infimum of the costs of finite executions ending in a state of the form(l, u).

mincost(l) = inf{cost(α)|αa run ending in locationl}

Example 1. Consider the LPTA of Fig. 3. The LPTA has a single clock x, and the locations and transitions are decorated with guards and prices. A sample execution of this LPTA is for instance:

(A,0)−−−−−−→⁽¹^.⁵⁾^,⁴^.⁵ (A,1.5)−−→^τ,⁵ (B,1.5)−−→^τ,¹ (C,1.5)

(8)

The cost of this execution is 10.5. In fact, there are executions with cost ar- bitrarily close to the value 7, obtainable by avoiding delaying in location A, and delaying just long enough in location B. Due to the infimum definition of mincost, it follows thatmincost(C) = 7. However, note that because of the strict comparison in the guard of the second transition, no execution actually achieves

this cost. 2

3 Priced Clock Regions

For ordinary timed automata, the key to decidability results has been the valu- able notion of region [3]. In particular, regions provide a finite partitioning of the uncountable set of clock valuations, which is also stable with respect to the various operations needed for exploration of the behavior of timed automata (in particular the operations of delay and reset).

In the setting of linearly priced timed automata, we put forward a new ex- tended notion ofpriced region. Besides providing a finite partitioning of the set of clock-valuations (as in the case of ordinary regions), priced regions also associate costs to each individual clock-valuation within the region. However, as we shall see in the following, priced regions may be presented and manipulated in a symbolic manner and are thus suitable as an algorithmic basis.

Definition 3 (Priced Regions). Given set S, let Seq(S)be the set of finite sequences of elements ofS. A priced clock regionover a finite set of clocksC

R= (h,[r₀, . . . , rk],[c₀, . . . , cl])

is an element of (C → N)×Seq(2^C)×Seq(N), with k =l, C = ∪i∈{0,...,k}ri, ri∩rj =∅wheni6=j, andi >0 implies thatri 6=∅.

Given a clock valuationu∈R^C, and regionR= (h,[r₀, . . . , rk],[c₀, . . . , ck]), u∈Riff

1. handuagree on the integer part of each clock inC, 2. x∈r₀ ifffrac(u(x)) = 0,

3. x, y∈ri⇒frac(u(x)) =frac(u(y)), and

4. x∈ri,y∈rj andi < j ⇒frac(u(x))<frac(u(y)).

For a priced region R = (h,[r₀, . . . , rk],[c₀, . . . , ck]) the first two components of the triple constitute an ordinary (unpriced) region ˆR= (h,[r₀, . . . , rk]). The naturals c₀, . . . , ck are the costs, which are associated with the vertices of the closure of the (unpriced) region, as follows. We start in the left-most lower vertex of the exterior of the region and associate cost c₀ with it, then move one time unit in the direction of set rk to the next vertex of the exterior, and associate costc₁with that vertex, then move one unit in the direction ofrk−1, etc. In this way, the costsc₀, . . . , ck, span a linear cost plane on thek-dimensional unpriced region.

(9)

The closure of the unpriced regionR is the convex hull of the vertices. Each clock valuationu∈Ris a (unique) convex combination⁴ of the vertices. There- fore the cost ofucan be defined as the same convex combination of the cost in the vertices. This gives the following definition:

Definition 4 (Cost inside Regions).Given priced regionR= (h,[r₀, . . . , rk], [c₀, . . . , ck])and clock valuationu∈R, thecostofuinR is defined as:

cost(u, R) =c₀+

kX−1

i=0

frac(u(xk−i))∗(ci+1−ci)

wherexjis some clock inrj. The minimal cost associated withRismincost(R) = min({c₀, . . . , ck}).

Fig. 4.A three dimensional priced region.

In the symbolic state-space, constructed with the priced regions, the costs will be computed such that for each concrete state in a symbolic state, the cost associated with it is the minimal cost for reaching that state by the symbolic path that was followed. In this way, we always have the minimal cost of all concrete paths represented by that symbolic path, but there may be more symbolic paths leading to a symbolic state in which the costs are different. Note that the cost of a clock valuation in the region is computed by adding fractions of costs for equivalence sets of clocks, rather than for each clock.

To prepare for the symbolic semantics, we define in the following a number of operations on priced regions. These operations are also the ones used in the algorithm for finding the optimal cost of reaching a location.

The delay operation computes the time successor, which works exactly as in the classical (unpriced) regions. The changing dimensions of the regions cause the addition or deletion of vertices and thus of the associated cost. The price

4 A linear expressionP

aⁱvⁱwhereP

aⁱ= 1, andaⁱ≥0.

(10)

Fig. 5.Delay and reset operations for two-dimensional priced regions.

argument will be instantiated to the price of the location in which time is passing;

this is needed only when a vertex is added. The two cases in the operation are illustrated in Fig. 5 to the left (5.1) and (5.2).

Definition 5 (Delay). Given a priced region R = (h,[r₀, . . . , rk],[c₀, . . . , ck]) and a pricep, the functiondelayis defined as follows:

1. Ifr₀ is not empty, then

delay(R, p) = (h,[∅, r0, . . . , rk],[c₀, . . . , ck, c₀+p]) 2. Ifr₀ is empty, then

delay(R, p) = (h⁰,[rk, r₁, . . . , rk−1],[c₁, . . . , ck]) whereh⁰=hincremented for all clocks inrk

When resetting a clock, a priced region may lose a dimension. If so, the two costs, associated with the vertices that are collapsed, are compared and the minimum is taken for the new vertex. Two of the three cases in the operation is illustrated in Fig. 5 to the right (6.2) and (6.3).

Definition 6 (Reset). Given a priced regionR = (h,[r₀, . . . , rk],[c₀, . . . , ck]) and a clockx∈ri, the functionreset is defined as follows:

1. If i= 0 thenreset(x, R) = (h⁰,[r₀, . . . , rk],[c₀, . . . , ck]), whereh⁰=hwithx set to zero

2. Ifi >0 andri6={x}, then

reset(x, R) = (h⁰,[r₀∪ {x}, . . . , ri\ {x}, . . . , rk],[c₀, . . . , ck]) whereh⁰=hwithxset to zero

(11)

3. Ifi >0 andri={x}, then

reset(x, R) = (h⁰,[r₀∪ {x}, . . . , ri−1, ri+1, . . . , rk], [c₀, . . . , ck−i−1, c⁰, ck−i+2, . . . , ck]) wherec⁰=min(ck−i, ck−i+1)

h⁰=hwithxset to zero

The reset operation on a set of clocks:reset(C∪ {x}, R) =reset(C,reset(x, R)), andreset(∅, R) =R.

The price argument in the increment operation will be instantiated to the price of the particular transition taken; all costs are updated accordingly.

Definition 7 (Increment).Given a priced regionR=(h,[r₀, . . . , rk],[c₀, . . . , ck]) and a price p, the increment of R with respect to p is the priced region R⊕p= (h,[r₀, . . . , rk],[c⁰₀, . . . , c⁰_k])where c⁰_i=ci+p.

If in region R, no clock has fractional part 0, then time may pass in R, that is, each clock valuation in R has a time successor and predecessor inR. When changing location withR, we must choose for each clock valuationuinRbetween delaying in the previous location until uis reached, followed by the change of location, or changing location immediately and delaying touin the new location.

This depends on the price of either location. For this the following operationself is useful.

Definition 8 (Self ).Given a priced regionR=(h,[r₀, . . . , rk],[c₀, . . . , ck])and a pricep, the functionselfis defined as follows:

1. Ifr₀ is not empty, thenself(R, p) =R.

2. Ifr₀ is empty, then

self(R, p) = (h,[r₀, . . . , rk],[c₀, . . . , ck−1, c⁰]) wherec⁰= min(ck, c₀+p)

Definition 9 (Comparison). Two priced regions may be compared only if their unpriced versions are equal:(h,[r₀, . . . , rk],[c₀, . . . , ck])≤(h⁰,[r₀⁰, . . . , r⁰_k0], [c⁰₀, . . . , c⁰_k0])iffh=h⁰,k=k⁰, and for0≤i≤k:ri=r⁰i andci≤c⁰i.

The operationsdelayandselfsatisfy the following useful properties:

Proposition 1 (Interaction Properties).

1. self(R, p)≤R,

2. self(self(R, p), p) =self(R, p), 3. delay(self(R, p), p)≤delay(R, p), 4. self(delay(R, p), p) =delay(R, p), 5. self(R⊕q, p) =self(R, p)⊕q, 6. delay(R⊕q, p) =delay(R, p)⊕q,

7. Forg∈ B(C), wheneverR∈g thenself(R, p)∈g.

(12)

Proof. Directly from the definitions of the operators and≤. 2 Stated in terms of the cost,cost(u, R), of an individual clock valuation,u, of a priced region,R, the symbolic operations behave as follows:

Proposition 2 (Cost Relations).

1. Let R= (h,[r₀, . . . , rk],[c₀, . . . , ck]). Ifu∈R andu+d∈Rthen cost(u+ d, R) =cost(u, R) +d∗(ck−c₀).

2. IfR=self(R, p),u∈Randu+d∈delay(R, p)thencost(u+d,delay(R, p)) = cost(u, R) +d∗p.

3. cost(u,reset(x, R)) =inf{cost(v, R)|[x7→0]v=u}.

Proof. Directly from the definitions of the operators andcost. 2

4 Symbolic Semantics and Algorithm

In this section, we provide a symbolic semantics for linearly priced timed automata based on the notion of priced regions and the associated operations presented in the previous section. As a main result we shown that the cost of an execution of the underlying automaton is captured sufficiently accurately.

Finally, we present an algorithm based on priced regions.

Definition 10 (Symbolic Semantics). The symbolic semantics of an LPTA A is defined as a transition system with the states L×((C →N)×Seq(2^C)× Seq(N)), with initial state(l₀,(h₀,[C],[0]))(whereh₀ assigns zero to the integer part of all clocks inC), and with the following transition relation:

– (l, R)→(l,delay(R, P(l))) ifdelay(R, P(l))∈I(l).

– (l, R) → (l⁰, R⁰) if there exists g, r such that l −−−→^g,a,r l⁰, R ∈ g, R⁰ = reset(R, r)⊕P((l, g, a, r, l⁰))andR⁰∈I(l⁰).

– (l, R)→(l,self(R, P(l)))

In the remainder, states and executions of the symbolic transition system for LPTAAwill be referred to as the symbolic states and executions ofA.

Lemma 1. Given LPTAA, for each executionαofAthat ends in state(l, u), there is a symbolic execution β of A, that ends in symbolic state (l, R), such thatu∈R, andcost(u, R)≤cost(α).

Proof. For this proof we first observe that, giveng∈ B(C), ifu∈R andu∈g, thenR∈g.

We prove this by induction on the length ofα. Supposeαends in state (l, u).

The base step concernsαwith length 0, consisting of only the initial state (l₀, u₀) whereu₀is the valuation assigning zero to all clocks. Clearly,cost(α) = 0. Since the initial state of the symbolic semantics is the state (l₀,(h₀,[C],[0])), in which h₀assigns zero to the integer part of all clocks, and the fractional part of all clocks is zero, we can takeβ to be (l₀,(h₀,[C],[0])). Clearly, there is only one valuation

(13)

u∈(h₀,[C],[0]), namely the valuationuthat assigns zero to all clocks, which is exactlyu₀, and by definition,cost(u₀,(h₀,[C],[0])) = 0 and trivially 0≤0.

For the induction step, assume the following. We have an execution α⁰ in the concrete semantics, ending in (l⁰, u⁰), a corresponding execution β⁰ in the symbolic semantics, ending in (l⁰, R⁰), such that u⁰ ∈ R⁰, and cost(u⁰, R⁰) ≤ cost(α⁰).

Suppose (l⁰, u⁰) −−→^a,p (l, u). Then there is a transition l⁰ −−−→^a,g,r l in the automaton A such that u∈ g,u = [r 7→ 0]u⁰, u ∈I(l) andp= P((l⁰, a, g, r, l)).

Nowu⁰∈gimplies thatR⁰∈g. LetR=reset(R⁰, r)⊕p. It is easy to show that u= [r7→0]u⁰ ∈Rand asu∈Rwe then have thatR∈I(l). So (l⁰, R⁰)→(l, R) and

cost(u, R) = inf{cost(v, R⁰)|[r7→0]v=u} +p

≤ cost(u⁰, R⁰) +p

≤^IHcost(α⁰) +p

= cost(α)

Suppose (l⁰, u⁰) −−−−−→⁽^d⁾^,p^∗^d (l, u), where p = P(l), i.e. l = l⁰, u = u⁰ +d, andu∈I(l). Now there exist sequencesRo, R₁, . . . , Rmandd₁, . . . , dmof price regions and delays such thatd=d₁+· · ·+dm,R₀=R⁰ and fori∈ {1, . . . , m}, Ri =delay(Ri−1, p) withu⁰+Pi

k=1dk ∈Ri. This defines the sequence of regions wisited without considering cost. To obtain the priced regions with the optimal cost we apply the self operation. Let R⁰₀ = self(R₀, p) and for i ∈ {1, . . . , m} let R⁰_i = delay(R_i⁰₋₁, p) (in fact, for i ∈ {1, . . . , m}, R⁰_i = self(R⁰_i, p) due to Proposition 1.4 andR_i⁰ ≤Ri). Clearly we have the following symbolic extension ofβ⁰:

β⁰→(l⁰, R⁰₀)→ · · · →(l⁰, R_m⁰ )

Now by Proposition 2.2 (the condition of Proposition 2.2 is satisfied for all R_i⁰(i≥0) because of Proposition 1.4:

cost(u⁰+d, R⁰m) = cost(u⁰, R⁰₀) +d∗p

≤ cost(u⁰, R⁰) +d∗p

≤^IHcost(α⁰) +d∗p

= cost(α)

2 Lemma 2. Whenever (l, R) is a reachable symbolic state and u ∈ R, then mincost((l, u))≤cost(u, R).

Proof. The proof is by induction on the length of the symbolic traceβ reaching (l, R). In the base case, the length ofβ is 0 and (l, R) = (l₀, R₀), whereR₀is the initial price region (h₀,[C],[0]) in whichh₀ associates 0 with all clocks. Clearly, there is only one valuationu∈R₀, namely the valuation which assigns 0 to all clocks. Obviously,mincost((l₀, u₀)) = 0≤cost(u₀, R₀) = 0.

(14)

For the induction step, assume that (l, R) is reached by a traceβ with length greater than 0. In particular, let (l⁰, R⁰) be the immediate predecessor of (l, R) in β. Let u ∈ R. We consider three cases depending on the type of symbolic transition from (l⁰, R⁰) to (l, R).

Case 1: Suppose (l⁰, R⁰) → (l, R) is a symbolic delay transition. That is, l = l⁰, R = delay(R⁰, p) with p = P(l) and R ∈ I(l). We consider two sub-cases depending on whetherR⁰ is self-delayable or not⁵.

Assume that R⁰ is not self-delayable, i.e.R⁰ = (h⁰,[r₀⁰, . . . , r⁰_k],[c⁰₀, . . . , c⁰_k]) with r⁰₀ 6= ∅. Then R = (h⁰,[∅, r₀⁰, . . . , r⁰_k],[c⁰₀, . . . , c⁰_k, c⁰₀ +p]). Let x ∈ r₀⁰ and let u⁰ =u−d where d= frac(u(x)). Then u⁰ ∈ R⁰ and (l⁰, u⁰) −−−→⁽^d⁾^,q (l, u) where q=d∗p. Thusmincost((l, u))≤mincost((l⁰, u⁰)) +d∗p. By induction hypothesis, mincost((l⁰, u⁰))≤cost(u⁰, R⁰), and ascost(u, R) =cost(u⁰, R) +d∗p, we obtain, as desired,mincost((l, u))≤cost(u, R).

Assume that R⁰ is self-delayable. That is, R⁰ = (h⁰,[r⁰₀, r⁰₁, . . . , r_k⁰],[c⁰₀, . . . , c⁰_k]) withr₀⁰ =∅andR= (h⁰⁰,[r⁰_k, r₁⁰, . . . , r_k⁰₋₁],[c⁰₁, . . . , c⁰_k]). Now, letx∈r⁰₁. Then for anyd <frac(u(x)) we letud=u−d. Clearly,ud∈R⁰ and (l, ud)−−−−−→⁽^d⁾^,p^∗^d (l, u).

Now,

mincost((l, u)) ≤ mincost((l, ud)) +p∗d

≤^IHcost(ud, R⁰) +p∗d

Nowcost(u, R) =cost(ud, R⁰)+(c⁰_k−c⁰₀)∗dso it is clear thatcost(ud, R⁰)+k∗d→ cost(u, R) whend→0 for anyk. In particular,cost(ud, R⁰) +p∗d→cost(u, R) whend→0. Thus mincost((l, u))≤cost(u, R) as desired.

Case 2: Suppose (l⁰, R⁰) → (l, R) is a symbolic action transition. That is R = reset(R⁰, r)⊕p for some transition l⁰ −−−→^g,a,r l of the automaton with R⁰ ∈ g and p=P((l⁰, g, a, r, l)). Now letv ∈R⁰ such that [r 7→0]v =u. Then clearly (l⁰, v)−−→^a,p (l, u). Thus:

mincost((l, u)) ≤ inf{mincost((l, v))|v∈R⁰,[r7→0]v=u}

≤^IHinf{cost(v, R⁰)|[r7→0]v=u}

= cost(u, R) by Proposition 2.3

Case 3:Suppose (l⁰, R⁰)→(l, R) is a symbolic self-delay transition. Thus, in par- ticularl=l⁰. IfR=R⁰the lemma follows immediately by applying the induction hypothesis to (l⁰, R⁰). Otherwise,R⁰is self-delayable andR⁰ andRare identical except for the cost of the ‘last’ vertex; i.e.R⁰= (h,[r₀, . . . , rk],[c₀, . . . , ck−1, ck]) and R = (h,[r₀, . . . , rk],[c₀, . . . , ck−1, c₀+p]) with r₀ = ∅, c₀ +p < ck and p= P(l). Now let x ∈ r₁. Then for any d > u(x) we let ud =u−d. Clearly, ud∈R(andud∈R⁰) and (l, ud)−−−−−→⁽^d⁾^,p^∗^d (l, u). Now:

mincost((l, u)) ≤ mincost((l, ud)) +p∗d

≤^IHcost(ud, R⁰) +p∗d

5 A priced region,R= (h,[r0, . . . , rk],[c0, . . . , ck]), is self-delayable wheneverr0=∅.

(15)

i ii

Fig. 6.Two reachable sets of priced regions.

Now let R⁰⁰ = (h,[r₁, . . . , rk],[c₀, . . . , ck−1]). Then R = delay(R⁰⁰, p) and R⁰ = delay(R⁰⁰, ck−c₀). Now cost(ud, R⁰) = cost(uu(x), R⁰⁰) + (ck −c₀)∗(d−u(x)) which converges to cost(uu(x), R⁰⁰) when d → u(x). Thus cost(ud, R⁰) +p∗ d → cost(uu(x), R⁰⁰) +p∗d = cost(u, R) for d → u(x). Hence, as desired,

mincost((l, u))≤cost(u, R). 2

Combining the two lemmas we obtain as a main theorem that the symbolic semantics captures (sufficiently) accurately the cost of reaching states and locations:

Theorem 1. Letlbe a location of a LPTA A. Then

mincost(l) =min({mincost(R)|(l, R)is reachable})

Example 2. We now return to the linearly priced timed automaton in Fig. 2 where the value of both α and β is two, and look at its symbolic state-space.

The shaded area in Fig. 6(i) including the lines in and around the shaded area represents some of the reachable priced regions in location B after time has passed (a number of delay actions have been taken). Only priced regions with integer values up to 3 are shown. The numbers are the cost of the vertices. The shaded area in Fig. 6(ii) represents in a similar way some of the reachable priced regions in locationCafter time has passed. For a more elaborate explanation of the reachable state-space we refer to the appendix. 2 The introduction of priced regions provides a first step towards an algorithmic solution for the minimum-cost reachability problem. However, in the present form both the integral part as well as the cost of vertices of priced regions may grow beyond any given bound during symbolic exploration. In the unpriced case, the growth of integral parts is often dealt with by suitable abstractions of (unpriced) regions, taking the maximal constant of the given timed automaton into account. Here we have chosen a very similar approach exploiting the fact, that any LPTAA may be transformed into an equivalent “bounded” LPTA ˜A in the sense thatAand ˜Areaches the same locations with the exact same cost.

(16)

Theorem 2. LetA= (L, l₀, E, I, P) be a LPTA with maximal constantmax.

Then there exists a bounded time equivalent ofA, A˜= (L, l₀, E⁰, I⁰, P⁰), satis- fying the following:

1. Whenever (l, u)is reachable inA, then for all˜ x∈C, u(x)≤max +2.

2. For any location l ∈ L, l is reachable with costc in A if and only if l is reachable with costc inA˜

Proof. We construct ˜A = (L, l₀, E ∪E⁰, I⁰, P⁰), as follows. E⁰ = {(l, x ==

maxA(x)+2, τ, x:=maxA(x)+1, l)|x∈C, l∈L}. Forl∈L,I⁰(l) =I(l)V

x∈Cx≤ maxA(x) + 2, P⁰(l) =P(l). Fore∈ (E∪E⁰), ife ∈E then P⁰(e) =P(e) else P⁰(e) = 0.

By definition, ˜Asatisfies the first requirement.

As to the second requirement. Let R be a relation between states from A and Ã such that for ((l₁, u₁),(l₂, u₂)) ∈ R iff l₂ = l₁, and for each x ∈ C, if u₁(x)≤maxÂ(x) thenu₂(x) =u₁(x), else u₂(x)>maxÂ(x). We show that for each state (l₁, u₁) ofA which is reached with cost c, there is a state (l₂, u₂) of A, such that ((l˜ ₁, u₁),(l₂, u₂))∈R and (l₂, u₂) is reached with costc, and vice versa.

Let (l₁, u₁), (l₂, u₂) be states of Aand ˜A, respectively, We use induction on the length of some execution leading to (l₁, u₁) or (l₂, u₂).

For the base step, the length of such an execution is 0. Trivially, the cost of such an execution is 0, and if (l₁, u₁) and (l₂, u₂) are initial states, clearly ((l₁, u₁),(l₂, u₂))∈R.

For the transition steps, we first observe that for each clockx∈C,u₁(x)∼c iffu₂(x)∼cwith∼∈ {<,≤, >,≥}andc≤maxA(x) (∗). Assume ((l₁, u₁),(l₂, u₂))

∈R, and (l₁, u₁) and (l₂, u₂) can both be reached with costc. We make the following case distinction.

Case 1: Suppose (l₁, u₁)−−−→⁽^d⁾^,pA (l₁, u₁+d). In order to let dtime pass in (l₂, u₂), we have to alternatingly perform the addedτ transition to reset those clocks that have reached themaxÂ(x) + 2 bound as many times as needed, and then let a bit of the time pass. Letd₁. . . dmbe a sequence of delays, such that d=d₁+. . .+dm, and forx∈Cand i∈ {1, . . . , m}, ifmaxÂ(x) + 2−(u₁(x) + d₁+. . .+di−1) ≥ 0 then di ≤maxÂ(x) + 2−(u₁(x) +d₁+. . .+di−1), else di≤1−frac(u₁(x) +d₁+. . .+di−1). It is easy to see that for someu⁰₂,

(l₂, u₂)(−−→)^τ,⁰ ^∗−−−−−→⁽^d¹⁾^,p¹ . . .(−−→)^τ,⁰ ^∗−−−−−−→⁽^d^m⁾^,p^m (l₂, u⁰₂)

where pi = di ∗P(l₂). The cost for reaching (l₁, u₁+d) is c+d∗PA(l₁) = c+d∗P_A_˜(l₂) =c+ (d₁+. . .+dm)∗P_A_˜(l₂), which is the cost for reaching (l₂, u⁰₂).

Now, ((l₁, u₁+d),(l₂, u⁰₂)) ∈ R, because of the following. For each x ∈ C, If u₁(x)>maxA(x), thenu₂(x)>maxA(x), and eitherxis not reset tomaxA(x)+1 by any of the τ transitions, in which case still u⁰₂(x) >maxÂ(x), or xis reset by some of the τ transitions, and thenmaxÂ(x) + 1≤u⁰₂(x)≤maxÂ(x) + 2, so u⁰₂(x)>maxÂ(x). Ifu₁(x)≤maxÂ(x), then byu₁(x) =u₂(x),u₂(x)≤maxÂ(x).

If (u₁+d)(x)≤max^A(x), thenxis not touched by any of theτtransitions leading

(17)

to (l₂, u⁰₂), hence u⁰₂(x) = u₂(x) +d₁+. . .+dm=u₂(x) +d= (u₁+d)(x). If (u₁+d)(x)>maxA(x), thenxmay be reset by some of theτ transitions leading to (l₂, u⁰₂). If so, thenmaxA(x) + 1≤u⁰₂(x)≤maxA(x) + 2, sou⁰₂(x)>maxA(x).

If not, thenu⁰₂(x) =u₂(x) +d₁+. . .+dm=u₂(x) +d= (u₁+d)(x)>max^A(x).

Case 2:Suppose (l₂, u₂)−−−→⁽^d⁾^,pA(l₂, u₂+d). Then trivially ((l₁, u₁+d),(l₂, u₂+ d))∈R. Now we show (l₁, u₁)−−−→⁽^d⁾^,pA(l₁, u₁+d). Since (l₂, u₂+d)∈I_A_˜, since I_A_˜ implies IA and since ((l₁, u₁+d),(l₂, u₂+d))∈R, from observation (∗) it follows that (l₁, u₁+d)∈IA. So (l₁, u₁)−−−→⁽^d⁾^,pA (l₁, u₁+d), and trivially, the cost of reaching (l₂, u₂+d) is c+d∗P_A_˜(l₂) =c+d∗PA(l₁), which is the cost of reaching (l₁, u₁+d).

Case 3: Suppose (l₁, u₁) −−→^a,p A (l₁⁰, u⁰₁). Let (l, g, a, r, l⁰) be a corresponding edge. Then p = PA((l, g, a, r, l⁰)). By definition, (l, g, a, r, l⁰) ∈ E_A_˜ and P_A_˜((l, g, a, r, l⁰)) =PA((l, g, a, r, l⁰)). From observation (∗) it follows thatu₁∈g impliesu₂∈g. It is easy to see that forx∈r,u⁰₁(x) = 0 =u₂[r7→0](x), and for x6∈r,u⁰₁(x) =u₁(x) andu₂(x) =u₂[r7→0](x), so ((l₁⁰, u⁰₁),(l⁰, u₂[r7→0]))∈R.

Combining this with observation (∗) it follows that u₁[r 7→0]∈ IA(l⁰) implies u₂[r7→0]∈I_A_˜(l⁰), hence (l₂, u₂)−−→^a,p _A_˜(l⁰, u₂[r7→0]). Clearly, the cost of reaching (l₁, u⁰₁) isc+d∗P_A_˜((l, g, a, r, l⁰)) =c+d∗PA((l, g, a, r, l⁰)), which is the cost of reaching (l₂, u₂[r7→0]).

Case 4:Suppose (l₂, u₂) −−→â,p A˜ (l⁰₂, u⁰₂). Let (l, g, a, r, l⁰) be a corresponding edge. If (l, g, a, r, l⁰)∈EA, then the argument goes exactly like in the previous case. If (l, g, a, r, l⁰)6∈EA, then a=τ, p= 0,l⁰₂=l⁰=l=l₂, and x∈rimplies u⁰₂(x) = maxA(x) + 1 and u₂(x) = maxA(x) + 2. Since the cost of reaching (l₂⁰, u⁰₂) is c+ 0 = c, it suffices to show ((l₁, u₁),(l₂, u⁰₂)) ∈ R. For x6∈ r, this follows trivially. For x∈r, u₂(x) =maxÂ(x) + 2, so u₁(x) >maxÂ(x) and by u⁰₂(x) =maxÂ(x) + 1 we haveu⁰₂(x)>maxÂ(x). 2 Now, we suggest in Fig. 7 a branch-and-bound algorithm for determining the minimum-cost of reaching a given target locationlg from the initial state of a LPTA. All encountered states are stored in the two data structuresPassedand Waiting, divided into explored and unexplored states, respectively. The global variable Cost stores the lowest cost for reaching the target location found so far. In each iteration, a state is taken fromWaiting. If it matches the target location lg and has a lower cost than the previously lowest cost Cost, then Costis updated. Then, only if the state has not been previously explored with a lower cost do we add it toPassed and add the successors toWaiting. This bounding of the search in line 8 of Fig. 7 may be optimized even further by adding the constraintmincost(R)<Cost; i.e. we only need to continue exploration if the minimum cost of the current region is below the optimal cost computed so far. Due to Theorem 1, the algorithm of Fig. 7 does indeed yield the correct minimum-cost value.

Theorem 3. When the algorithm in Fig. 7 terminates, the value ofCostequals mincost(lg).