We present a new translation of Metric Temporal Logic to the Linear Temporal Logic with a new set of the atomic propositions. We investigate a SAT-based bounded model checking method for Metric Temporal Logic that is interpreted over linear discrete infinite time models generated by discrete timed automata. We show how to implement the bounded model checking technique for Linear Temporal Logic with a new set of the atomic propositions and discrete timed automata, and as a case study we apply the technique in the analysis of the Timed Generic Pipeline Paradigm modelled by a network of discrete timed automata. We also present a comparison of the two translations of Metric Temporal Logic on common instances that can be scaled up to for performance evaluation. The theoretical description is supported by the experimental results that demonstrate the efficiency of the method.
Bounded model checking [
The novelty of our paper lies in : 1. defining a translation of the existential model checking problem for MTL to the existential model checking problem for linear temporal logic with additional propositional variables qI . This logic is denoted by LTLq ; 2. defining bounded sematics for LTLq and defining the BMC algorithm; 3. implementing the new method.
The translation from MTL to LTLq requires neither new clocks nor new transitions,
whereas the translation to HLTL [
Finally, we evaluate the BMC method experimentally by means of a timed generic
pipeline paradigm (TGPP), which we model by a network of discrete timed automata
and compare with the corresponding method [
The rest of the paper is structured as follows. In Section 2 we briefly recall the basic notion used through the paper. In Section 3 we define the translation to LTLq. In Section 4 we define the BMC method for LTLq. In Section 5 we discuss our experimental results. In Section 6 we conclude the paper. 2 2.1
Let IN be a set of natural numbers. We assume a finite set X = fx0; : : : ; xn 1g of variables, called clocks. Each clock is a variable ranging over a set of non-negative natural numbers.
A clock valuation is a total function v : X 7! IN that assigns to each clock x a non-negative integer value v(x). The set of all the clock valuations is denoted by INn. For X X, the valuation v0 = v[X := 0] is defined as: 8x 2 X, v0(x) = 0 and 8x 2 X n X, v0(x) = v(x). For 2 IN, v + denotes the valuation v00 such that 8x 2 X; v00(x) = v(x) + . Let x 2 X, c 2 IN, and 2 f<; 6; =; >; >g. The set C(X) of clock constraints over the set of clocks X is defined by the following grammar: cc := x
c j cc ^ cc.
Let v be a clock valuation, and cc 2 C(X). A clock valuation v satisfies a clock constraint cc, written as v j= cc, iff cc evaluates to true using the clock values given by the valuation v.
Definition 1. A discrete timed automaton A is a tuple (Act; Loc; `0; T; X; Inv; AP ; V ), where Act is a finite set of actions, Loc is a finite set of locations, `0 2 Loc is an initial location, T Loc Act C(X) 2X Loc is a transition relation, X is a finite set of clocks, Inv : Loc 7! C(X) is a state invariant function, AP is a set of atomic proposition, and V : Loc 7! 2AP is a valuation function assigning to each location a set of atomic propositions true in this location.
Each element t 2 T is denoted by ` ;c!c;X `0, and it represents a transition from location ` to location `0 on the input action . X X is the set of the clocks to be reset with this transition, and cc 2 C(X) is the enabling condition for t.
The semantics of the discrete timed automaton is defined by associating a transition system with it, which we call a concrete model.
Definition 2. Let A = (Act; Loc; `0; T; X; Inv; AP ; V ) be a discrete timed automaton, and v0 a clock valuation such that 8x 2 X, v0(x) = 0. A concrete model for A is a tuple MA = (Q; q0; !; V), where Q = Loc INn is a set of the concrete states, q0 = (`0; v0) is the initial state, ! Q Q is a total binary relation on Q defined by action and time transitions as follows. For 2 Act and 2 IN, 1. Action transition: (`; v) ! (`0; v0) iff there is a transition `
that v j= cc ^ Inv(`) and v0 = v[X := 0] and v0 j= Inv(`0), 2. Time transition: (`; v) ! (`; v + ) iff v j= Inv(`) and v + j= Inv(`). ;cc;X `0 2 T such ! V : Q 7! 2AP is a valuation function such that V((`; v)) = V (`) for all (`; v) 2 Q. A run of A is an infinite sequence of concrete states: q0 0!;0 q1 1!;1 q2 2!;2 : : : such that qi 2 Q, i 2 Act, and i 2 IN+ for each i 2 IN. Notice that our runs are strongly monotonic. This is because the definition of the run does not permit two consecutive actions to be performed one after the other, i.e., between each two actions some time must pass. 2.2
Let p 2 AP , and I be an interval in IN of the form: [a; b) or [a; 1), for a; b 2 IN and a 6= b. The MTL in release positive normal form is defined by the following grammar: := true j false j p j :p j ^ j _ j
UI j GI .
Intuitively, UI and GI are the operators for bounded until and for bounded always. The formula UI is true in a computation if is true in the interval I at least in one state and always earlier holds. The formula GI is true in a computation is true at all states of the computation that are in the interval I. The derived basic modality is defined as follows: FI d=ef trueUI (bounded eventually).
Let A be a discrete timed automaton, MA = (Q; q0; !; V) a concrete model for
A, : q0 0!;0 q1 1!;1 q2 2!;2 : : : a run of A, and , formulae of MTL. In order
to define the satisfiability relation for MTL, we need to define the notion of a discrete
path corresponding to run [
In order to improve readability, in the following definition we write t j=MTL' instead of M'; t j=MTL', for any MTL formula '.
Definition 3. The satisfiability relation j=MTL, which indicates truth of an MTL formula in the concrete model MA along a path at time t 2 IN, is defined inductively as follows: – – t j=MTL true, t 6 j=MTL false, t j=MTL p iff p 2 V( (t)), t j=MTL :p iff p 62 V( (t)), t j=MTL t j=MTL t j=MTL iff t j=MTL iff t j=MTL ^ _ UI iff (9t0 2 I)( t+t0 j=MTL and t j=MTL , or t j=MTL , t j=MTL GI iff (8t0 2 I)( t+t0 j=MTL ). and (80 6 t00 < t0) t+t00 j=MTL ), As 0 = , we shall write MA; j=MTL ' for MA; 0 j=MTL '. An MTL formula ' is existentially valid in the model MA, denoted MA j=MTL E', if, and only if MA; j=MTL ' for some path starting in the initial state of MA. Determining whether an MTL formula ' is existentially valid in a given model is called an existential model checking problem.
– – – – 3 3.1
Let ' be an MTL formula and A = (Act; Loc; `0; T; X; Inv; AP ; V ) be a discrete timed automaton with X = fx0; : : : ; xn 1g. For each j 2 f0; : : : ; n 1g, let cjmax be the largest constant appearing in intervals of ' and in any enabling condition involving the clock xj and used in the state invariants and guards of A. For two clock valuations v and v0 in INn, we say that v ' v0 iff for each 0 6 j < n either v(xj ) > cjmax and v0(xj ) > cjmax or v(x) 6 cjmax and v0(x) 6 cjmax and v(x) = v0(x).
It is well known, that the relation ' is an equivalence relation, what gives rise to construct an finite abstract model. To this end we define the set of possible values of the clock xj in the abstract model as IDj = f0; : : : ; cjmax +1g for 0 6 j < n. Moreover, for two clock valuations v and v0 in ID0 : : : IDn 1, we say that v0 is the time successor of v (denoted succ(v)) as follows: for each 0 6 j < n, succ(v)(xj ) = v(xj ) + 1; if v(xj ) 6 cjmax; cjmax + 1; if v(xj ) = cjmax + 1: Definition 4. Let A = (Act; Loc; `0; T; X; Inv; AP ; V ) be a discrete timed automaton, and ' an MTL formula build over the set AP of atomic propositions. An abstract model for the automaton A and the formula ' is a tuple M' = (Sb; s0; ,!; Vb), where Sb = L (ID0 : : : IDn 1) is the set of abstract states, s0 = (`0; f0gn+1) is the initial state, Vb : Sb ! 2AP is a valuation function such that for all p 2 AP , p 2 Vb((`; v)) iff p 2 V (`), and ,! S Act0 S, where Act0 = Act [ f g, is a transition relation defined by the time and action transitions: – Time transition: (`; v) ,! (`; v0) iff v j= Inv(`), v0 = succ(v), and v0 j= Inv(`), – Action transition: for any 2 Act, (`; v) ,! (`0; v0) iff there exists a transition ` ;c!c;X `0 2 T such that v j= cc ^ Inv(`), v0 = v[X := 0], and v0 j= Inv(`0). Definition 5. A path in M' is a sequence = (s0; s1; : : :) of states such that for each j 2 IN, either (sj ,! sj+1) or (sj ,! sj+1) for some transition is preceded by at least one time transition. Let I be the set of all intervals in IN. Let AP I = fqI j I 2 Ig. The LTLq formulae in the negation normal form are defined by the following grammar: ::= true j false j p j :p j qI j :qI j ^ j _ j U j G , where p 2 AP and qI 2 AP I . The temporal modalities U and G are, respectively, named as the until and the always. The derived basic temporal modality for eventually is defined in the standard way: F d=ef trueU .
In order to improve readability, in the following definition we write h ; mi j=k instead of M'; h ; mi j=k , for any LTLq formula .
Definition 6. The satisfiability relation j=d, which indicates truth of an LTLq formula in the abstract model M' along the path with the starting point m and at the depth d > m, is defined inductively as follows: – h ; mi j=d true, h ; mi 6 j=d false, – h ; mi j=d p iff p 2 V( (d)), h ; mi j=d :p iff p 2= V( (d)), – h ; mi j=d qI iff (d) (m) 2 I, – h ; mi j=d :qI iff (d) (m) 62 I, ––– hhh ;;; mmmiii jjj===ddd U_^ iiiffffff(hh9j;; mm>iid)jj==(hdd ; doairnjd=hhj; m;mainijd=j=(d8dd, 6, i < j) h ; di j=i – h ; mi j=dG iff (8j > d) h ; di j=j . ),
An LTLq formula existentially holds in the model M', written M' j= E , if, and only if M'; h ; 0i j=0 for some path starting at the initial state. The existential model checking problem asks whether M' j= E . 3.3
Let p 2 AP , and be formulae of MTL. We define the translation from MTL into LTLq as a function tr : MTL ! LTLq in the following way: – tr(true) = true, tr(false) = false, tr(p) = p, tr(:p) = :p, – tr( ^ ) = tr( ) ^ tr( ), tr( _ ) = tr( ) _ tr( ), – tr( UI ) = tr( )Utr(qI ^ ), tr(GI ) = G(:qI _ tr( )) Observe that the translation of literals as well as logical connectives is straightforward. The translation of the UI operator ensures that holds somewhere in the interval I (this is expressed by the requirement qI ^ tr( )), and holds always before . Similarly, the translation of the GI operator ensures that always holds in the interval I (this is expressed by the requirement :qI _ tr( )).
Theorem 1. Let A be a discrete timed automaton, MA the concrete model for A, ' an MTL formula, and M' the abstract model for the automaton A and the formula '. Then, MA j= E' if, and only if M' j= Etr('). 4
In this section we define a bounded semantics for LTLq in order to translate the existential model checking problem for LTLq into the satisfiability problem. 4.1
To define the bounded semantics one needs to represent infinite paths in a model in a
special way. To this aim, we recall the notions of k-paths and loops [
Definition 7. Let M' be a model, k 2 IN, and 0 6 l 6 k. A k-path is a pair ( ; l), also denoted by l, where is a finite sequence = (s0; : : : ; sk) of states such that for each 0 6 j < k, either (sj ,! sj+1) or (sj ,! sj+1) for some 2 Act, and every action transition is preceded by at least one time transition. A k-path l is a loop, written a( l) for short, if l < k and (k) = (l).
If a k-path l is a loop it represents the infinite path of the form uv!, where u = ( (0); : : : ; (l)) and v = ( (l + 1); : : : ; (k)). We denote this unique path by l. Note that for each j 2 IN, ell+j = elk+j . e
In the definition of bounded semantics for variables from AP I one needs to use only a finite prefix of the sequence ( el (0); l (1); : : :). Namely, for a k-path l that is not a loop the prefix of the length k is needeed, and for a k-path l that is a loop the prefix of the length k + k l is needed.
In order to improve readability, in the following definition we write h l; mi j=k instead of M'; h l; mi j=k , for any LTLq formula .
Definition 8 (Bounded semantics). Let M' be the abstract model, l be a k-path in M', and 0 6 m; d 6 k. The relation j=dk is defined inductively as follows: d :> eell ((dd)+ k – h l; mi j=k :qI iff h l; mi 6 j=dk qI – h l; mi j=dk true, h l; mi 6 j=dk false, – h l; mi j=dk p iff p 2 V( l(d)), h l; mi j=k :p iff p 2= V( l(d)), d 8>< el (d) if l is not a loop; – h l; mi j=dk qI iff if l is a loop and d > m; el (m) 2 I; if l is a loop and d < m; el (m) 2 I; el (m) 2 I;
l) – h l; mi j=dk G
d – h l; mi j=k
d
– h l; mi j=k
– h l; mi j=dk
Theorem 2. Let A be a discrete timed automaton, ' an MTL formula, and M' the
abstract model for the automaton A and the formula '. Moreover, let = tr('). Then,
M' j= E if, and only if there exists k > 0 such that M'j=kE .
The last step of our method is the standard one (see [
Theorem 3. Let M' be an abstract model. Then, for every k 2 IN, M' j=dk Etr(') if, and only if, the propositional formula [M'; tr(')]k is satisfiable. 5
In this section we experimentally evaluate the performance of our new translation.
We have conducted the experiments using the slightly modified timed generic pipeline
paradigm (TGPP) [
The Timed Generic Pipeline Paradigm (TGPP) discrete timed automata model shown in Figure 1 consists of Producer producing data within the certain time interval ([a; b]) or being inactive, Consumer receiving data within the certain time interval ([c; d]) or being inactive within the certain time interval ([g; h]), and a chain of n intermediate Nodes which can be ready for receiving data within the certain time interval ([c; d]), processing data within the certain time interval ([e; f ]) or sending data. We assume that a = c = e = g = 1 and b = d = f = h = 2 n + 2, where n represents number of nodes in the TGPP.
To compare our experimental results with [
All the benchmarks together with instructions on how to reproduce our experimental results can be found at the web page http://ajd.czest.pl/~a.zbrzezny/ bmc.html.
The number of considered k-paths (fk) for the new translation is always equal to 1 and for the old translation is respectively equal to: fk('0) = 2, fk('1) = 2, fk('2) = 2, fk('3) = 3, fk('4) = 8 n + 9, fk('5) = 16 n + 17. The length of the witness for the formula '0 is equal to 4 n + 4 ; for the formula '1 is equal to 8 n + 6; for the formula '2 and is equal to 8 n + 6; for the formula '3 is equal to 8 n + 15; for the formula '4 is equal to 8 n + 6; for the formula '5 is equal to 8 n + 6.
From Fig. 2 one can observe that the new method is able to verify the formula '0 for TGPP with 27 nodes. The old method is able to verify the formula '0 for TGPP with 24 nodes. The memory usage for the old method is 1:72 times higher than for the new method for 24 nodes.
Total time usage for a TGPP ϕ1 New translation
Old translation 4500 4000 3500 . 3000 c se 2500 n iem 2000 iT 1500 1000 500 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Number of Nodes 800 700 600 BM 500 n iry 400 o em 300 M 200 100 0
Memory usage for a TGPP ϕ1 New translation
Old translation 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Number of Nodes
From Fig. 3 one can observe that the new method is able to verify the formula '1 for TGPP with 17 nodes. The old method is able to verify the formula '1 for TGPP with 15 nodes. The memory usage for the old method is 1:50 times higher than for the new method for 15 nodes.
From Fig. 4 one can observe that the new method is able to verify the formula '2 for TGPP with 18 nodes. The old method is able to verify the formula '2 for TGPP with 15 nodes. The memory usage for the old method is 1:55 times higher than for the new method for 15 nodes.
From Fig. 5 one can observe that the new method is able to verify the formula '3 for TGPP with 17 nodes. The old method is able to verify the formula '3 for TGPP with 13 nodes. The memory usage for the old method is 2:21 times higher than for the new method for 13 nodes.
From Fig. 6 one can observe that the new method is able to verify the formula '4 for TGPP with 13 nodes. The old method is able to verify the formula '4 for TGPP with 7 nodes. The memory usage for the old method is 10:32 times higher than for the new method for 7 nodes.
From Fig. 8 one can observe that the new method is able to verify the formula '5 for TGPP with 13 nodes. The old method is able to verify the formula '5 for TGPP with 6 nodes. The memory usage for the old method is 21:39 times higher than for the new method for 6 nodes.
For the formula '4 the new method generates only 395775 variables and 1229009 clauses (Fig. 7) for 7 nodes. The time consumed by BMC to generate the set of clauses is equal 65:35 sec. The memory consumed by BMC to generate the set of clauses is 1 2 3 4 5 6 7 8 9 10 11 12
Number of Nodes 1 2 3 4 5 6 7 8 9 10 11 12
Number of Nodes equal 100:54 MB. The time and memory consumed by the state of the art SAT solver CryptoMiniSat5, respectively is equal to 112:59 sec. and 287:41 MB.
The old method generates 6122646 variables and 18739998 clauses. The time consumed by BMC to generate the set of clauses is equal 977:18 sec. The memory consumed by BMC to generate the set of clauses is equal 1505:05 MB. The time and memory consumed by the state of the art SAT solver CryptoMiniSat5, respectively is equal to 2892:31 sec. and 2967:82 MB.
The example above shows that our new method results in reducing the overall runtime and memory of BMC to construct a CNF formula, and of SAT solver to check satisfiability of this formula.
We have proposed, implemented, and experimentally evaluated SAT-based BMC method for soft real-time systems, which are modelled by discrete timed automata, and for properties expressible in MTL with the semantics over discrete timed automata. The method is based on a translation of the existential model checking for MTL to the existential model checking for LTLq, and then on the translation of the existential model checking for LTLq to the propositional satisfiability problem.
In the following table we compare the new BMC method with the old one.
Simple BMC+DTA&MTL
no new clocks no new transitions
only one path smaller number of propositional
variables and clauses better time and memory usage
BMC+DTA&MTL[
of intervals in the given formula exponential number of new transitions a number of paths depending on the given formula and the length of the k-path
substantially larger number of propositonal variables and clauses
worse time and memory usage
The experimental results show that our approach is much better than the approach based on translation to HLTL. The reason is that the new method needs only one new path, does not need any new clocks, and does not need any new transitions. The experiments confirm that the improvement in question leads to a reduction of the size of the CNF formulas submitted to the SAT solver, and therefore to a significant reduction both in the time and memory required by the SAT solver to return an answer. The paper presents preliminary experimental results only, but they show that the proposed verification method is quite efficient and worth exploring.
Therefore, in our future work we are going to define the SMT-based BMC encoding for DTA and for LTLq and compare this encoding with the SAT-based encoding, and we would like to develop SAT-based BMC method for timed automata and properties expressible in TECTL.