On Boolean Encodings of Transition Relation for Parallel Compositions of Transition Systems∗ Extended abstract Andrzej Zbrzezny IMCS, Jan Długosz University in Cz˛estochowa, Al. Armii Krajowej 13/15, 42-200 Cz˛estochowa, Poland. a.zbrzezny@ajd.czest.pl Abstract. We present and compare different Boolean encodings of the transi- tion relation for the parallel composition of transition systems, both for the asyn- chronous and the synchronous semantics. We compare the encodings considered by applying them to the SAT-based bounded model checking (BMC) of ECTL∗ properties. We provide experimental results which show that our new encoding for the asynchronous semantics significantly increases the efficiency of the SAT- based BMC. Keywords: transition system, parallel composition, SAT-based bounded model checking, Boolean encoding. 1 Introduction One of the most important practical problems in model checking is the exponential growth of number of states of the transition system, depending on the number of com- ponents of the modelled system. Edmund M. Clarke, co-inventor of the model check- ing, stressed that the problem of overcoming the exponential explosion in the number of states has been one of the most important research questions he was dealing with since the inventing of model checking [1–3]. Reducing the negative impact of the exponential explosion of the state space requires in particular the methods and algorithms to have the highest possible efficiency. The aim of this paper is to present and compare different Boolean encodings of the transition relation for the parallel composition of transition systems, both for the asynchronous and the synchronous semantics. We provide experimental results which show that our new encoding for the asynchronous semantics significantly increases the efficiency of the SAT-based bounded model checking. 2 Preliminaries 2.1 Transition systems Transition systems ([4]) are often used as models to describe the behaviour of systems. They are basically directed graphs where nodes represent states, and edges model transi- ∗ Partly supported by National Science Center under the grant No. 2011/01/B/ST6/05317. On Boolean Encodings of Transition Relation . . . 479 tions, i.e., state changes. A state describes some information about a system at a certain moment of its behaviour. Definition 1. A transition system is a tuple M = (S, Act, −→, I, AP, L), where S is a nonempty finite set of states, Act is a set of actions, I ⊆ S is the set of initial states, −→ ⊆ 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. Transition systems are also called models. σ For convenience, we write s −→ s0 instead of (s, σ, s0 ) ∈ −→. Moreover, we write σ s −→ s0 if s −→ s0 for some σ ∈ Act. From now on we assume that transition systems are finite, i.e. the sets S, Act and AP are finite We also assume that a transition system has no terminal states, i.e. for every s ∈ S there exist s0 ∈ S such that s −→ s0 . The set of all natural numbers is denoted by N N and the set of all positive natural numbers by + . A path in M is an infinite sequence ρ = (s0 , s1 , . . .) of states such that sj −→sj+1 for each j ∈ . N 2.2 Parallel compositions of transition systems Definition 2. Let J be a non-empty, finite set of indices and let {Mj | j ∈ J} be a family of transition systems, i.e. Mj = (Sj , Actj , −→j , Ij , APj , Lj ). Assume that APi ∩ APj = ∅, for i 6= j. Moreover, let J(σ) = {j ∈ J | σ ∈ Actj }, and ε ∈ / Actj for each j ∈ J. 1. The asynchronous parallel composition of the family {Mj | j ∈ J} of tran- sition Y systems is the transition [ systemYM = (S, Act, [7−→, I, AP, L)[such that S = Sj , Act = Actj , I = Ij , AP = APj , L = Lj , and j∈J j∈J j∈J j∈J j∈J 0 σ 0 7−→ is defined as follows: for every s, s ∈ S and every σ ∈ Act: s 7−→ s if and only if the following conditions hold: σ (a) sj −→j s0j for j ∈ J(σ), 0 (b) sj = sj for j ∈ J \ J(σ). 2. The synchronous parallel composition of the family {Mj | j ∈ J} of transition Ysys- tems is the transition system M = (S, Act, −→, I, AP, L) such that S = Sj , j∈J Y Y [ [ Act = (Actj ∪ {ε}), I = Ij , AP = APj , L = Lj , and −→ is j∈J j∈J j∈J j∈J 0 σ 0 defined as follows: for every s, s ∈ S and every σ ∈ Act: s −→ s if and only if the following conditions hold: (a) (∀j ∈ J) (σj = ε =⇒ s0j = sj ), (b) (∃j ∈ J)((σj 6= ε), σj (c) (∀j ∈ J) (σj 6= ε =⇒ sj −→j s0j ), (d) (∀i ∈ J)(σi 6= ε =⇒ (∀j ∈ J(σi )) σj = σi ). 480 A. Zbrzezny S Recall that if |J(σ)| > 1 for an action σ ∈ j∈J Actj , then the action σ is called a shared action; otherwise, i.e. if |J(σ)| = 1, it is called a local action. The actions from Act are called joint actions. In the transition system M being the asynchronous parallel composition of a family of transition systems only one local or shared action may be performed at a given time in a given global state of M. Moreover, a shared action σ has to be performed in all the components Mj , for j ∈ J(σ). In the transition system M being the synchronous parallel composition of a family of transition systems a joint action σ ∈ Act is to be performed by the system at a given time in a given global state of M. It means, that every component Mj of the system can perform an action (also an empty action ε). Notice however, that at least one component has to perform a non-empty action. Moreover, if one of the components performs a shared action σ, then the action σ has to be performed in all the components Mj , for j ∈ J(σ). σ Observe that if s 7−→ s0 then there exists σ ∈ Act such that (s, −→, s0 ). Thus every path of the asynchronous parallel composition of transition systems is also a path of the synchronous parallel composition of transition systems. It follows that every ECTL∗ formula valid in the asynchronous parallel composition of a given family of transition systems is also valid in the synchronous parallel composition of this family. Note that the converse of the implication does not hold. However, let us note that each formula of the form E(Fψ1 ∧ . . . ∧ Fψm ), where ψ1 , . . . , ψm are propositional formulae, valid in the synchronous parallel composition of the given family of transition systems is also valid in the asynchronous parallel composition of this family. 3 Boolean Encodings of States, Actions and Transition Relations We start with describing the Boolean encoding of states, actions and the transition re- lation of a given model by means of propositional formulae, which are built over a set P V of propositional variables plus the constants true and false, with help of the propositional connectives ¬, ∧, ∨ and →. Let {Mj | j ∈ J} be a finite family of transition systems and let M be the parallel composition (either asynchronous or synchronous) of {Mj | j ∈ J}. Since the set Sj of states of each Mj is finite, every element of Sj can be encoded as a bit vector of the length dlog2 |Sj |e. Therefore, each state of Mj can be represented by a valuation of a vector wj (called a symbolic local state) of unique propositional state variables. Then, each state of M can be represented by a valuation of a vector w (called a symbolic global state) of the vectors wj . Similarly, since the set Actj of actions of each Mj is finite, the set Act is also finite, and it follows that every element of Actj can be encoded as a bit vector of the length dlog2 |Act|e. Therefore, each action of Mj can be represented by a valuation of a vector aj (called a symbolic action) of unique propositional action variables. Then, each element of the set Act can be represented by a valuation of a vector a (called a symbolic joint action) of the vectors aj . Let SV = {w1 , w2 , . . .} be a set of propositional state variables and AV = {v1 , v2 , . . .} be a set of propositional action variables. We assume that SV ∩ AV = ∅. On Boolean Encodings of Transition Relation . . . 481 Moreover, let P V = SV ∪ AV and V : P V → {0, 1} be a valuation of propositional N variables (a valuation for short). For every m, r ∈ + each valuation V induces the functions S : SV m → {0, 1}m and A : AV r → {0, 1}r defined as follows: S(wj1 , . . . , wjm ) = (V (wj1 ), . . . , V (wjm )) A(vj1 , . . . , vjr ) = (V (vjr ), . . . , V (vjr )) Our aim is to define either a Boolean formula T (w, w0 ) so that for each valuation V ∈ {0, 1}SV , V satisfies T (w, w0 ) iff S(w) 7−→ S(w0 ) in M or a Boolean for- mula T (w, a, w0 ) so that for each valuation V ∈ {0, 1}P V , V satisfies T (w, a, w0 ) iff S(a) S(w) −→ S(w0 ) in M. 3.1 The standard Boolean encoding of asynchronous parallel composition This encoding is implemented in all the SAT-based verification modules of VerICS [5– 10]. In this encoding we use the following auxiliary propositional formulae: – Hj (wj , wj0 ) for j ∈ J is a Boolean formula defined so that for each valuation V ∈ {0, 1}SV , V satisfies T (wj , wj0 ) iff S(wj0 ) = S(wj ); – Tj,σ (wj , wj0 ) for j ∈ J and σ ∈ Actj is a Boolean formula defined so that for each σ V ∈ {0, 1}SV , V satisfies Tj,σ (wj , wj0 ) iff S(wj ) −→ S(wj0 ) in Mj . Now it is possible to define the Boolean formula T (w, w0 )   _ ^ ^ T (w, w0 ) =  Tj,σ (wj , wj0 ) ∧ Hj (wj , wj0 ) σ∈Act j∈J(σ) j ∈J(σ) / which symbolically encodes the transition relation 7−→ of the asynchronous parallel composition of the family {Mj | j ∈ J}. 3.2 The Boolean encoding of synchronous parallel composition We have recently implemented this encoding in the module BMC4ELTLK of VerICS. This module was used for performing experimental results presented in the article [11], which was recently accepted for publication. However, the encoding in question was not described in [11]. In this encoding we use the following auxiliary propositional formulae: – Hσ (aj ) for j ∈ J and σ ∈ Actj ∪ {ε} is a Boolean formula defined so that for each valuation V ∈ {0, 1}AV , V satisfies Hσ (aj ) iff A(aj ) = σ; – Tj,σ (wj , aj , wj0 ) for j ∈ J and σ ∈ Actj is a Boolean formula defined so that for each valuation V ∈ {0, 1}P V , V satisfies Tj,σ (wj , aj , wj0 ) iff A(aj ) = σ and σ S(wj ) −→ S(wj0 ) in Mj . Now we can define the Boolean formula Tj (wj , aj , wj0 ) _ Tj (wj , aj , wj0 ) = H(wj , wj0 ) ∧ Hε (aj ) ∨ Tj,σ (wj , aj , wj0 )  σ∈Actj 482 A. Zbrzezny which symbolically encodes the transition relation −→j of Mj . Eventually, we define the Boolean formula T (w, a, w0 ) which symbolically encodes the transition relation −→ of the synchronous parallel composition of the family {Mj | j ∈ J}.   ^ ^ ^ ^ T (w, a, w0 ) = Tj (wj , aj , wj0 ) ∧  Hσ (aj ) ∨ Hε (aj ) j∈J σ∈Act j∈J(σ) j∈J(σ) The first subformula of the above conjunction assures that executing a joint action σ consists of executing all the actions that are the components of σ. The second subfor- mula requires that each action σ being a component of a joint action has to be executed in all the components of the synchronous parallel composition in which it appears. 3.3 A new Boolean encoding of asynchronous parallel composition This encoding is inspired by the encoding for the synchronous parallel composition. However, it is not directly derived from the encoding for the synchronous parallel com- position. In the new encoding for asynchronous parallel composition b stands for a vector (of the length dlog2 |Act|e) of propositional action variables so that every ac- tion in Act can be be represented by a valuation of propositional variables in b. In the encoding we use the following auxiliary propositional formula: – Tj,σ (wj , b, wj0 ) for j ∈ J and σ ∈ Actj is a Boolean formula defined so that for each valuation V ∈ {0, 1}P V , V satisfies Tj,σ (wj , b, wj0 ) iff A(b) = σ and σ S(wj ) −→ S(wj0 ) in Mj . Now we can define the Boolean formula Tj (wj , b, wj0 ) which symbolically encodes the transition relation −→j of Mj :   ^ _ Tj (wj , b, wj0 ) = H(wj , wj0 ) ∧ ¬Hσ (b) ∨ Tj,σ (wj , b, wj0 ) σ∈Actj σ∈Actj Intuitively, Tj (wj , b, wj0 ) assures that either A(b) ∈ / Actj and S(wj ) = S(wj0 ) A(b) (i.e. no action is performed in Mj in a given step) or S(wj ) −→ S(wj0 ) in Mj . Eventually, we define the Boolean formula T (w, b, w0 ) which symbolically en- codes the transition relation 7−→ of the synchronous parallel composition of the family {Mj | j ∈ J}: ^ _ T (w, b, w0 ) = Tj (w, b, w0 ) ∧ Hσ (b) j∈J σ∈Act The first subformula of the above conjunction assures that for each action from Act the following condition is satisfied: if this action is to be performed in one of the components of the asynchronous parallel composition, then it has to be performed in all the components in which it appears. The second subformula requires that the vector b represents an action σ ∈ Act. On Boolean Encodings of Transition Relation . . . 483 4 Experimental Results Our experiments were performed on a computer equipped with Intel Xeon 2 GHz pro- cessor, 4GB of RAM and the operating system Ubuntu Linux Server with the kernel 3.5.0. We set the default limits of 1 GB of memory and 1800 seconds. Moreover, we used PicoSAT [12] in version 957 to test the satisfiability of the propositional formulae generated by the module BMC4ECTLS [9]. As the first benchmark we used the generic pipeline paradigm (GPP) introduced in [13]. The GPP consists of the Producer that is able to produce data, the Consumer that is able to receive data, and a chain of n intermediate Nodes that are able to receive, process, and send data. We assume that the following local states ProdReady, Readyj and ConsReady are initial, respectively, for Producer, Nodej and Consumer. The global system is obtained as the parallel composition of the components, which are shown in Figure 4. Fig. 1. The automata for the Sender, the Nodes and the Producer. As the second benchmark we used the train controller system (TC) introduced in [14]. The TC consists of a controller, and n trains (for n > 2). Each train uses its own circular track for travelling in one direction. Eventually, each train has to pass through a tunnel, but because there is only one track in the tunnel, the trains arriving from each direction cannot use it simultaneously. There are signals on both sides of the tunnel, which can be either red or green. Each train notifies the controller when it request entry to the tunnel or when it leave the tunnel. The controller controls the colour of the displayed signal. The local state Awayj is initial for Trainj , and the local state Green is initial for Controller. The global system is obtained as the parallel composition of the components, which are shown in Figure 4. As the third benchmark we used the dining philosophers problem [15, 16]. We have modelled this problem by means of a parallel composition of 2n + 1 transition systems. The global system consists of n transition system each of which models a philoso- pher, together with n transition systems each of which models a fork, together with one transition system which models the lackey. The latter transition system is used to 484 A. Zbrzezny Fig. 2. The automata for the Trains and the Controller. 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 3. Fig. 3. The automata for the j-th Philosopher, the j-th Fork and the Lackey. Let I(w) be a propositional formula such that for each valuation V ∈ {0, 1}SV , V satisfies I(w) iff S(w) is an initial state of the model. In order to compare experimental results for the three Boolean encodings of transition relation we have tested first (on a symbolic path of the length 1) the ECTL∗ formula ϕ0 = E(true) that is valid in the models considered. The translation of the formula ϕ0 results in the propositional formula: – I(w) ∧ T (w, w0 ) for the old encoding of the asynchronous parallel composition, On Boolean Encodings of Transition Relation . . . 485 – I(w) ∧ T (w, a, w0 ) for the encoding of the synchronous parallel composition, – I(w) ∧ T (w, b, w0 ) for the new encoding of the asynchronous parallel composi- tion. As we expected, the experimental results for the formula ϕ0 (Table 1) show that the new encoding of the transition relation for the asynchronous parallel composition significantly influence the size (i.e. the number of clauses) of the resulting propositional formulae: for the GPP and 1800 nodes the number of clauses for the new encoding is 56 times less than for the old one; for the TC and 2800 trains the number of clauses for the new encoding is 25 times less than for the old one; for the DP and 1250 philosophers the number of clauses for the new encoding is 26 times less than for the old one. Moreover, the results from Table 1 show that the encoding of the transition rela- tion for the synchronous parallel composition results in propositional formulae that are shorter than formulae for the old encoding and significantly longer than formulae for the new encoding. Encoding of the (? Max) number Number of Number of transition relation of components variables clauses Generic Pipeline Paradigm ? New 105000 3727243 10131599 ? Sync 28000 3689932 8130256 New 28000 989629 2688769 ? Old 1800 3283218 9833442 Sync 1800 190792 426140 New 1800 63577 172637 Train Controller ? New 87000 3829207 10617501 ? Sync 29000 4262182 9800524 New 29000 1320132 3670282 ? Old 2800 3991404 11949004 Sync 2800 346605 809243 New 2800 131235 365609 Dining Philosophers ? New 2400 288650 805804 ? Sync 2350 812694 1994856 New 2350 283150 790554 ? Old 1150 3374711 10137875 Sync 1150 376831 927590 New 1150 138855 387680 Table 1. Results for the formula ϕ0 generated by the SAT-based BMC translations Although, in our opinion, testing the formula ϕ0 for different systems allows to draw reliable conclusions about the presented encodings, we have also tested some for- 486 A. Zbrzezny Clauses for GPP, Formula 0 Clauses for TC, Formula 0 Clauses for DP, Formula 0 40000 25000 100000 90000 35000 20000 80000 30000 70000 Number of clauses Number of clauses Number of clauses 25000 15000 60000 20000 50000 10000 40000 15000 30000 10000 5000 20000 5000 OLD-ASYNC OLD-ASYNC OLD-ASYNC NEW-ASYNC NEW-ASYNC 10000 NEW-ASYNC SYNC SYNC SYNC 0 0 0 10 20 30 40 50 60 70 80 90 100 10 20 30 40 50 60 70 80 90 100 10 20 30 40 50 60 70 80 90 100 Number of nodes Number of nodes Number of nodes Fig. 4. Number of clauses for the formula ϕ0 . mulae each of which expresses either a reachability or an extended reachability property (i.e. a formula of the form E(Fψ1 ∧ . . . ∧ Fψm ), where ψ1 , . . . , ψm are propositional formulae). For all the tested systems we assume that for every local state s, L(s) = {s}. For the GPP we have tested the following two formulae: – ϕ1 (n) = EF(Received) – ϕ2 (n) = EF(Send1 ∧ . . . ∧ Sendn ) Let us note that for the asynchronous parallel composition the witness for the for- mula ϕ1 (n) has the length 2n + 2, and the witness for the formula ϕ2 (n) has the length n2 + 2n, whereas for the synchronous parallel composition the witness for the formula ϕ1 (n) has the length 2n + 2, and the witness for the formula ϕ2 (n) has the length 3n. The experimental results for the tested formulae ϕ1 and ϕ2 , are presented at the pictures 9 and 10 respectively. Total memory for GPP, Formula 1 Total time for GPP, Formula 1 1000 3000 2500 100 2000 Memory in MB. Time in sec. 1500 10 1000 OLD-ASYNC 500 OLD-ASYNC NEW-ASYNC NEW-ASYNC SYNC SYNC 1 0 10 100 10 20 30 40 50 60 70 80 Number of nodes Number of trains Fig. 5. Experimental results for GPP and the formula ϕ1 . Total memory for GPP, Formula 2 Total time for GPP, Formula 2 100 1000 900 800 700 10 Memory in MB. Time in sec. 600 500 400 1 300 200 OLD-ASYNC OLD-ASYNC NEW-ASYNC 100 NEW-ASYNC SYNC SYNC 0.1 0 10 100 5 10 15 20 25 30 35 40 Number of nodes Number of trains Fig. 6. Experimental results for GPP and the formula ϕ2 . On Boolean Encodings of Transition Relation . . . 487 For the TC we have tested the following two formulae: – ϕ3 (n) = E(F(T unnel1 ) ∧ F(T unneln ) – ϕ4 (n) = E(F(T unnel1 ) ∧ . . . ∧ F(T unneln )) Let us note that for the asynchronous parallel composition the witness for the for- mula ϕ3 (n) has the length 5, and the witness for the formula ϕ4 (n) has the length 3(n − 1) + 2, whereas for the synchronous parallel composition the witness for the formula ϕ4 (n) has the length 4, and the witness for the formula ϕ4 (n) has the length 2n. The experimental results for the tested formulae ϕ3 and ϕ4 , are presented at the pictures 7 and 8 respectively. Total memory for TC, Formula 1 Total time for FTC, Formula 1 1200 1600 1400 1000 1200 800 Memory in MB. 1000 Time in sec. 600 800 600 400 400 200 OLD-ASYNC OLD-ASYNC NEW-ASYNC 200 NEW-ASYNC SYNC SYNC 0 0 0 2000 4000 6000 8000 10000 12000 14000 16000 18000 20000 0 2000 4000 6000 8000 10000 12000 14000 16000 18000 20000 Number of trains Number of trains Fig. 7. Experimental results for TC and the formula ϕ1 . Total memory for TC, Formula 2 Total time for FTC, Formula 2 30 1400 25 1200 1000 20 Memory in MB. Time in sec. 800 15 600 10 400 5 OLD-ASYNC 200 OLD-ASYNC NEW-ASYNC NEW-ASYNC SYNC SYNC 0 0 2 3 4 5 6 7 8 9 2 3 4 5 6 7 8 9 Number of trains Number of trains Fig. 8. Experimental results for TC and the formula ϕ2 . For the DP we have tested the following two formulae: – ϕ5 (n) = E(F(Eat0 ) ∧ F(Eatn−1 ) – ϕ6 (n) = E(F(Eat0 ) ∧ . . . ∧ F(Eatn−1 )) Let us note that for the asynchronous parallel composition the witness for the for- mula ϕ5 (n) has the length 7, and the witness for the formula ϕ6 (n) has the length 4n + 1, whereas for the synchronous parallel composition the witness for the formula ϕ5 (n) has the length 6, and the witness for the formula ϕ6 (n) has the length n + 3 for n > 6 and 9 otherwise. The experimental results for the tested formulae ϕ5 and ϕ6 , are presented at the pictures 7 and 8 respectively. 488 A. Zbrzezny Total memory for DP, Formula 1 Total time for DP, Formula 1 10000 10000 1000 1000 100 Memory in MB. Time in sec. 100 10 1 10 OLD-ASYNC 0.1 OLD-ASYNC NEW-ASYNC NEW-ASYNC SYNC SYNC 1 0.01 10 100 1000 10000 10 100 1000 10000 Number of Philosophers Number of Philosophers Fig. 9. Experimental results for DP and the formula ϕ1 . Total memory for DP, Formula 2 Total time for DP, Formula 2 100 10000 1000 Memory in MB. Time in sec. 100 10 10 1 OLD-ASYNC OLD-ASYNC NEW-ASYNC NEW-ASYNC SYNC SYNC 1 0.1 10 10 Number of Philosophers Number of Philosophers Fig. 10. Experimental results DP and for the formula ϕ2 . 5 Conclusions and Future Work The experiments showed that our new Boolean encoding for asynchronous parallel composition is the most effective one while comparing to the other two considered. Moreover, the encoding of the transition relation for the synchronous parallel composi- tion is nearly as effective as the new encoding for asynchronous parallel composition. The standard Boolean encoding used so far in the SAT-based verification modules of VerICS turned out to be the worst one. This is clearly seen for the formula ϕ0 (n) that is verified on the path of the length 1. The length equal to 1 assures that the experimental results for the formula ϕ0 (n) are affected by the Boolean encoding of the transition relation only. The above conclusions, which are based on the experimental results presented in Section 4, are also supported by the fact that the length of the resulting Boolean formula for standard Boolean encoding for asynchronous parallel composition is O(|Act| · n), whereas the length of the resulting Boolean formula for our new Boolean encoding for asynchronous parallel composition is O(|Act| · log |Act|). Let us note that the experimental results for the formulae ϕj (n), for j = 1, . . . , 6, are affected not only by the Boolean encoding of the transition relation but also by the encoding of the translation of ECTL∗ formulae to SAT. Nevertheless, the experimen- tal results for these formulae confirm that the new encoding for asynchronous seman- tics significantly increases the efficiency of the SAT-based bounded model checking. It means that the effectiveness of the most of the SAT-based verification modules of VerICS could be significantly improved. Moreover, the experimental results for the formulae ϕ2 (n), ϕ4 (n) and ϕ6 (n) show that for formulae for which the length of the witness is significantly shorter for the On Boolean Encodings of Transition Relation . . . 489 synchronous semantics, it is worth to apply the synchronous semantics instead of the asynchronous one. We strongly believe that the choice of a SAT-solver will not change our conclusions. Nevertheless, in the nearest future we are going to repeat all the experiments for the other SAT-solvers. References 1. Clarke, E.M.: The birth of model checking. In: 25 Years of Model Checking - History, Achievements, Perspectives. Volume 5000 of Lecture Notes in Computer Science., Springer (2008) 1–26 2. Clarke, E.M.: Model checking - my 27-year quest to overcome the state explosion prob- lem. In: Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. Volume 5330 of Lecture Notes in Computer Science., Springer (2008) 182 3. Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and de- bugging. Communications of the ACM 52(11) (2009) 74–84 4. Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008) 5. Zbrzezny, A.: Improvements in SAT-based reachability analysis for timed automata. Funda- menta Informaticae 60(1-4) (2004) 417–434 6. Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal con- straints. Fundamenta Informaticae 67(1-3) (2005) 303–322 7. Kacprzak, M., Nabiałek, W., Niewiadomski, A., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1-4) (2008) 313–328 8. Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1-4) (2008) 513–531 9. Zbrzezny, A.: A new translation from ECTL∗ to SAT. Fundamenta Informaticae 120(3-4) (2012) 377–397 10. Zbrzezny, A., Półrola, A.: SAT-based reachability checking for timed automata with discrete data. Fundamenta Informaticae 79(3-4) (2007) 579–593 11. M˛eski, A., Penczek, W., Szreter, M., Woźna-Szcześniak, B., Zbrzezny, A.: BDD- versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: Algorithms and their performance. Autonomous Agents and Multi-Agent Systems (2013) to appear. 12. Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 4 (2008) 75–97 13. Peled, D.: All from one, one for all: On model checking using representatives. In: Proc. of the 5th Int. Conf. on Computer Aided Verification (CAV’93). Volume 697 of LNCS., Springer-Verlag (1993) 409–423 14. Hoek, W., Wooldridge, M.: Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica 75(1) (2003) 125–157 15. Dijkstra, E.: Hierarchical ordering of sequential processes. Acta Inf. 1 (1971) 115–138 16. Hoare, C.: Communicating sequential processes. Prentice Hall (1985)