We investigate an optimal cost reachability problem for weighted timed automata, and we use a translation to SMT to solve the problem. In particular, 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.
Reachability is a core decision problem that appears in several different contexts, for
example: concurrent systems [
The optimal reachability problem was considered by numerous researchers and
several methodologies treating the issue in the setting of timed automata have been
described 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.
SMTsolvers are tools for deciding the satisfiability of formulae in a number of theories [
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.
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 [
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
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 locations, 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. 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 [
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, J i, Jdi , zi, Vi), for i = 1, . . . , n, that run in parallel and communicate via synchronised s actions. A formal definition of a parallel composition of the weighted timed automata is the following.
V(l1, . . . , ln) = Sin=1 Vi(li).
Definition 2. Let Σ = Sin=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 the weighted timed automaton A = (Σ, L, l0, X , E, I, Js, Jd, z, V), where Σ = Sin=1 Σi, L = Qin=1 Li, l0 = (l10, . . . , ln0), X = Sin=1 Xi, a transition ((l1, . . . , ln), σ, Vj∈Σ(σ) ccj , Sj∈Σ(σ) Xj , (l1′, . . . , lm′)) ∈ E iff (∀j ∈ Σ(σ)) (lj , σ, ccj , Xj , lj′ ) ∈ Ej and (∀i ∈ {1, . . . , n} \ Σ(σ)) li′ = li, I(l1, . . . , ln) = Vin=1 Ii(li), Js(σ) = Pi∈Σ(σ) Jsi(σ), Jd(l1, . . . , ln) = Pin=1 Jdi (li), z = z1, and
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 automaton 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, 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: s0 δ1→,σ1 s1 δ2→,σ2 . . . δk−1→,σk−1 sk−1 δk→,σk 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 a k-run ρ of A and cost functions Js and Jd, we associate cost to ρ as follows:
Js(ρ) = Pik=1 Js(σi), and Jd(ρ) = Pik=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
[
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-quasioptimal 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. An informal explanation. To solve the k-optimal cost reachability problem we proceed 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 meanings 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 argument 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. 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 informal 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, symbolic switch costs si, and symbolic numbers ri, for 0 ≤ i ≤ k, and it constrains the 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,
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 [
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 • Jdi (j) = 1 for j ∈ {P rodSend, ConsStart, ConsReady} ∪ Snm=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
i=1 LNi × LC ) × (Qin=+12 IR) × IR), and we consider the following initial state s0 = ((P rodReady, N ode1Start, . . ., N odenStart, ConsStart), (0, . . . , 0), 0) . | n{+z2 }
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 description 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.
start
Node1Start start
NodenStart start
ConsStart
Sendn+1 Sendn+1 xn+1 ≥ c xn := 0 xn+1 := 0 Startn+1 xn+1 := 0
ConsReady xn+1 ≤ d
Consume xn+1 ≥ g xn+1 := 0 ConsFree xn+1 ≤ h start Produce x0 ≥ a
ProdReady x0 ≤ b Send1 x0 := 0 ProdSend
Send1 x1 ≥ c x1 := 0 Proc1 x1 ≥ e
Start1 x1 := 0
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 [
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. In this paper we defined, solved, and implemented the k-optimal cost reachability problem 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
No. of BMC Z3 BMC + Z3
Nodes k sec. MB sec. MB sec. MB
1 12 0.0 1.8 0.1 15.5 0.1 15.5
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 [
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 [
The paper [
The paper [
Furthermore, the paper [