A comparison of SAT-based and SMT-based bounded model checking methods for ECTL*

Abstract

In this paper we present a comparison of the SAT-based bounded model checking (BMC) and SMT-based bounded model checking methods for ECTL* properties of a parallel composition of transition systems. In the both methods we use the parallel composition (of the transition systems) based on the interleaved semantics. Moreover, the both methods use the same bounded semantics of ECTL* formulae, the compatible encodings of the transition systems and the compatible translations of ECTL* formulae. For the SAT-based BMC we have used the PicoSAT solver and for the SAT-based BMC we have used the Z3 solver. We have implemented the both methods and made some preliminary experimental results which shows that generally the SAT-based method is superior to the SMT-based method. However, in some cases the SMT-method overcomes the SAT-based method.

1 Introduction

The problem of model checking [ 10 ] is to check automatically whether a structure M defines a model for a modal (temporal, epistemic, etc.) formula . The practical applicability of model checking is strongly limited by the state explosion problem, which means that the number of model states grows exponentially in the size of the system representation. To avoid this problem a number of state reduction techniques and symbolic model checking approaches have been developed, among others, [ 8, 9, 19, 20 ].

The SAT-based bounded model checking (BMC) is one of the symbolic model checking technique designed for finding witnesses for existential properties or counterexamples for universal properties. Its main idea is to consider a model reduced to a specific depth. The first BMC method was proposed in [ 5 ], and it was designed for linear time properties. Next in [ 21 ] the method has been extended to handle branching time properties.

The SMT problem [ 7 ] is a generalisation of the SAT problem, where Boolean variables are replaced by predicates from various background theories, such as linear, real, and integer arithmetic. SMT generalises SAT by adding equality reasoning, arithmetic, fixed-size bit-vectors, arrays, quantifiers, and other useful first-order theories.

The SMT-based bounded model checking is quite new technique. It was using to verifying Embedded ANSI-C Software [ 12 ], C++ Programs [ 22 ], Multi-threaded Software [ 11 ], Fixed-Point Digital Controllers [ 3 ], timed automata [ 17 ], real-time systems [ 24 ], LTL Specifications with Integer Constraints [ 2 ] and many others.

In order to use the bounded model checking method we need to define a translation from a given temporal logic to the satisfiability modulo theories problem (in short: to SMT). As far as we know, no such translation was given in the literature. However, several translations to SAT from ECTL* and its sublogics were proposed. The first translation from LTL to SAT was introduced in [ 4 ] and another ones in [ 18 ] and [ 6 ]. The first translation from ECTL to SAT was introduced in [ 21 ] and then it was substantially improved in [ 25 ]. The first correct translation from ECTL* to SAT was introduced in [ 23 ] and then it was substantially improved in [ 26 ]. The translation from ECTL* to SMT that we use in this paper strictly follows the translation from ECTL* to SAT introduced in [ 26 ].

The rest of the paper is organised as follows. In the next section we give some remarks about the syntax and (both the bounded and unbounded) semantics of ECTL*. In Section 3 we give some remarks about our translation from ECTL* to SMT. Preliminary experimental results and some conclusions are presented in Section 4. 2

Syntax and Semantics of ECTL* In this section we briefly recall the syntax and semantics of the logic ECTL*. The Existential Computation Tree Logic ECTL* is a restriction of a propositional branchingtime temporal logic CTL* introduced by Emerson and Halpern in [ 15 ] as a specification language for finite-state systems. The restriction consists in using only existential path quantifiers and allowing the negation to be applied to propositional variables only (instead of to arbitrary formulae). For more thorough description one can see [ 1 ]. 2.1

Syntax of ECTL*

The language of ECTL* consists of two types of formulae: state formulae (interpreted at states) and path formulae (interpreted along paths). The syntax of ECTL* state formulae over the set AP of atomic propositions is defined by the following grammar: ::= true j false j p j :p j 1 ^ 2 j 1 _ 2 j E' where p 2 AP , 1, 2 and are state formulae, and ' is a path formula. The syntax of ECTL* path formulae over the set AP of atomic propositions is defined by the following grammar: ' ::=

j '1 ^ '2 j '1 _ '2 j X'1 j '1U'2 j '1R'2 where is a state formula and ', '1 and '2 are path formulae. In practice, many interesting temporal properties are formulated by using temporal operators F (eventually) and G (always) defined as follows:

Definition 1. A transition system is a tuple M = (S; Act; !; s0; AP; L), where S is a nonempty finite set of states, Act is a set of actions, s0 2 S is the initial state, ! S Act S is a transition relation, AP is a set of atomic propositions, and L : S ! 2AP is a labelling function that assigns to each state a set of atomic propositions that are assumed to be true at that state.

Definition 2. An ECTL* state formula is valid in M, denoted by M j= , iff s0 j= , i.e., holds at the initial state of M. 2.3

Bounded Semantics of ECTL*

The bounded semantics of ECTL* is defined in [ 26 ]. This is done in order to define the bounded model checking problem for ECTL* and to translate it into the satisfiability problem. For more thorough description one can see [ 26 ].

From now on we assume that models are finite, i.e. the sets S, Act and AP are finite. To define the bounded semantics one needs to represent infinite paths in a model in a special way. To this aim, the notions of k-paths and loops are defined. Definition 3. Let M be a model, k 2 N, and let l 2 N such that 0 6 l 6 k. A kpath is a pair ( ; l), also denoted by l, where is a finite sequence = (s0; : : : ; sk) of states such that sj !sj+1 for each 0 6 j < k. A k-path l is a loop 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 N, %( l)l+j = %( l)k+j .

Let s be a state and l be a k-path. For a state formula over AP , the notation M; s j=k means that k-holds at the state s in the model M. Similarly, for a path formula ' over AP , the notation M; lm j=k ', where 0 6 m 6 k, means that ' k-holds along the suffix (m); : : : ; (k) of l.

Lemma 1. Let M be a model. For every ECTL* path formula ', every k-path l in M, and every 0 6 m 6 k, if M; lm j=k ', then 2 M such that [::k] = it holds M; m j= 1. if l is not a loop, then for each path

'. 2. if l is a loop, then M; %( l)m j= ', Theorem 1. Let M be a model and iff for some k 2 N, M; s0 j=k .

be an ECTL* state formula. Then M; s0 j=

Translation to SMT

We have implemented a translation to SMT strictly following the translation to SAT given in [ 26 ]. In our translation to SMT states, loops and actions are represented by natural variables. Since M is a parallel composition of a finite number n of finite transition system, every state of M can be encoded as a natural number vector of the length n. Thus, each state of M can be represented by a valuation of a vector (called a symbolic state) of different individual variables called individual state variables. Moreover, every action of M can be represented by a valuation of an individual variable, and the designated positions l of the k-paths used in the translation can be also be represented by valuations of individual variables. Furthermore, k-paths can be represented as vectors of symbolic states.

The details of the translation to SMT will be provided in the full version of the present paper. 3.1

Bounded Model Checking of ECTL* properties

Now let us recall the the BMC method of verifying a given ECTL* state formula . Let I(w0;0) be a be a quantifier-free first-order formula representing the initial state, [M ]kFk( ) be a quantifier-free first-order formula representing transition relation and [0;0;Fk( )] be a quantifier-free first-order formula that is the translation of the formula h ik

. In order to verify the formula one has to check the satisfiability of the following conjunction:

[M ]k := I(w0;0) ^ [M ]kFk( ) ^ h i[k0;0;Fk( )] starting with k = 0. If for a given k the formula [M ]k is not satisfiable, then k is increased and the resulting formula is to be checked by a SMT-solver again. The method described relies on the following theorem.

Theorem 2. Let M be a model and be an ECTL* state formula. Then for every k 2 N, M; s0 j=k if, and only if, the quantifier-free first-order formula [M ]k is satisfiable. 4

Experimental Results

In this section we present a comparison of a performance evaluation of two methods: SMT-based BMC and SAT-based BMC for dining philosophers problem.

An evaluation of both BMC algorithms is given by means of the running time and the memory used. In order to compare the translation to SMT with the translation to SAT we have implemented both the algorithms as standalone programs written in the programming language C++. In our SAT-BMC technique we use the state of the art SATsolver PicoSAT (http://fmv.jku.at/picosat/) and in SMT-BMC technique we use the state of the art SMT-solver Z3 [ 13 ] (http://z3.codeplex.com/).

Our experiments were performed on a computer equipped with I7-3770 processor, 32 GB of RAM, and the operating system Arch Linux with the kernel 3.15.3. As the benchmark we used the well-known dining philosophers problem [ 14, 16 ]. We have modelled this problem by means of communicating finite automata. The system consists of n automata each of which models a philosopher, together with n automata each of which models a fork, together with one automaton which models the lackey. The latter automaton is used to coordinate the philosophers’ access to the dining-room. In fact, this automaton ensures that no deadlock is possible. The global system is obtained as the parallel composition of the components, which are shown in Figure 1. outj 0 5

0 0 in0, . . . , inn−1 out0, . . . , outn−1 inj putj 1 4

getj put(j+1) mod n getj, get(j−1) mod n putj, put(j−1) mod n 1 q q q n-2 1 2 3 Let AP = fpj j 0 6 j < n; 0 6 i 6 5g and assume that the variable pij is true i only at the i-th state of the j-th philosopher. We have tested three ECTL* formulae over AP in order to compare the experimental results for the translation to SAT with the experimental results for the translation to SMT. All the tested formulae are valid in the considered model for every n 2.

The first formula

n 1 '1 = ^ E F pj3 :

j=0 expresses the following property: For each philosopher there exists a path on which this philosopher eventually gets his left and right forks.

In Figures 2(a) and 2(b) we present a comparison of total time usage and total memory usage for the formulae '1.

The second formula get(j+1) mod n in0, . . . , inn−1 out0, . . . , outn−1 n-1 700 SAT 600 SMT 500 .cse 400 n i ieTm 300 200 100 1400 SAT 1200 SMT 1000 .cse 800 n i ieTm 600 400 200 n b 2 c '2 = EGF ^ j=0 expresses the following property: There exists a path on which every philosopher eventually gets his left and right forks.

In Figures 4(a) and 4(b) we present a comparison of total time usage and total memory usage for the formulae '3.

Total time usage for a DP, formula 1

Memory usage for a DP, formula 1 0 5 10 15 20 25 30 35 40 45 50 55 60 65 70 75 80 85 90 95 100

Number of philosophers (a)

Our preliminary experimental results suggest that generally the SAT-based method is superior to the SMT-based method. However, in some cases the SMT-method overcomes the SAT-based method. An observation of experimental results leads to the conclusion that the SAT-based BMC for ECTL* uses less time and memory comparing to the SMT-based BMC for ECTL*. In particular, using the SAT-based BMC it was possible to verify the formula '1 for 100 philosophers, whereas using the SMT-based BMC it was possible to verify the formula '1 for 40 philosophers only. However, it was possible to verify the formulae '2 and '3 for the same numbers of philosophers for the both methods. Moreover, the experimental results for formulae '2 and '3 lead to the conclusion that the SMT-based BMC method uses less time than the SAT-based BMC method when the number of philosophers increases.

We should stress that the implementation of the SMT-based BMC we used for performing the experiments is our first implementation that uses SMT solvers. Therefore, 12000 SAT

SMT 10000 8000 . cse ine 6000 m i T 4000 2000 50000 SAT 45000 SMT 40000 35000 .c 30000 isene 25000 iTm 20000 15000 10000 5000 0 2 350 SMT 300 .c 250 se ine 200 we hope to improve the implementation in the near future by taking many advantages of possibilities (of SMT-solvers) that we did not use so far.

References

1. C. Baier and J.-P. Katoen . Principles of model checking . MIT Press, 2008 .

2. Marcello M. Bersani , Luca Cavallaro, Achille Frigeri, Matteo Pradella, and Matteo Rossi . SMT-based verification of LTL specification with integer constraints and its application to runtime checking of service substitutability . In SEFM , pages 244 - 254 , 2010 .

3. Iury Bessa , Renato B. Abreu , Joao Edgar Chaves Filho, and Lucas Cordeiro . SMT-based bounded model checking of fixed-point digital controllers . CoRR, abs/1403.5172 , 2014 .

4. A. Biere , A. Cimatti , E. Clarke, M. Fujita , and Y. Zhu . Symbolic model checking using SAT procedures instead of BDDs . In Proc. of the ACM=IEEE Design Automation Conference (DAC'99) , pages 317 - 320 , 1999 .

5. A. Biere , A. Cimatti , E. Clarke, and Y. Zhu . Symbolic model checking without BDDs . In Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99) , volume 1579 of LNCS , pages 193 - 207 . Springer-Verlag, 1999 .

6. A. Biere , K. Heljanko , T. A. Junttila , T. Latvala , and V. Schuppan . Linear encodings of bounded LTL model checking . Logical Methods in Computer Science , 2 ( 5 ), 2006 .

7. Armin Biere , Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications . IOS Press, 2009 .

8. R. Bryant . Graph-based algorithms for boolean function manipulation . IEEE Transaction on Computers , 35 ( 8 ): 677 - 691 , 1986 .

9. E. Clarke , E. A. Emerson , and A. P. Sistla . Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach . ACM Transactions on Programming Languages and Systems , 8 ( 2 ): 244 - 263 , 1986 .

10. E. Clarke , O. Grumberg , and D. Peled . Model Checking. MIT Press, 1999 .

11. Lucas Cordeiro and Bernd Fischer . Verifying multi-threaded software using SMT-based context-bounded model checking . In ICSE , pages 331 - 340 , 2011 .

12. Lucas Cordeiro , Bernd Fischer , and João Marques-Silva. SMT-based bounded model checking for embedded ANSI-C software . IEEE Trans. Software Eng. , 38 ( 4 ): 957 - 974 , 2012 .

13. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver . In TACAS , pages 337 - 340 , 2008 .

14. E.W. Dijkstra . Hierarchical ordering of sequential processes . Acta Inf. , 1 : 115 - 138 , 1971 .

15. E. Allen Emerson and Joseph Y. Halpern . Decision procedures and expressiveness in the temporal logic of branching time . J. Comput. Syst. Sci. , 30 ( 1 ): 1 - 24 , 1985 .

16. C.A.R. Hoare . Communicating sequential processes . Prentice Hall , 1985 .

17. Roland Kindermann , Tommi A. Junttila , and Ilkka Niemelä . Beyond lassos: Complete SMTbased bounded model checking for timed automata . In FMOODS/FORTE , pages 84 - 100 , 2012 .

18. T. Latvala , A. Biere , K. Heljanko , and T. A. Junttila . Simple bounded LTL model checking . In A. J. Hu and A. K . Martin, editors, FMCAD , volume 3312 of Lecture Notes in Computer Science, pages 186 - 200 . Springer, 2004 .

19. A. Lomuscio , W. Penczek , and Hongyang Qu . Partial order reduction for model checking interleaved multi-agent systems . In Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS ' 2010 )., pages 659 - 666 . IFAAMAS Press, 2010 .

20. K. McMillan . Symbolic model checking: An approach to the state explosion problem . Kluwer Academic Publishers, 1993 .

21. W. Penczek , B. Woz´na, and A. Zbrzezny . Bounded model checking for the universal fragment of CTL . Fundamenta Informaticae , 51 ( 1-2 ): 135 - 156 , 2002 .

22. Mikhail Ramalho , Mauro Freitas, Felipe Sousa, Hendrio Marques, Lucas Cordeiro, and Bernd Fischer . SMT-based bounded model checking of C++ programs . In ECBS , pages 147 - 156 , 2013 .

23. B. Woz´na. ACTL properties and bounded model checking . Fundamenta Informaticae , 63 ( 1 ): 65 - 87 , 2004 .

24. Liang Xu . SMT-based bounded model checking for real-time systems (short paper) . In QSIC , pages 120 - 125 , 2008 .

25. A. Zbrzezny . Improving the translation from ECTL to SAT . Fundamenta Informaticae, 85 ( 1-4 ): 513 - 531 , 2008 .

26. A. Zbrzezny . A new translation from ECTL to SAT . Fundamenta Informaticae, 120 ( 3- 4 ): 377 - 397 , 2012 .