We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete in nite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of TGPP, a Timed Generic Pipeline Paradigm modelled by a network of discrete timed automata.
Introduction
Nowadays the interest in model checking [
Bounded model checking (BMC) [
The original contributions of the paper are as follows. First, we de ne a SAT-based BMC for soft real-time systems, which are modelled by discrete grant
No.
timed automata, and for properties expressible in MTL. Next, we report on
the implementation of the proposed BMC method as a new module of VerICS
[
The rest of the paper is structured as follows. In Section 2 we brief the basic notion used through the paper. In Section 3 we de ne the BMC method for HLTL. In Section 4 we discuss our experimental results. In Section 5 we conclude the paper. 2
Preliminaries
We assume familiarity with the notion of discrete timed automaton (DTA) and
their semantics in terms of the Kripke structure (called model). We refer the
reader to the body of the paper [
UI j
RI
We refer the reader to the body of the paper [
Determining whether an MTL formula ' is existentially (resp. universally) valid in a given model is called an existential (resp. universal ) model checking problem.
In order to de ne a SAT-based BMC method for MTL, we rst translate the
existential model checking problem for MTL that is interpreted over the region
graph (i.e., a standard nite model de ned for (discrete) timed automata) to the
existential model checking problem for HLTL that is also interpreted over the
region graph. For the details on this translation and the semantics of the HLTL
language we refer the reader to [
Let ' be an MTL formula, n the number of intervals in ', p 2 PV a propositional variables, and h = 0; : : : ; n 1. The HLTL formulae in release positive normal form are given by the following grammar: :=> j ? j p j :p j ^ j _
j Hh j U j R where the symbols U and R denote the until and release modalities, respectively. The indexed symbol Hh denotes the reset modality representing the reset of the clock number h. In addition, we introduce some useful derived temporal modalities: G d=ef ?R (always), F d=ef >U (eventually ).
Let ' be a MTL formula. We translate the formula ' inductively into the HLTL formula H(') in the following way:
H(>) = >, H(?) = ?, H(p) = p, H(:p) = :p, for p 2 PV, H( _ ) = H( ) _ H( ), H( ^ ) = H( ) ^ H( ), H( UIh ) = Hh(H( )U(H( ) ^ pyh2Ih ^ (pnf _ H( )))),
H( RIh )) = Hh(H( )R(:pyh2Ih _ H( ))).
Observe that the translation of literals as well as logical connectives is straightforward. The translation of the UIh operator ensures that: (1) the translation of holds in the interval I { this is expressed by the requirement H( ) ^ pyh2Ih ; (2) the translation of holds always before the translation of ; and (3) if the value of the clock yh belong to the nal zone, i.e. the values of all the clocks are bigger then some maximal value (in this case the proposition pnf is not true), then the translation of H( ) is taken into account as well. The translation of the RIh operator makes use of the fact RIh = UIh ^ _ GIh .
This translation preserves the existential model checking problem, i.e., the existential model checking of an MTL formula ' over the discrete model can be reduced to the existential model checking of H(') over the region graph.
The next step in de ning a SAT-based BMC method for MTL relies on
introducing a discretisation scheme for the region graph (de ned for a given discrete
timed automaton) that will represent zones (i.e. sets of equivalent clock
valuations) of the region graph by exactly one specially chosen representative, and
proving that a discretised model based on this scheme preserves the validity of
the HLTL formulae - the discretised model constitutes the base for an
implementation of our BMC method. We do not report on this step here in detail,
since it requires introducing the huge mathematical machinery, but in fact it
can be done in a way similar to the one presented in [
The nal step in de ning a SAT-based BMC method for MTL relies on de ning the BMC method for HLTL. This is described in the next section. 3
Bounded model checking for HLTL Bounded semantics of a logic in question with existential interpretation is always used as the theoretical basis for the SAT-based bounded model checking. In the paper we have decided not to provide this semantics and not to show its equivalence to the unbounded semantics. This will be presented in the full version of the paper. Here, we only focus on the core of the BMC method, i.e. on the translation to SAT.
Let A be a discrete timed automaton, ' an MTL formula, = H(') the
corresponding HLTL formula, M a discretized model for A' (this an extension
of A { for the exact construction we refer to [
The de nition of the formula [M; ]k requires, among other, states of the model M to be encoded in a symbolic way. This encoding is possible, since the set of states of M is nite. In particular, we represent each state s by a vector w = (w1; : : : ; wr) (called a symbolic state) of propositional variables (called state variables ), whose length r depends on the number of locations and clocks in A'. Further, we need to represent nite pre xes of paths in a symbolic way. We call this representation a j-th symbolic k-path j and de ne it as a pair ((w0;j ; : : : ; wk;j ); uj ), where wi;j are symbolic states for 0 j < fk( ) and 0 i k, and uj is a symbolic number for 0 j < fk( ). The symbolic number uj is a vector uj = (u1;j ; : : : ; ut;j ) of propositional variables (called natural variables ), whose length t equals to max(1; dlog2(k + 1)e), and it is used to encode the looping conditions. Next, we need an auxiliary function fbk : HLTL ! N that gives a bound on the number of k-paths su cient for validating a given HLTL formula. The function is de ned as fbk( ) = fk( ) + 1, where fk(>) = fk(?) = fk(p) = fk(:p) = 0 for p 2 PV; fk( ^ ) = fk( ) + fk( ); fk( _ ) = maxffk( ); fk( )g; fk(Hh ) = fk( )+1; fk( U ) = k fk( )+fk( ); fk( R ) = (k + 1) fk( ) + fk( ).
The formula [M ; ]k { the 1st conjunct of Formula (1) { encodes fbk( )-times unrolled transition relation, and it is de ned in the following way: [M
fck(') ; ]k := I (w0;0)^ _
fbk( ) k 1 H(w0;0; w0;j )^ ^ ^
T (wi;j ; wi+1;j )^ j=1 j=1 i=0 fbk( ) k ^ _ Bl=(uj ) j=0 l=0 (2) where wi;j are symbolic states, uj is a symbolic number, I (w0;0) and Bl=(uj ) are formulae encoding the initial state, and the value l, respectively. H(w; w0) is a formula that encodes equality of two global states. The formula T (wi;j ; wi+1;j ) is disjunction of three formulas: T (wi;j ; wi+1;j ), T A(wi;j ; wi+1;j ), and A(wi;j ; wi+1;j ) that encode respectively the time, time-action, and action successors of M.
The formula [ ]M;k := [ ][0;1;Fk( )] { the 2nd conjunct of Formula (1) {
enk
codes the translation of a HLTL formula along a k-path, whose number belongs
to the set Fk( ) = fj 2 N j 1 j fbk( )g. The main idea of this translation
consists in translating every subformula of using only fk( ) k-paths. More
precisely, given a formula and a set Fk( ) of indices of k-paths, following [
First, we recall the relation that is de ned on the power set of N as: A B i for all natural numbers x and y, if x 2 A and y 2 B, then x < y. Now, let A N be a nite nonempty set, and n; d 2 N, where d jAj. Then, gl(A; d) denotes the subset B of A such that jBj = d and B A n B. gr(A; d) denotes the subset C of A such that jCj = d and A n C C. gs(A) denotes the set A n fmin(A)g. if n divides jAj d, then hp(A; d; n) denotes the sequence (B0; : : : ; Bn) of subsets of A such that Sjn=0 Bj = A, jB0j = : : : = jBn 1j, jBnj = d, and Bi Bj for every 0 i < j n.
Now let hU(A; d) d=f hp(A; d; k) and hkR(A; d) d=f hp(A; d; k + 1). Note that if
k
hkU(A; d) = (B0; : : : ; Bk), then hkU(A; d)(j) denotes the set Bj, for every 0 j
k. Similarly, if hkR(A; d) = (B0; : : : ; Bk+1), then hR(A; d)(j) denotes the set Bj,
k
for every 0 j k + 1. Further, the function gs is used in the translation of
subformulae of the form Hh , if a set A is used to translate this formula, then
the path of the number min(A) is used to translate the operator Hh and the set
gs(A) is used to translate the subformula . For more details on the remaining
functions we refer to [
Now we are ready to de ne the formula [ ][k0;1;Fk( )]. Let be a HLTL formula, and k 0 a bound. We can de ne inductively the translation [ ][km;n;A] of along the n-th symbolic k path n (n 2 Fk( )) with starting point m by using the set A as shown below. Let cl(wm;n; h) denote the fragment of the symbolic state wm;n that encodes the h-th clock from the set Y, n0 = min(A), hkU = hkU(gs(A); fk( )), and hkR = hkR(gs(A); fk( )). Then, [>][km;n;A] := >, [?][km;n;A] := ? [m;n;A] := p(wm;n), [:p][km;n;A] := :p(wm;n), [ ^ ][km;n;A] := [ ][km;n;gl(A,;f[pk(]k ))] ^ [ ][km;n;gr(A;fk( ))], [ _ ][km;n;A] := [ ][km;n;gl(A;fk( ))] _ [ ][km;n;gl(A;fk( ))], [Hh( U )][km;n;A] := Vjm=01 H(wj;n; wj;n0 ) ^ Hh=0(wm;n; wm;n0 )^ Vjk=m+1 H6=h [Hh( R )][km;n; A] := Vjm=01 H(wj;n; wj;n0 ) ^ Hh=0(wm;n; wm;n0 ) ^ Vk j=m+1 H6=h (wj;n; wj;n0 ) ^ Wjk=m([ ][kj;n0;hkR(k+1)] ^ Vij=m[ ][ki;n0;hkR(i)]) (wj;n; wj;n0 ) ^ Wjk=m([ ][kj;n0;hkU(k)]^ Vij= m1[ ][ki;n0;hkU(i)]) _ Vjk=m+1 H6=h(wj;n; wj;n0 ) ^ Hh=0(wm;n; wm;n0 )^
Wm 1
l=0 (Llk( n0 ) ^ Vlj=10 H(wj;n; wj;n0 ) ^ H(wl;n0 ; wk;n0 )^ Vjm=l +11 H6=h(wj;n; wj;n0 )) ^ Wjm=01(Bj>(un0 ) ^ [ ][kj;n0;hkU(k)] ^ Vij=0 (Bi>(un0 ) ! [ ][ki;n0;hkU(i)])) ^ Vik=m[ ][ki;n0;hkU(i)],
1 _ Vjk=m+1 H6=h(wj;n; wj;n0 ) ^ Hh=0(wm;n; wm;n0 )^
Wm 1
l=0 (Llk( n0 ) ^ Vlj=10 H(wj;n; wj;n0 ) ^ H(wl;n0 ; wk;n0 )^ Vjm=l+1 H6=h(wj;n; wj;n0 )) ^ 1
Wjm=0(Bj>(u0n) ^ [ ][kj;n0;hkR(k+1)] H6=h(wj;n; wj;n0 ) ^ Vjk=m[ ][kj;n0;hkR(j)]^ Bright(h)(cl(wk;n0 ; h)) _Bright(h)(cl(wk;n0 ; h)) ^ Vjm=01 H(wj;n; wj;n0 ) ^ Hh=0
> (wm;n; wm;n0 ) ^ Vk j=m[ ][kj;n0;hkR(j)]
j=m+1 H6=h(wj;n; wj;n0 ) ^ Vk ^(Wlk=m1 (Llk( n0 ))_ Bright(h)(cl(wk;n0 ; h)) ^ Hh=0(wm;n; wm;n0 )
> ^WVmjk= m1+1 H6=h(wj;n; wj;n0 ) ^ Vjk=m[ ][kj;n0;hkR(j)]^
l=0 (Llk( n0 ) ^ Vlj=10 H(wj;n; wj;n0 ) ^ H(wl;n0 ; wk;n0 )^ Vm 1 j=l +11[ ][j;n0;hkR(j)]) .
j=l+1 H6=h(wj;n; wj;n0 ) ^ Vm k where p(w) is a formula that encodes a set of states of M in which p 2 PV holds; H(w; w0) is a formula that encodes equality of two global states; Hh=0(w; w0) is a formula that for two global states encodes the equality of their locations, the equality of values of the original clocks (i.e., clocks from X), and the equality of values of the new clocks (i.e., clocks from Y) but the value of clock yh. For clock yh the formula guarantees that its value in the 2nd global state is equal to zero; H6=h(w; w0) is a formula that for two global states encodes the equality of their locations, the equality of values of the original clocks, and the equality of the values of the new clocks with the potential exception of clock yh. For clock yh the formula guarantees that its value in the 2nd global state is greater than zero; HX(w; w0) is a formula that encodes equality of two global states on locations and values of the original clocks; Bjs(v) is a formula that encodes that the value represented by the vector of propositional variables v is in arithmetic relation s with the value j, where s 2 f<; 6; =; >; >g; Llk( j ) := Bk>(uj ) ^ HX(wk;j ; wl;j ).
The following theorem, whose proof will be provided in the full version of the paper, guarantees that the bounded model checking problem can be reduced to the SAT-problem.
Theorem 1. Let M be a discrete abstract model, and a HLTL formula. Then for every k 2 N, is existentially valid in M with the bound k if, and only if, the propositional formula [M; ]k is satis able. 4
Experimental results
Our SAT-based BMC method for MTL, interpreted over the discrete time
models, and discrete timed automata is, to our best knowledge, the rst one formally
presented in the literature, and moreover there is no any other model checking
technique for the considered MTL language. Further, our implementation of the
presented BMC method uses Reduced Boolean Circuits (RBC) [
For the tests we have used a computer with Intel Core i3-2125 processor, 8 GB of RAM, and running Linux 2.6. We set the time limit to 900 seconds, and memory limit to 8GB, and we used the state of the art SAT-solver MiniSat 2. The speci cations for the described benchmark are given in the universal form, for which we verify the corresponding counterexample formula, i.e., the formula which is negated and interpreted existentially.
To evaluate the performance of our SAT-based BMC algorithms for the veri cation of several properties expressed in MTL, we have analysed a Timed Generic Pipeline Paradigm (TGPP) discrete timed automata model shown in Figure 1. It consists of Producer producing data (P rodReady) or being inactive, Consumer receiving data (ConsReady) or being inactive, and a chain of n intermediate Nodes which can be ready for receiving data (N odeiReady), processing data (N odeiP roc), or sending data (N odeiSend). The example can be scaled by adding intermediate 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, Consumer, and of the intermediate Nodes. start Produce x0 ≥ a x1 := 0
ProdReady x0 ≤ b Send1 x0 := 0 ProdSend start
Send1 x1 ≥ c x1 := 0 Proc1 x1 ≥ e x2 := 0
Node1Ready x1 ≤ d Node1Proc x1 ≤ f Node1Send · · · start
Sendn xn ≥ c xn := 0 Send2 x1 := 0
Procn xnx+n1≥:=e0
NodenReady xn ≤ d NodenProc xn ≤ f NodenSend start
Sendn+1 Sendn+1 xn+1 ≥ c xn := 0 xn+1 := 0
ConsReady xn+1 ≤ d
out xn+1 ≥ g xn+1 := 0 ConsFree xn+1 ≤ h We have tested the TGPP discrete timed automata model, scaled in the number of intermediate nodes and with all the intervals set to [1; 3], on the following MTL formulae: '1 = G[0;1)(P rodSend ) F[2n+1;2n+2)ConsF ree), where n is the number of nodes. It expresses that each time Producer produces data, then Consumer receives this data in 2n + 1 time units. '2 = G[0;1)(P rodSend ) F[2n+1;2n+2)(ConsF ree ^ F[1;2)ConsReady)), where n is the number of nodes. It expresses that each time Producer produces data, then Consumer receives this data in 2n + 1 time units and one unit after that it will be ready to receive another data.
Since there is no model checker that supports the MTL properties of systems modelled by discrete timed automata, we were not able to compare results of the application of our method to a TGPP system with others.
We provide a preliminary evaluation of our method by means of the running time and the consumed memory. We have observed that for both formulae '1 and '2, we managed to compute the results for 5 nodes in the time of 900 seconds. The exact data for the mentioned maximal number of nodes are the following: '1: k = 20, fk('1) = 3, bmcT is 6.50, bmcM is 19.54, satT is 25.24, satM is 43.00, bmcT+satT is 31.74, max(bmcM,satM) is 43.00; '2: k = 20, fk('2) = 24, bmcT is 89.96, bmcM is 163.40, satT is 610.23, satM is 310.00, bmcT+satT is 700.19, max(bmcM,satM) is 310.00; where k is the bound, fk(') is the number of symbolic k-paths, bmcT is the encoding time, bmcM is memory use for encoding, satT is the satis ability checking time, satM is memory use for the satis ability checking.
The preliminary results are very promising and indicate that the method is worthy of further investigation for which purpose especially designed benchmarks will be developed. 5
Conclusions We have introduced a SAT-based approach to bounded model checking of discrete timed automata and properties expressed in MTL with discrete semantics. The method is based on a translation of the existential model checking for MTL to the existential model checking for HLTL, and then on the translation of the existential model checking for HLTL to the propositional satis ability problem. The two translations have been implemented and tested on the benchmark, which has been carefully selected in such a way as to reveal the advantages and disadvantages of the presented approaches.