=Paper=
{{Paper
|id=Vol-1492/Paper_44
|storemode=property
|title=SMT-based Searching for k-quasi-optimal Runs in Weighted Timed Automata
|pdfUrl=https://ceur-ws.org/Vol-1492/Paper_44.pdf
|volume=Vol-1492
|dblpUrl=https://dblp.org/rec/conf/csp/Wozna-Szczesniak15
}}
==SMT-based Searching for k-quasi-optimal Runs in Weighted Timed Automata==
https://ceur-ws.org/Vol-1492/Paper_44.pdf
SMT-based Searching for k-quasi-optimal Runs
in Weighted Timed Automata⋆
Extended Abstract
Bozena Wozna-Szczesniak, Agnieszka M. Zbrzezny, and Andrzej Zbrzezny
IMCS, Jan Dlugosz University Al. Armii Krajowej 13/15, 42-200 Czestochowa, Poland
{b.wozna,agnieszka.zbrzezny,a.zbrzezny}@ajd.czest.pl
Abstract. We investigate an optimal cost reachability problem for weighted
timed automata, and we use a translation to SMT to solve the problem. In par-
ticular, we show how to find a run of length k ∈ IN that starts at the initial state
and terminates at a state containing the target location, its total cost belongs to
the interval [c, c + 1), for some natural number c ∈ IN, and the cost of each other
run of length k, which also leads from the initial state to a state containing the
target location, is greater or equal to c. This kind of runs we call k-quasi-optimal.
We exemplify the use of our solution to the mentioned problem by means of
the weighted timed generic pipeline protocol, and we provide some preliminary
experimental results.
1 Introduction
Reachability is a core decision problem that appears in several different contexts, for ex-
ample: concurrent systems [8, 17], time critical systems [12], and probabilistic systems
[10]. For computational models of time critical systems like weighted timed automata
[2] (see Section 2 for the formal definition), or priced timed automata [5], it is reason-
able to make inquiries about the minimum (optimal) cost of reaching a desirable state
of the system, i.e., to investigated the optimal reachability problem.
The optimal reachability problem was considered by numerous researchers and sev-
eral methodologies treating the issue in the setting of timed automata have been de-
scribed in the literature, but none of them used SMT- or SAT-based methods (see the
Related Work section). The acronym SMT means satisfiability modulo theories. SMT-
solvers are tools for deciding the satisfiability of formulae in a number of theories [4].
Nevertheless, in the paper [19] we made the first attempt to solve, so called, the k-
optimal cost reachability problem for weighted timed automata (see Section 3 for the
formal definition). The proposed solution used the translation to SAT, and it could only
be applied to systems modelled by a single weighted timed automaton.
In this paper we also deal with the k-optimal cost reachability problem, but for
time critical systems modelled by a network of weighted timed automata. Moreover,
we are interested in using SMT-based verification methods to solve the problem instead
of the SAT-based verification. The use of a translation to SMT allows us to avoid an
intermediate discretised model.
⋆
Partly supported by National Science Centre under the grant No. 2014/15/N/ST6/05079.
197
The solution which we propose for the k-optimal cost reachability problem is the
combination of a well-known forward reachability algorithm with the bounded model
checking (BMC) method [18, 19] that uses SMT solvers instead of SAT solvers (see
Section 3 for the informal and formal description of the solution). The forward reacha-
bility algorithm searches the state space using the breadth first mode, whereas the BMC
performs a verification on a part of the automata model exploiting SMT solvers.
How our solution to the k-optimal cost reachability problem is effective we show
by means of the weighted timed generic pipeline protocol (see Section 4).
2 Preliminaries
Let us start by introducing the key sets of numbers and variables used in the rest of the
paper. The first is the set IN = {0, 1, 2, 3, . . .} of natural numbers. The second is the set
IR of non-negative real numbers, and the third is the set IR+ of positive real numbers.
The next is the set PV of propositional variables, and the final is a finite set X of real
variables, called clocks.
For the set X of clocks, x, y ∈ X , c ∈ IN and ∼ ∈ {≤, <, =, >, ≥}, the set C(X )
of all the clock constraints over X is defined by the following grammar:
cc ::= true | x ∼ c | x − y ∼ c | cc ∧ cc
Furthermore, a clock valuation is a total mapping cv : X → IR, and satisfiability of a
clock constraint cc ∈ C(X ) by a clock valuation cv (cv |= cc) is defined inductively
as follows:
• cv |= true,
• cv |= (x ∼ c) iff cv(x) |= c,
• cv |= (x − y ∼ c) iff cv(x) − cv(y) ∼ c,
• cv |= cc1 ∧ cc2 iff cv |= cc1 and cv |= cc2 .
Given a clock valuation cv and δ ∈ IR+ , by cv + δ we denote a clock valuation cv′
such that cv′ (x) = cv(x) + δ, for all x ∈ X . Moreover, for a subset of clocks X ⊆ X ,
cv[X := 0] denotes the valuation cv′ such that for all x ∈ X, cv′ (x) = 0 and for all
x ∈ X \ X, cv′ (x) = cv(x). Finally, by cv0 we denote the initial clock valuation, i.e.,
the valuation such that cv0 (x) = 0 for all x ∈ X .
Definition 1. A weighted timed automaton is a tuple A =
(Σ, L, l0, X , E, I, Js ,Jd , z, V), where Σ is a finite set of actions, L is a finite set of loca-
tions, l0 ∈ L is an initial location, X is a finite set of clocks, E ⊆ L×Σ×C(X )×2X ×L
is a transition relation, I : L 7→ C(X ) is an invariant function, Js : Σ 7→ IN is a
switch cost function, Jd : L → IN is a duration cost function, z is a real variable, and
V : L 7→ 2PV is a valuation function assigning to each location a set of propositional
variables true in that location.
The switch cost function assigns to each action a cost expressing the price of taking the
action. The duration cost function assigns to each location a cost expressing the price of
staying in this location for one time unit. The invariant function assigns to each location
a clock constraint expressing the condition under which A can stay in this location.
198
Each element t = (l, σ, cc, X, l′ ) ∈ E represents a transition from the location l to the
location l′ , where σ is the action of the transition t, cc defines the enabling conditions
for t, and X is a set of clocks to be reset.
Note that the syntax of weighted timed automata is borrowed from [2, 19], but it
is extended to a special real variable z. Moreover, we have changed the domain of the
switch cost function. Namely, we assume that the domain of the switch cost function is
the set of actions instead of the set of transitions. Such a change is necessary, since we
considered systems that are modelled through a network of weighted timed automata
instead of a single weighted timed automaton.
In general, weighted timed automata are often composed into a network of weighted
timed automata consisting of n weighted timed automata Ai = (Σi , Li , li0 , Xi , Ei , Ii ,
Jsi , Jdi , zi , Vi ), for i = 1, . . . , n, that run in parallel and communicate via synchronised
actions. A formal definition of a parallel composition of the weighted timed automata
is the following.
Sn
Definition 2. Let Σ = i=1 Σi , σ ∈ Σ, and Σ(σ) = {1 ≤ i ≤ n | σ ∈ Σi } be the set
of indexes of automata that synchronise at σ, and z1 = . . . = zn (i.e., all the automata
have to share the variable). For i = 1, . . . , n, a parallel composition of weighted timed
automata Ai is Snthe weighted timed Qn automaton A = (Σ, L, l0 , X , S E, I, Js , Jd , z, V),
0 0 0 n
where Σ = i=1 ΣV i, L = i=1
S Li , l = (l 1 , . . . , ln ), X = i=1 Xi , a transi-
tion ((l1 , . . . , ln ), σ, j∈Σ(σ) ccj , j∈Σ(σ) Xj , (l1′ , . . . , lm ′
)) ∈ E iff (∀j ∈ Σ(σ))
(l , σ, ccj , Xj , lj′ ) ∈ Ej and (∀i ∈ {1, . . . , n} \ Σ(σ)) li′ = li , I(l1 , . . . , ln ) =
Vjn P Pn
i=1 Ii (li ), Js (σ) = i∈Σ(σ) Jsi (σ), Jd (l1 , . . . , ln ) = i
i=1 Jd (li ), z = z1 , and
Sn
V(l1 , . . . , ln ) = i=1 Vi (li ).
The semantics of weighted timed automata is defined by associating to them dense
models as defined below.
Definition 3. Let A = (Σ, L, l0 , X , E, I, Js , Jd , z, V) be a weighted timed automaton,
z : {z} → IR a valuation for z, and z0 the initial valuation for z (i.e., z0 (z) = 0).
A dense model for A is the tuple M = (Σ ∪ IR+ , S, s0 , →, V ′ ), where Σ ∪ IR+ is a
set of labels, S = {(l, cv, z) | l ∈ L, cv ∈ IR|X | , cv |= I(l), z ∈ IR} is a set of
states, s0 = (l0 , cv0 , z0 ) is the initial state, V ′ : S → 2PV is a valuation function such
that V ′ ((l, cv, z)) = V(l), and →⊆ S × Σ ∪ IR × S is the smallest transition relation
defined by the following two rules:
σ
• action transition: for σ ∈ Σ, (l, cv, z) → (l′ , cv′ , z′ ) iff there exists a transition
t = (l, σ, cc, X, l′ ) ∈ E such that cv |= cc, cv |= I(l), cv[X := 0] |= I(l′ ), and
z′ = z + Js (σ),
δ
• time transition: for δ ∈ IR+ , (l, cv, z) → (l, cv + δ, z′ ) iff cv |= I(l), cv + δ |=
I(l), and z′ = z + Jd (l) · δ.
Intuitively, an action transition corresponds to an action performed by the automa-
ton under consideration. The action can be performed only if the underlying enabling
condition is satisfied. Moreover, all the clocks that are associated with the action are set
to zero, its locations change accordingly, and the value of the variable z is increased by
the switch cost. A time transition causes an equal increase in the value of all the clocks,
199
and does not involve a location change. Obviously, the new clock valuations have to
still satisfy all the location invariants, and the value of the variable z is increased by the
duration cost.
δ,σ
Let us denote by s → s′ the sequence of the following time and action transitions:
δ σ
s → s′′ and s′′ → s′ , where σ ∈ Σ, δ ∈ IR+ , and s, s′ , s′′ ∈ S.
Definition 4. Let k ∈ IN, i ∈ {0, . . . , k}, si ∈ S, j ∈ {1, . . . , k}, σj ∈ Σ, and
δj ∈ IR+ . A k-run ρ of a weighted timed automaton A is a finite sequence of transition:
δ1 ,σ1 δ2 ,σ2 δk−1 ,σk−1 δk ,σk
s0 → s1 → . . . → sk−1 → sk .
In other words, a k-run is a finite path of A, where action transitions are taken finitely
often and time transitions are aggregated. Moreover, the k-run does not permit two
consecutive actions to be performed one after the other; such a run is called strongly
monotonic.
Given Pa k-run ρ of A and cost functions
Pk Js and Jd , we associate cost to ρ as follows:
k
Js (ρ) = i=1 Js (σi ), and Jd (ρ) = i=1 δi · Jd (li−1 ). Furthermore, the total cost
associated to a k-run ρ is defined as J(ρ) = Jd (ρ) + Js (ρ). Finally, we recall the
definitions of both the k-optimal cost and k-quasi-optimal that have been introduced in
[19].
Definition 5. The k-optimal cost for k-runs that start at a state containing location l
and end at a state containing location l′ is defined as: Jk∗ (l, l′ ) = inf {J(ρ) | ρ is a k −
run from a state containing location l to a state containing location l′ }.
If ⌊J(ρ)⌋ = ⌊Jk∗ (l, l′ )⌋, then a k-run ρ from a state containing location l to a state
containing location l′ is k-quasi-optimal.
In this paper, for given two locations l and l′ we are interested in finding the greatest
integer lower bound (g.i.l.b. for short) of the k-optimal cost for k-runs starting at a state
s containing location l and terminating at a state t containing location l′ , where k is
the length of a shortest run from s to t. Moreover, we are interested in finding k-quasi-
optimal runs. Therefore, in Section 3 we define k-optimal cost reachability problem,
and we show how to solve it using SMT-methods.
3 k-Optimal Cost Reachability Problem
In this section we formally define the k-optimal cost reachability problem for weighted
timed automata, and we present a solution to the problem which uses SMT-solvers. We
begin with defining the problem, and then we describe our solution informally, which
will help to understand the formal algorithm presented later on in this section.
Definition 6 (k-optimal cost reachability). Given a weighted timed automaton A =
(Σ, L, l0 , X , E, I, Js , Jd , z, V), and a desirable location lp ∈ L satisfying a property p.
k-optimal cost reachability problem consists in finding out a k-quasi-optimal run ρ
starting at s0 ∈ M and terminating at a state in M containing location lp .
Note that if ρ is a k-quasi-optimal run, then there exists c ∈ IN such that: c ≤ J(ρ) <
c + 1, and for all the k-runs ρ′ that starts at s0 and terminates at a state in M containing
location lp , J(ρ′ ) ≥ c holds.
200
An informal explanation. To solve the k-optimal cost reachability problem we pro-
ceed as follows. We first encode by quantifier-free first-order formulae with individual
variables ranging over the real numbers both the property p, and the unfolding of the
transition relation of M up to depth k (for k ∈ IN). Let ϕk be the conjunction of the
two above formulae. We test ϕk for satisfiability using an SMT-solver. If the test for
ϕk is positive, we calculate the cost r0 ∈ IR of the resulting witness ρ0 , and we know
that J(ρ0 ) < ⌈r0 ⌉. Next, we set c0 = ⌈r0 ⌉ − 1, and we run the satisfiability test once
again, but for the formula φk (c0 ) = ϕk ∧ (z < c0 ). If the test for φk (c0 ) is positive, we
calculate the cost r1 ∈ IR of the resulting witness ρ1 , and we know that r1 < c0 . Next,
we set c1 = ⌈r1 ⌉ − 1, and we run the satisfiability test once again, but for the formula
φk (c1 ) = ϕk ∧ (z < c1 ), and so on. We stop testing, if the test for φk (ci ) is negative or
ri = 0.
Notice that, if the test for φk (ci ) is negative, we can perform one more test for the
formula ψk (ci ) = ϕk ∧ (z = ci ). If the test for ψk (ci ) is positive, we can conclude that
k-optimal cost is equal to ci . Otherwise, we can only conclude that the g.i.l.b. of the
k-optimal cost is equal to ci .
A formal algorithm for finding the g.i.l.b. of k-optimal cost. Algorithm 5 uses the
procedure checkSM T (γ) that for any given quantifier-free first-order formula γ returns
a pair (W, X), where W denotes the valuation returned by a SMT solver, and X can be
one of the following three values: T RU E, F ALSE, and U N KN OW N . The mean-
ings of the values T RU E and F ALSE are self-evident. The value U N KN OW N is
returned either if the procedure checkSM T is not able to decide satisfiability of its ar-
gument within some preset timeout period, or has to terminate itself due to exhaustion
of available memory. Algorithm 5 also uses the procedure getCOST (W ) that for the
valuation W , which represents a k-run ρ, returns a natural number c such that the cost
of ρ is less than c. Finally, for a given quantifier-free first-order formula ϕk , the symbol
φk (c) denotes the formula ϕk ∧ (z < c), and the symbol ψk (c) denotes the formula
ϕk ∧ (z = c).
Translation to quantifier-free first-order formulae. Let A = (Σ, L, l0 , X , E, I, Js ,
Jd , z, V) be a weighted timed automaton that is a parallel composition of n weighted
timed automata Ai , M = (Σ ∪ IR, S, s0 , →, V ′ ) a dense model for A, and k ∈ IN.
Each state s ∈ S of M can be represented by a valuation of a symbolic state w =
((l1 , . . . , ln ), (x1 , . . . , x|X | ), (d1 , . . . , dn ), z) that consists of symbolic local states,
symbolic clock valuations, symbolic duration costs, and symbolic valuation of variable
z. Each symbolic local state li (1 ≤ i ≤ n) is an individual variable ranging over the
natural numbers. Each symbolic clock valuations xi (1 ≤ i ≤ |X |) is an individual
variable ranging over the real numbers. Each symbolic duration cost di (1 ≤ i ≤ n)
is an individual variable ranging over the natural numbers, and symbolic valuation of
variable z is an individual variable ranging over the real numbers. Similarly, each action
σ ∈ Σ can be represented by a valuation of a symbolic action a that is an individual
variable ranging over the natural numbers, each real number r ∈ IR can be represented
by a valuation of a symbolic number r that is an individual variable ranging over the real
numbers, and finally each switch cost s can be represented by a valuation of a symbolic
switch cost s that is an individual variable ranging over the natural numbers.
A finite sequence (w0 , . . . , wk ) of symbolic states is called a symbolic k-path.
201
Algorithm 5: An algorithm for finding g.i.l.b. of k-optimal cost
1: k ← 0
2: repeat
3: (W, result) ← checkSM T (ϕk )
4: if result = F ALSE then
5: k ←k+2
6: else if result = U N KN OW N then
7: return U N KN OW N
8: end if
9: until result = T RU E
{there exists a witness of the length k for a desirable property}
10: c ← getCOST (W )
11: repeat
12: if c = 0 then
13: return k-optimal cost is equal to 0
14: end if
15: (W, result) ← checkSM T (φk (c − 1))
16: if result = T RU E then
17: c ← getCOST (W )
18: else if result = U N KN OW N then
19: return U N KN OW N
20: end if
21: until result = F ALSE
{optimal cost of any k-run is greater or equal to c}
22: (W, result) ← checkSM T (ψk (c))
23: if result = T RU E then
24: return k-optimal cost is equal to c
25: else
26: return g.i.l.b. of k-optimal cost is equal to c
27: end if
For two symbolic states w, w′ , we define the following propositional formulae:
• Is (w) is a formula that encodes the state s of M
• p(w) is a formula that encodes the set of states of M in which p ∈ PV holds.
• Ta (w, (a, s), w′ ) is a formula that encodes the action transition relation of M .
• Tr (w, r, w′ ) is a formula that encodes the time transition relation of M .
We can now define the quantifier-free first-order formula ϕk , introduced in the in-
formal description section. The formula ϕk is a conjunction of two formulae. The first
formula p(w) is a translation of a propositional variable p that represents a location in
0
question. The second formula [M s ]k encodes the unfolding of the transition relation
of M up to depth k ∈ IN.
0
The formula [M s ]k is defined over symbolic states wi , symbolic actions ai , sym-
bolic switch costs si , and symbolic numbers ri , for 0 ≤ i ≤ k, and it constrains the
202
symbolic k-path to be valid k-run of M . Namely, let T (wi , wi+1 )=Tr (wi , ri , wi+1 ) if
i is even, and T (wi , wi+1 )=Ta (wi , (ai , si ), wi+1 ) if i is odd. Then,
k−1
^
0
[M s ]k := Is0 (w0 ) ∧ T (wi , wi+1 )
i=0
4 Experimental Results
In this section we experimentally evaluate the performance of our SMT-based solution
to the k-optimal cost reachability problem by means of the weighted timed generic
pipeline protocol (WTGPP).
WTGPP. The WTGPP (adapted from [16]) consists of n + 2 automata: Producer P that
is able to produce data within certain time interval [a, b] or being inactive , Consumer
C that is able to receive data within certain time interval [c, d], to consume data within
certain time interval [g, h] or being inactive, and a chain of n intermediate Nodes Ni
which can be ready for receiving data within certain time interval [c, d], processing data
within certain time interval [e, f ], sending data, or being inactive. The local locations,
the possible local actions, the local clocks, the clock constraints, invariants and the local
transitions for each automaton are shown in Fig. 1. Moreover, we assume the following
two switch cost functions for each automaton:
• JsP (P roduce) = 4, JsP (send1 ) = 2, JsC (Consume) = 4, JsC (sendn+1 ) = 2,
JsNi (sendi ) = JsNi (sendi+1 ) = JsNi (P roci ) = 2.
• JsP (P roduce) = 4000000, JsP (send1 ) = 2000000, JsC (Consume) = 4000000,
JsC (sendn+1 ) = 2000000, JsNi (sendi ) = JsNi (sendi+1 ) = JsNi (P roci ) =
2000000.
Finally, we assume the following duration cost function for each automaton:
• JdP (P rodReady) = 4, JdC (ConsF ree) = 4, and Sn
• Jdi (j) = 1 for j ∈ {P rodSend, ConsStart, ConsReady} ∪ m=1 LNm , and
i ∈ {P, C, N1 , . . . , Nn }.
We can define the set of global states S for the protocol as the product ((LP ×
Qn Qn+2 0
i=1 LNi × LC ) × ( i=1 IR) × IR), and we consider the following initial state s =
((P rodReady, N ode1 Start, . . ., N oden Start, ConsStart), (0, . . . , 0), 0) .
| {z }
n+2
The example can be scaled by adding Nodes, or by changing the length of intervals
(i.e., the parameters a, b, c, d, e, f , g, h) that are used to adjust the time properties of
Producer P , Consumer C, and Nodes Ni (i = 1, .., n), or by changing the switch cost
functions or by changing the duration cost functions.
It should be straightforward to infer the model that is induced by the above descrip-
tion of WTGPP. Next, in the dense model of the protocol we assume the following set
of proposition variables: PV = {ConsF ree}, and the following definition of valuation
functions for Consumer: VC (ConsF ree) = ConsF ree.
The k-optimal reachability property we consider is the following. Given a weighted
timed automata model of the WTGPP system, decide whether there is a k-optimal run
of the weighted timed automaton from the initial state of the system to the given global
state of the system that contains the Consumer location ConsF ree.
203
start Node1 Start start Noden Start start ConsStart
Start1 Startn
x1 := 0 xn := 0 Startn+1
xn+1 := 0
Node1 Ready Noden Ready
···
x1 ≤ d xn ≤ d
ProdReady ConsReady
start Send1 Sendn
x0 ≤ b xn+1 ≤ d
x1 ≥ c xn ≥ c
x1 := 0 xn := 0
Sendn+1 Consume
Produce Send1 Node1 Proc Send2 Noden Proc Sendn+1 x
n+1 ≥ c xn+1 ≥ g
x0 ≥ a x0 := 0 x1 ≤ f x1 := 0 xn ≤ f xn := 0 x
n+1 := 0 xn+1 := 0
Proc1 Procn
ProdSend x1 ≥ e xn ≥ e ConsFree
xn+1 ≤ h
Node1 Send Noden Send
Fig. 1. A WTGPP protocol.
Performance evaluation. We have computed our experimental results on a computer
equipped with I7-3770 processor, 32 GB of RAM, and the operating system Arch Linux
with the kernel 3.15.3. Moreover, we used the state of the art SMT-solver Z3 [14].
In Tables 1 and 2 we present experimental results for the WTGPP system modelled
by the network of automata on Figure 1 and for k−optimal reachability property. As can
be seen from these tables, our method allows us to locate k-optimal path for 5 Nodes
within a reasonable time. This result does not change if we drastically increase the
values of the considered switch cost function, which may suggest that the effectiveness
of our method does not depend on values of the switch cost function. In addition, a
noticeable enormous increase in time for 5 Nodes suggests that a significant impact
on the effectiveness of our method has a number of arithmetic operations performed,
especially multiplication.
No. of BMC Z3 BMC + Z3 Table 1. Time and memory used for k-
Nodes k sec. MB sec. MB sec. MB optimal path and a number of Nodes n.
1 12 0.0 1.8 0.2 15.5 0.2 15.5 Assumed the first switch cost function.
2 18 0.0 1.8 0.7 17.2 0.7 17.2
3 26 0.0 1.9 7.3 22.3 7.3 22.3
4 34 0.2 2.1 211.6 33.6 211.8 33.6
5 44 0.3 2.1 7594.7 59.1 7595.0 59.1
5 Conclusions and Related Work
In this paper we defined, solved, and implemented the k-optimal cost reachability prob-
lem for a network of weighted timed automata. The proposed solution is based on the
reduction to the satisfiability problem of the quantifier-free first-order formulae, and it
204
Table 2. Time and memory used No. of BMC Z3 BMC + Z3
for k-optimal path and a number Nodes k sec. MB sec. MB sec. MB
of Nodes n. Assumed the second 1 12 0.0 1.8 0.1 15.5 0.1 15.5
switch cost function. 2 18 0.0 1.8 0.5 17.2 0.5 17.2
3 26 0.0 1.9 6.4 22.6 6.4 22.6
4 34 0.1 2.1 270.5 33.8 270.7 33.8
5 44 0.3 2.1 17715.3 71.6 17715.6 71.6
uses an external tool that is the state of the art SMT-solver Z3 [14]. Experimental re-
sults, which we carried out, show that the proposed algorithm can be extremely helpful
in finding g.i.l.b. of k-optimal cost.
Clearly, our method takes into account discovering just lower and upper bounds on
the cost to which the k-quasi-optimal run belongs (an unit interval [c, c+1), for c ∈ IN),
but in many real-time settings such a cost optimal approximation is sufficient.
Related Work. The issue of processing lower and upper bounds on time delays in
timed automata was addressed in [9]. A duration-bounded reachability issue for timed
automata expanded to incorporate the duration cost function is considered in [1]. This
issue inquires as to whether there is a run of the timed automaton from the initial state to
the given last state such that the duration of the run fulfils an arithmetic requirement (an
optimal cost). The duration-bounded reachability issue has been also analysed in [11].
This is because the problem can be reduced to checking whether a duration formula,
which defines an optimal cost, is fulfilled by a integer computation of an integration
graph (a sort of a timed automaton). The solution is based on constructing a set of
equations that characterises the length of time a computation spends in each location of
the given automaton.
The paper [3] also handles the optimal (minimum-time) reachability problem for
timed automata. Specifically, here, the issue is formulated in terms of a timed game
automaton (TGA), and solved by constructing an optimal strategy utilizing a backward
fixed-point calculation on the state-space of the TGA. The minimum-time reachability
problem for timed automata is likewise illuminated in [15]. However here, the solu-
tion is based on the forward fixed-point algorithm that generates on-the-fly a forward
reachability graph for a given timed automaton.
The paper [5] defines priced timed automata as an extension of timed automata
with costs on both transitions and locations, and demonstrates how to solve the min-
imum cost reachability problem; this kind of automata we used in our paper. In [2]
such reachability problem is called as the single-source optimal reachability problem,
and it is solved by a reduction of the problem to a parametric shortest-path problem.
The methods exhibited in both papers [5] and [2] are taking into account clock region
graphs; in [2] the authors refer to priced timed automata as weighted timed automata.
Furthermore, the paper [6] solves the optimal reachability problem for weighted
timed automata with cost functions allowing for both positive and negative costs on
edges and locations, and apply the proposed method to timed games. Next, the paper
[13] deals with the decidability of the optimal (minimum and maximum cost) reacha-
bility problems for multi-priced timed automata (an extension of timed automata with
205
multiple cost variables evolving according to given rates for each location). Finally, the
paper [7] handles cost-optimal infinite schedules in terms of minimal (or maximal) cost
per time ratio in the limit.
References
1. R. Alur, C. Courcoubetis, and T. Henzinger. Computing accumulated delays in real-time
systems. Formal Methods in System Design, 11(2):137–155, 1997.
2. R. Alur, S. La Torre, and G. J. Pappas. Optimal paths in weighted timed automata. Theoret-
ical Computer Science, 318(3):297–322, June 8 2004.
3. E. Asarin and O. Maler. As soon as possible: Time optimal control for timed automata.
In Proceedings of the 2nd International Workshop on Hybrid Systems: Computation and
Control, volume 1569 of LNCS, pages 19–30. Springer-Verlag, 1999.
4. Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. Satisfiability modulo
theories. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and
Applications, chapter 26, pages 825–885. IOS Press, 2009.
5. G. Behrmann, A. Fehnker, T.S. Hune, K. G. Larsen, P. Pettersson, J. M. T. Romijn, F.W.
Vaandrager, F. W. Va, Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Larsen, Paul
Pettersson, and Judi Romijn. Minimum-cost reachability for priced timed automata. In
Proceedings of HSCC’01, volume 2034 of LNCS, pages 147–161. Springer-Verlag, 2001.
6. P. Bouyer, T. Brihaye, V. Bruyère, and J. Raskin. On the optimal reachability problem of
weighted timed automata. Formal Methods in System Design, 31(2):135–175, 2007.
7. P. Bouyer, E. Brinksma, and K. G. Larsen. Optimal infinite scheduling for multi-priced timed
automata. Formal Methods in System Design, 32(1):3–23, 2008.
8. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
9. C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time
systems. Formal Methods in System Design, 1(4):385–415, 1992.
10. P.R. D’Argenio, B. Jeannet, H. E. Jensen, and K.G. Larsen. Reachability analysis of proba-
bilistic systems by successive refinements. In Proceedings of the Joint International Work-
shop on Process Algebra and Probabilistic Methods, Performance Modeling and Verifica-
tion, volume 2165 of LNCS, pages 39–56. Springer-Verlag, 2001.
11. Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Decidable integration graphs. Information
and Computation, 150(2):209–243, 1999.
12. R. Koymans. Specifying Message Passing and Time-Critical Systems with Temporal Logic,
volume 651 of LNCS, chapter Time-critical systems, pages 99–142. Springer Berlin Heidel-
berg, 1992.
13. K. G. Larsen and J. I. Rasmussen. Optimal reachability for multi-priced timed automata.
Theoretical Computer Science, 390(2-3):197–213, 2008.
14. L. De Moura and N. Bjørner. Z3: an efficient SMT solver. In Proceedings of 14th Inter-
national Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS’2008), volume 4963 of LNCS, pages 337–340. Springer-Verlag, 2008.
15. P. Niebert, S. Tripakis, and S. Yovine. Minimum-time reachability for Timed Automata.
In Proceedings of the 8th IEEE Mediterranean Conference on Control and Automation
(MED’2000), Patros, Greece, July 2000. IEEE Computer Society.
16. D. Peled. All from one, one for all: On model checking using representatives. In Proceedings
of the 5th International Conference on Computer Aided Verification (CAV’93), volume 697
of LNCS, pages 409–423. Springer-Verlag, 1993.
17. A.W. Roscoe. Understanding Concurrent Systems. Springer-Verlag, 2010.
206
18. B. Woźna, A. Zbrzezny, and W. Penczek. Checking reachability properties for Timed Au-
tomata via SAT. Fundamenta Informaticae, 55(2):223–241, 2003.
19. B. Woźna-Szcześniak and A. Zbrzezny. SAT-based searching for k-quasi-optimal runs in
weighted timed automata. Scientific Issues of Jan Długosz University in Czȩstochowa: Math-
ematica, XV:149–162, 2010.