=Paper=
{{Paper
|id=None
|storemode=property
|title=On Boolean Encodings of Transition Relation for Parallel Compositions of Transition
Systems
|pdfUrl=https://ceur-ws.org/Vol-1032/paper-42.pdf
|volume=Vol-1032
|dblpUrl=https://dblp.org/rec/conf/csp/Zbrzezny13
}}
==On Boolean Encodings of Transition Relation for Parallel Compositions of Transition
Systems==
https://ceur-ws.org/Vol-1032/paper-42.pdf
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)