On Boolean Encodings of Transition Relation for Parallel Compositions of Transition Systems

Abstract

We 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 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 SATbased BMC.

Keywords

• transition system
• parallel composition
• SAT-based bounded model checking
• Boolean encoding

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 components of the modelled system. Edmund M. Clarke, co-inventor of the model checking, 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.1

Preliminaries

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 transitions, 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) 2 !. Moreover, we write s ! s0 if s ! s0 for some 2 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 2 S there exist s0 2 S such that s ! s0. The set of all natural numbers is denoted by N and the set of all positive natural numbers by N+. A path in M is an infinite sequence = (s0; s1; : : :) of states such that sj !sj+1 for each j 2 N. 2.2

Parallel compositions of transition systems Definition 2. Let J be a non-empty, finite set of indices and let fMj j j 2 J g 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 ( ) = fj 2 J j 2 Actj g, and " 2= Actj for each j 2 J . 1. The asynchronous parallel composition of the family fMj j j 2 J g of transition systems is the transition system M = (S; Act; 7 !; I ; AP; L) such that S = Y Sj , Act = [ Actj , I = Y Ij , AP = [ APj , L = [ Lj , and j2J j2J j2J j2J j2J 7 ! is defined as follows: for every s; s0 2 S and every 2 Act: s 7 ! s0 if and only if the following conditions hold: (a) sj !j s0j for j 2 J ( ), (b) s0j = sj for j 2 J n J ( ). 2. The synchronous parallel composition of the family fMj j j 2 J g of transition systems is the transition system M = (S; Act; !; I ; AP; L) such that S = Y Sj , Act =

Y(Actj [ f"g), I = j2J

j2J j2J defined as follows: for every s; s0 2 S and every the following conditions hold: (a) (8j 2 J ) ( j = " =) s0j = sj ), (b) (9j 2 J )(( j 6= "), (c) (8j 2 J ) ( j 6= " =) sj !jj s0j ), (d) (8i 2 J )( i 6= " =) (8j 2 J ( i)) j = i).

Y Ij , AP = [ APj , L = [ Lj , and j2J

! is j2J 2 Act: s ! s0 if and only if

Recall that if jJ ( )j > 1 for an action 2 Sj2J Actj , then the action is called a shared action; otherwise, i.e. if jJ ( )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 2 J ( ).

In the transition system M being the synchronous parallel composition of a family of transition systems a joint action 2 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 2 J ( ).

Observe that if s 7 ! s0 then there exists 2 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 relation 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 fMj j j 2 J g be a finite family of transition systems and let M be the parallel composition (either asynchronous or synchronous) of fMj j j 2 J g. 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 jSj je. 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 jActje. 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 = fw1; w2; : : :g be a set of propositional state variables and AV = fv1; v2; : : :g be a set of propositional action variables. We assume that SV \ AV = ;. Moreover, let P V = SV [ AV and V : P V ! f0; 1g be a valuation of propositional variables (a valuation for short). For every m; r 2 N+ each valuation V induces the functions S : SV m ! f0; 1gm and A : AV r ! f0; 1gr 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 2 f0; 1gSV , V satisfies T (w; w0) iff S(w) 7 ! S(w0) in M or a Boolean formula T (w; a; w0) so that for each valuation V 2 f0; 1gP V , V satisfies T (w; a; w0) iff S(w) S(!a) 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 2 J is a Boolean formula defined so that for each valuation

V 2 f0; 1gSV , V satisfies T (wj ; wj0 ) iff S(wj0 ) = S(wj ); – Tj; (wj ; wj0 ) for j 2 J and 2 Actj is a Boolean formula defined so that for each V 2 f0; 1gSV , V satisfies Tj; (wj ; wj0 ) iff S(wj ) j2J( )

^ j2=J( ) 1 T (w; w0) =

Tj; (wj ; wj0 ) ^

Hj (wj ; wj0 )A which symbolically encodes the transition relation 7 ! of the asynchronous parallel composition of the family fMj j j 2 J g. 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 2 J and 2 Actj [ f"g is a Boolean formula defined so that for each valuation V 2 f0; 1gAV , V satisfies H (aj ) iff A(aj ) = ; – Tj; (wj ; aj ; wj0 ) for j 2 J and 2 Actj is a Boolean formula defined so that for each valuation V 2 f0; 1gP V , V satisfies Tj; (wj ; aj ; wj0 ) iff A(aj ) = and

Now we can define the Boolean formula Tj (wj ; aj ; wj0 )

Tj (wj ; aj ; wj0 ) =

H(wj ; wj0 ) ^ H"(aj ) _

Tj; (wj ; aj ; wj0 ) _ 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 fMj j j 2 J g. T (w; a; w0) = ^ Tj (wj ; aj ; wj0 ) ^ j2J ^ 2Act 0

^ j2J( )

H (aj ) _

^

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 subformula 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. 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 composition. In the new encoding for asynchronous parallel composition b stands for a vector (of the length dlog2 jActje) of propositional action variables so that every action 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 2 J and 2 Actj is a Boolean formula defined so that for each valuation V 2 f0; 1gP V , V satisfies Tj; (wj ; b; wj0 ) iff A(b) = and :H (b)A _

Tj; (wj ; b; wj0 )

Intuitively, Tj (wj ; b; wj0 ) assures that either A(b) 2= Actj and S(wj ) = S(wj0 ) (i.e. no action is performed in Mj in a given step) or S(wj ) A(!b) S(wj0 ) in Mj .

Eventually, we define the Boolean formula T (w; b; w0) which symbolically encodes the transition relation 7 ! of the synchronous parallel composition of the family fMj j j 2 J g:

T (w; b; w0) = ^ Tj (w; b; w0) ^ j2J _ 2Act

H (b)

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 2 Act.

Experimental Results

Our experiments were performed on a computer equipped with Intel Xeon 2 GHz processor, 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.

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 philosopher, 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 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.

Let I(w) be a propositional formula such that for each valuation V 2 f0; 1gSV , 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, – 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 composition.

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 relation 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

?105000 3727243 New Sync New Old Sync New New Sync New Old Sync New New Sync New Old Sync New 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

ClausesforGPP,Formula0 40000 35000 30000 lrsseubeuaNm 11250550000000000000 10 20 30 40 Numbe5r0ofnodes60 70 NOELW8D0--AASSSYYYNNNCCC90 100 fco 20000

ClausesforTC,Formula0 25000 20000 lfrscseobeuam 1105000000 uN 5000 NOELWD--AASSYYNNCC 0 10 20 30 40 Numbe5r0ofnodes60 70 80 SYNC90 100

ClausesforDP,Formula0 100000 90000 80000 s 70000 lfrcsaeeoubm 564000000000000 uN 30000 12000000000 10 20 30 40Numbe5r0ofnodes60 70 NOELW8D0--AASSSYYYNNNCCC90 100 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) = f g 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 formula '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 .BM 100 iryon eMm 10

1 100 .BM 10 iryon eMm 1 0.1 1N0umber of nodes 100 5 10 15

Number of trains 25 20 Fig. 6. Experimental results for GPP and the formula '2.

OLD-ASYNC NEW-ASYNC

SYNC 60 70 30

OLD-ASYNC NEW-ASYNC

SYNC 35 80 40 OLD-ASYNC NEW-ASYNC

SYNC OLD-ASYNC NEW-ASYNC

SYNC 3000 2500 .c 2000 e isn 1500 e iTm 1000 500 0 1000 900 800 700 .c 600 se in 500 e iTm 430000 200 100 0 1N0umber of nodes 100 10 20 30 Number of trains 50 40

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 formula '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 1200 1000 .BM 800 ryn 600 i o eMm 400 200 NOELWD--AASSYYNNCC 0 0 2000 4000 6000 8000Numb1e0r0o0f0train1s2000 14000 16000SYN1C8000 20000

Total time for FTC, Formula 1 1600 1400 1200 .c 1000 e isn 800 e iTm 600

2400000 0 2000 4000 6000 8000Numb1e0r0o0f0train1s2000 14000 NO1EL6WD0--0AA0SSSYYYNNN1CCC8000 20000

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 formula '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.

30 25 .BM 20 iryn 15 o m eM 10 5 0 2

Total memory for DP, Formula 1 Total time for DP, Formula 1 10000 .BM 1000 ryn 100 i eo m M 10

1 100 .

BM iryn 10 oe m M 1

OLD-ASYNC NEW-ASYNC

SYNC 1000 10

100 Number of Philosophers 10000 10

100 Number of Philosophers

OLD-ASYNC NEW-ASYNC

SYNC 1000 10000 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 composition 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(jActj n), whereas the length of the resulting Boolean formula for our new Boolean encoding for asynchronous parallel composition is O(jActj log jActj).

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 experimental results for these formulae confirm that the new encoding for asynchronous semantics 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 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 problem . 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 debugging . 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 . Fundamenta Informaticae 60 ( 1-4 ) ( 2004 ) 417 - 434

6. Zbrzezny , A. : SAT-based reachability checking for timed automata with diagonal constraints . Fundamenta Informaticae 67 ( 1-3 ) ( 2005 ) 303 - 322

7. Kacprzak , M. , Nabiałek , W. , Niewiadomski , A. , Penczek , W. , Półrola , A. , Szreter , M. , Woz´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. Me˛ski, A. , Penczek , W. , Szreter , M. , Woz´ na-Szczes´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 )