State Distribution Policy for  Distributed Model Checking of Actor Models


Electronic Communications of the EASST
Volume 72 (2015)

Proceedings of the
15th International Workshop on

Automated Verification of Critical Systems (AVoCS 2015)

State Distribution Policy for
Distributed Model Checking of Actor Models

Ehsan Khamespanah ,, Marjan Sirjani , MohammadReza Mousavi , Zeynab Sabahi Kaviani ,
and MohamadReza Razzazi

15 pages

Guest Editors: Gudmund Grov, Andrew Ireland
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

State Distribution Policy for
Distributed Model Checking of Actor Models

Ehsan Khamespanah 1,2, Marjan Sirjani 2, MohammadReza Mousavi 3, Zeynab
Sabahi Kaviani 1, and MohamadReza Razzazi 4

1 e.khamespanah@ut.ac.ir ,z.sabahi@ut.ac.ir
University of Tehran, School of Electrical and Computer Engineering

2 ehsan13@ru.is, marjan@ru.is
Reykjavik University, School of Computer Science

3 m.r.mousavi@hh.se
Halmstad University, Centre for Research on Embedded Systems

4 Razzazi@aut.ac.ir
Amirkabir University of Technology, School of Computer Eng. and Information Tech.

Abstract: Model checking temporal properties is often reduced to finding accept-
ing cycles in Büchi automata. A key ingredient for an effective distributed model
checking technique is a distribution policy that does not split the potential accepting
cycles of the corresponding automaton among several nodes. In this paper, we intro-
duce a distribution policy to reduce the number of split cycles. This policy is based
on the call dependency graph, obtained from the message passing skeleton of the
model. We prove theoretical results about the correspondence between the cycles of
the call dependency graph and the cycles of the concrete state space and provide em-
pirical data obtained from applying our distribution policy in state space generation
and reachability analysis. We take Rebeca, an imperative interpretation of actors, as
our modeling language and implement the introduced policy in its distributed state
space generator. Our technique can be applied to other message-driven actor-based
models where concurrent objects or services are units of concurrency.

Keywords: Distributed Model Checking, State Distribution Policy, Concurrent Ob-
jects, Actors, Rebeca

1 Introduction

Providing quality guarantees despite the ever-increasing complexity of computer systems has
been and remains a grand challenge. Using formal methods, in general, and model checking
[CES86] in particular, has been advocated as a response to this grand challenge. Model-checking
tools explore the state space of the system exhaustively to make sure that a given property holds
in all possible execution of a system. A major limiting factor in applying model checkers to
practical systems is the huge amount of space and time required to store and explore the state
space. Generating the state space of large-scale practical systems undoubtedly results in state
spaces that cannot fit in the memory of a single computer.

Besides the traditional model-checking reduction techniques, distributed LTL model checking
[GMS13, BHR13, VVFB11, BBC05, BBS01, BC06, BCMS06] is a well-known technique to

1 / 15 Volume 72 (2015)

mailto:e.khamespanah@ut.ac.ir ,z.sabahi@ut.ac.ir
mailto:ehsan13@ru.is, marjan@ru.is
mailto:m.r.mousavi@hh.se
mailto:Razzazi@aut.ac.ir


State Distribution Policy

deal with huge state spaces. In distributed LTL model checking the state space is partitioned into
some slices and each slice is assigned to a node. Theoretically, dividing cycle detection in a state
space among a number of nodes increases the efficiency of model checking; however, unlike the
sequential and the shared-memory parallel algorithms, the efficiency of these algorithms depends
on the communication costs [OPE05]. The communication cost directly relates to the distribution
policy of states among nodes, as detecting accepting cycles that span over many different nodes
requires communication. Another, more fine-grained, representative of communication cost is
the number of split transitions; a split transition is a transition between two states, where the
hosts of source and destination states are different nodes.

In the present work, we tackle the state distribution policy problem in the state space gen-
eration of actor models [Hew72]. We introduce a new state distribution policy based on the
the so-called Call Dependency Graph (CDG) of actor models. A CDG represents the abstract
causality relation among messages of actors (Section 2). Our abstraction is akin to the dynamic
representation of actor’s event activation causality proposed by Clinger [Cli81].

The most primitive and widely used distribution policy is random state distribution [GMS13,
BHR13, VVFB11, BCMS06]. Random state distribution policy distributes states among nodes
based on their hash values. Random distribution policy guarantees load balancing. However, it
is not an effective technique as cycles are scattered over many different nodes. In [BBC05], state
distribution is performed based on the Büchi automata of the properties. LTL model checkers
find accepting cycles in the synchronous product of the state space and the Büchi automata of
LTL specifications. Therefore, distributing states based on the strongly connected components
of the property Büchi automata avoids creation of split cycles in the state space. This way, there
is no need for communication among nodes for detecting accepting cycles. In practice, the corre-
sponding Büchi automata of LTL properties do not have many strongly connected components.
Hence, this approach does not work efficiently in most practical cases.

In [OPE05], another state space distribution policy is suggested to improve the locality of cy-
cles.This policy is based on the static analysis of an abstracted model and detects may or must
transition relations among states [LT88]. Based on this analysis, if two states have a must rela-
tion, they should be stored in a same node. We use a similar idea in our state distribution policy
and show that using the CDG improves the locality of cycles by reducing the split transitions
in the state space. In other words, we find the must relations among the states of actor models
using the CDG. Our technique is applicable to other service-oriented models where the unit of
concurrency can be modeled as an autonomous active object and message passing is the only
way of communication. To illustrate the applicability of our method, we implement it in the
distributed model checker of Rebeca, which is an actor-based language for modeling and model
checking of reactive systems (Section 3). The experimental results of using CDG illustrate that
the number of split transitions is reduced significantly by up to 50% (Section 4). We also discuss
possible extensions of our work and possible application domains for it (Section 5).

In a nutshell, the contributions of this paper are as follows:

− Introducing the notion of call dependency graph (CDG) for actor models as an abstract
representation for message passing causality (Section 2),

− presenting the relation between the cycles in the CDG and the cycles in the state space of
a model (Section 2),

Proc. AVoCS 2015 2 / 15



ECEASST

− adapting the notion of CDG in order to define a state distribution policy (Section 3),

− implementing the proposed techniques in a distributed model checking tool (Section 4),
and

− providing experimental results and measuring the efficiency of our technique by means of
a number of case studies (Section 4).

2 Call Dependency Graphs of Actor Models

The actor model [Hew72, AMST97] is a well-established paradigm for modeling distributed and
asynchronous systems. In this model, actors encapsulate the concept of concurrent behavior.
Each actor provides services that can be requested by other actors through sending messages
to the provider. Messages are put in the message buffer of the receiver; the receiver takes the
message and executes the requested service, and consequently, may send some messages to
other actors. The source code of a simple actor model is shown in Figure 1. This model consists
of two actors ac1 and ac2, each of which provides two services. To start the execution of
the model, some messages must be put in the message buffer of the actors (i.e., initially sent
messages); this is specified in the main block (line 24). Sending a message is denoted by
“actor name.service name()” (line 3).

We illustrate our approach using a Simple Actor Modeling language, called SAM, which con-
tains the key features of the actor model. Below, we briefly introduce SAM, which is inspired by
the earlier actor models, e.g., by Agha et al. in [AMST97] and by Sirjani et al. in [SMSB04].

Definition 1 (An Actor Model) An actor in SAM is a member of type Actor = ID×P(Vars)×
P(mtds), where P(·) denotes power set and:

− ID is the set of actor identifiers,

1 Actor ac1 {
2 service msg1() {
3 ac1.msg2();
4 ac2.msg3();
5 }
6 service msg2() {
7 ac1.msg1();
8 ac2.msg4();
9 }

10 }
11 Actor ac2 {
12 int sv = 1;
13 service msg3() {

14 ac1.msg1();
15 }
16 service msg4() {
17 if (sv == 1)
18 sv = 4;
19 else
20 sv = 3;
21 }
22 }
23
24 main {
25 ac1.msg1();
26 }

Figure 1: An example of a simple actor model.

3 / 15 Volume 72 (2015)



State Distribution Policy

− Vars is the set of variable names, and

− Mtds is the set of method declarations.

Here, the members of Mtds are tuples (m, p,s)∈ MName×Vars∗×Statement∗, where m is the
name of the message which must be served by this method, p is the lists of message parameters,
and s ∈ Statement∗ is the sequence of statements compromising the method’s body.

The set of statements in SAM is limited to a number of preliminary statements defined below.

Definition 2 (SAM Statements) The set of SAM statements is defined as Statement = Assignment∪
Condition∪Send where:

− Assignment = Vars×Expr is the set of assignment statements. In Figure 1, we use var =
ex pr to denote the assignment statement (var,expr).

− Condition = BExpr×Statement∗×Statement∗ is the set of conditional statements. In Fig-
ure 1, we use if (bex pr) σ else σ ′ to denote the conditional statement (bex pr,σ,σ ′).

− Send = (ID∪{self})×MName×Expr∗ is the set of send statements. In Figure 1, we use
a.m(e) to denote the send statement (a,m,e).

In the aforementioned items, Expr denotes the set of integer expressions defined using usual
arithmetic operators (with no side effects). BExpr denotes the set of Boolean expressions defined
using usual relational and logical operators. We dispense with further details of the syntax in this
definition.

Based on Definition 1 and Definition 2, a SAM model is specified by P(Actor)∪Send∗ where
the Send∗ term addresses the send statements of the main block (i.e. the initially sent messages).
Note that since there may be more than one initial message for an actor, the send statements are
ordered in a sequence not just a set of statements.

We define below the operational semantics of SAM in terms of a Labeled Transition System
(LTS). In order to do this, the following assumptions and notations are required. We assume that
the only possible communication mechanism among actors is asynchronous message passing.
The type of messages is defined as Msgs = ID×MName×ID×(Vars → Vals), where for a mes-
sage (a1,m,a2,arg) ∈ Msgs, a1 is the name of the sending actor, a2 is the name of the receiving
actor, m is the name of the message, and arg is a function for mapping argument names to their
values. For the sake of simplicity and without loss of generality, we assume that the messages do
not have arguments and are left out of the message signature in the remainder of this paper. The
other assumption is that the received messages of an actor are stored in a FIFO mailbox. Hence,
the mailbox of an actor is denoted by a sequence of messages, i.e., a member of Msgs∗.

Definition 3 (SAM Operational Semantics) For a given actor model AC, its labeled transition
system LTS(AC), is defined as a tuple (S,s0,Act,→), where:

− S is the set of the global states of a SAM model defined as a set of functions in form of
S ={s | s : ID →(Vars → Vals)×Msgs∗}. Here, s ∈ S maps an actors identifier to the local
state of the actor, i.e., the values of its state variables and its mailbox content,

Proc. AVoCS 2015 4 / 15



ECEASST

− s0 ∈ S is the initial state,

− Act = Msgs is the set of action labels (sent messages).

− →⊆ S×Act×S is the set of transitions, defined by the coarse-grained interleaving of actor
message executions, by removing a message from their mailboxes, sending the messages
in the body of the corresponding method and finally updating the global state (as the result
of assignment statements). By coarse-grained interleaving, we mean that the sequence of
messages in the body of a method are sent in an atomic sequence.

Using the operational semantics of actor models, Clinger’s event diagram of actor models can
be created. Clinger’s event diagram comprise vertices (called dots) for each event, and edges
(called arrows) that represent the activation relation of two events. Using dots and arrows, the
runtime characteristics of an actor system is presented by the graph of activation relation of
events. Clinger’s event diagram is typically drawn using parallel vertical swim-lanes for actors,
where the dots are placed respecting their sequential execution order. Figure 2(a) presents the
Clingers’ event diagram of the example actor model of Figure 1. As shown in the actor model,
message msg1 is the first executing message (as it is put in the queue of ac1 in the main block)
which results in sending msg2 and msg3; hence, there is one dot with label msg1, which is
connected by arrows to two other dots with labels msg2 and msg3.

Clinger’s event diagrams can be seen as detailed representations of CDG. Intuitively, a CDG
represents the possible activation relations of events derived from a static analysis of the model.
Hence, a CDG over-approximates the event activations in the Clinger’s event diagram. The
activation relation of events in a CDG can be extracted from the source codes of actor models. For
example, as shown in Figure 2(a), the static activation relation between msg1 and two messages
msg2 and msg3 can be extracted from the source code of Figure 1. In addition, the execution of
msg3 results in the activation of msg1, hence, the loop back to the topmost state of the CDG in
Figure 2(b).

Definition 4 (Sent Messages) For a given message msg = (a1,m,a2) ∈ Msgs, the set of mes-
sages that can be possibly sent by a2 to arbitrary actors as a result of serving m (which is in turn
sent by a1) is denoted by snt(msg).
The set snt(msg) is statically determined by an evaluation of an actor model. For a given message
msg = (a1,m,a2) assume that (m, p,s) is its corresponding method. The members of snt(msg)
is computed by the analysis of the statements of the actor s, as depicted below for a given SAM
model sam = actors∪snt msgs.

snt(msg) =
{

msg′ ∈ Msgs|
msg = (a1,m,a2)∧msg′ = (a2,m′,ai)∧(a2,vars,mtds)∈ actors →
∃stmts ∈ P(Statements)·(m,arg,stmts)∈ mtds∧(ai,m′, /0)∈ stmts
}

Definition 5 (Call Dependency Graph (CDG) ) Given an actor model AC with LTS(AC) =
(S,s0,Act,→), its CDG is a finite labeled transition system CDG(AC) = (V,v0,Act,↪→), where

5 / 15 Volume 72 (2015)



State Distribution Policy

 

𝑎𝑐1. 𝑚𝑠𝑔1 𝑎𝑐2. 𝑚𝑠𝑔3 

𝑎𝑐1. 𝑚𝑠𝑔2 

𝑎𝑐2. 𝑚𝑠𝑔4 

𝑎𝑐1. 𝑚𝑠𝑔1 

𝑚𝑠𝑔1 

𝑚𝑠𝑔2 

𝑚𝑠𝑔1 

𝑚𝑠𝑔3 

𝑚𝑠𝑔4 

𝑎𝑐1 𝑎𝑐2 

𝑚𝑠𝑔1 

(a) Clinger event diagram of an
example actor model  

𝑎𝑐1. 𝑚𝑠𝑔1 𝑎𝑐2. 𝑚𝑠𝑔3 

𝑎𝑐1. 𝑚𝑠𝑔2 

𝑎𝑐2. 𝑚𝑠𝑔4 

𝑎𝑐1. 𝑚𝑠𝑔1 

𝑚𝑠𝑔1 

𝑚𝑠𝑔2 

𝑚𝑠𝑔1 

𝑚𝑠𝑔3 

𝑚𝑠𝑔4 

𝑎𝑐1 𝑎𝑐2 

𝑚𝑠𝑔1 

(b) CDG of an example actor
model

Figure 2: Clinger event diagram versus CDG of an example actor model.

V ⊆ Act ×P(Act) is the set of vertices (states), v0 ∈ V is the initial vertex (state), and ↪→⊆
V ×Act ×V is the set of edges (transitions). For two given states u,v ∈V , there is (u,act,v)∈↪→
if and only if u = (act, pm) and ∃(ai,m′,a j)∈ pm such that v = ((ai,m′,a j),snt(ai,m′,a j)). This
way, the initial state of a CDG is defined as v0 = (ε, pm) where (ε,m,ai) ∈ pm and there is a
send statement in form of ai.m() in the main block of AC.

This way, as the definition of the CDG is based on the sent messages and the sent messages
are computed by static analysis of an actor model, the CDG can be created when the target actors
of sent messages can be found by static analysis. So, only the actor models which do not support
dynamic creation and dynamic binding of actors are in the scope of this work.

Next, we show that the abstract notion of the CDG reflects the cycles of the state space; more
precisely, our goal is to show that each cycle in the LTS of an actor model can be projected into
at least one cycle in the corresponding CDG.

Definition 6 (Labels, Sub-Traces, Sub-Cycles, and Cycles) Given an actor model AC a finite
trace tr of LTS(AC) = (S,s0,Act,→) is any finite word mi,mi+1,...mn ∈ M∗ such that there is a
sequence si,si+1,...sn,sn+1 of vertices in LTS(AC), where for any two consequest states s j and
s j+1 there is (s j,m j,s j+1)∈→.

The set of cycles of LTS(AC), denoted by Cycles(LTS(AC)), is the set of all traces that start and
end with the same message. A sub-trace of a cycle which starts and ends with the same message
is called a sub-cycle. The set of all edge labels of a given trace tr is denoted by Labels(tr).

Using the aforementioned definition, the projection is reduced to proving that each cycle in
LTS(AC) as the state space of the actor model AC, has a sub-cycle in CDG(AC). In order to prove
this property, we first prove the following lemma, which establishes a link between individual
messages appearing in the cycles of the state space and those appearing in the CDG. Here appear
means that the message is the label of at least one of the transitions of the state space.

Lemma 1 For each message m appearing in LTS(AC) of actor model AC, m also appears in
CDG(AC).

Proc. AVoCS 2015 6 / 15



ECEASST

Proof. Assume that there exist messages which appear in the state space but never appear in the
CDG. Pick one such message m that is reachable with the shortest trace from the initial state.
Assume that m is sent in the body of a service m′. Due to the minimality assumption for m, m′

should appear in the CDG and by the definition of CDG, m should appear in the CDG subsequent
to the edge labeled m′ (i.e., m′ is the parent of m), contradicting our original assumption.

We also need the following definition.

Definition 7 (Parent and ancestors) Assume that LTS(AC) and a trace mk →···→ mt → m j →
mi ∈ tr(LTS(AC)) are given, m j is called the parent of mi, and is denoted by P(mi). In addition,
all messages from mk to mt are called the ancestors of mi.

Theorem 1 (Mapping LTS(AC) Cycles into CDG Cycles) Each cycle in LTS(AC) as the state
space of the actor model AC, has a sub-cycle in CDG(AC).

Proof. Consider a cycle cLTS ∈ Cycles(LTS(AC)) and an arbitrary label m ∈ Label(cLTS); we
claim that for each trace m → ...→ m′ in the traces of cLTS, there exists a sub-trace m → ...→ m′
in CDG(AC). Once we prove this claim, the theorem follows by taking m → ... → m = cLTS as
the antecedent of the claim (then, it follows from the claim that there should exist a sub-cycle of
cLTS in the CDG, which was to be shown).

To prove the claim, we use induction on the length of the trace m → ... → m′. The base case
follows from Lemma 1. Assume that the claim holds for all traces of length n or less and consider
a trace m → ...→ m′ of length n + 1. Let M be the set of parents of m′ in all cycles of CDG (by
Lemma 1, m′ should appear in at least one cycle of the CDG). There exists some mi ∈M such that
m → ...→ m′ = m → ...→ mi → ...→ m′. The trace m → ...→ mi is of length n (or less) and
hence the induction hypothesis applies and a sub-trace of it appears in CDG(AC). Since mi is a
parent of m′ in the CDG(AC), an edge labeled m′ follows after mi. Therefore m → ...→ mi → m′
is a trace of CDG, which was to be shown.

3 Using CDG in Distributed LTL Model Checking Algorithms

In this section, we show how CDG can be exploited to improve the efficiency of state distribu-
tion policy in distributed LTL model checking algorithms. As mentioned before, decreasing the
number of split transitions reduces the required communication and hence the distributed model
checking cost. Here, we show that how using CDG of actor models results in a better distribution
of states in the distributed model checking of actor models. In the following, we show that how
the CDG-based policy is implemented for distributed BFS-based LTL model checking algorithm.

3.1 BFS-based LTL Model Checking algorithm

The BFS-based exploration algorithm, creates and explores the state space in a level-by-level
fashion and examines the back edges of the state space graph for cycle detection (explained
below). In the first step of the BFS algorithm, the Cartesian product of the initial state of the
state space and the property (i.e., the Büchi automaton which corresponds to the given property)

7 / 15 Volume 72 (2015)



State Distribution Policy

is stored, is marked as visited, and its level is set to zero. Then, for each level the successors of
the states of that level are generated by applying the successor function to both the state space
and the property automaton and their level is set by increasing the current level by one; when
there are no unexplored states in the next level, the algorithm terminates.

This algorithm can be implemented using two queues to manage states of each level. The first
queue stores the current level states (CLQ) and the second one stores the successors of the CLQ
states. The latter queue is called the next level queue (NLQ). In each iteration, the unexplored
states of the CLQ are dequeued and their unvisited successors are generated. When all states of
the CLQ are dequeued, the content of the NLQ is moved to the CLQ and the algorithm continues
until the NLQ is empty, i.e., all successors of the states in the CLQ have been visited. There is no
need to examine all visited states, because only back edges may create cycles. Figure 1 shows a
pseudo code of this algorithm with explores the state space and creates the Cartesian product of
a given state space and a property automaton. The backward search algorithm done by function
ACCEPTING-CYCLE-DETECTION(·) the same as the algorithm given in [BC06].

Algorithm 1: BFS-MODEL-CHECKING(systemInitState, propertyInitState) traverses a
given state space level by level and detects the existing accepting cycles.
Input: The initial state initState
Output: The result of the model checking

1 CLQ ←{〈systemInitState,propertyInitState〉}
2 NLQ ← /0
3 Visited ← /0
4 while CLQ 6= /0 do
5 foreach state 〈s, p〉∈CLQ do
6 foreach system state s′ ∈ SUCCESSORS(s) do
7 foreach property state p′ ∈ P-SUCCESSORS(p,s′) do
8 if 〈s′, p′〉 /∈ Visited then
9 Visited ← Visited∪{〈s′, p′〉}

10 NLQ ← NLQ∪{〈s′, p′〉}
11 else
12 ACCEPTING-CYCLE-DETECTION(〈s′, p′〉)

13 CLQ ← NLQ
14 NLQ ← /0

In the following, function SUCCESSORS(·) computes the successor states of its given system
state and P-SUCCESSORS(·) computes the property successor states based on its given property
state and system state.

3.2 Distributed BFS Model Checking Algorithm

A major difference between the centralized- and the distributed BFS model checking (BFS-MC)
algorithm is in storing the next level states. In the centralized BFS-MC, all newly generated

Proc. AVoCS 2015 8 / 15



ECEASST

system states are stored in the NLQ but in the distributed BFS-MC, some of them should be sent
to other nodes of the cluster. In other words, each state has a host node. The host of a state is the
node that is responsible for storing the state and generating its successors.

Algorithm 2: DISTRIBUTED-BFS-MODEL-CHECKING(initState,id) traverses a given
state space level by level.
Input: The initial state {〈systemInitState,propertyInitState〉} (which is null if this node is

not the host of the initial state) and the node’s id
Output: The result of the model checking

1 CLQ ←{〈systemInitState,propertyInitState〉}
2 NLQ ← /0
3 Visited ← /0
4 allFinished ← f alse
5 while ¬allFinished do
6 foreach state 〈s, p〉∈CLQ do
7 foreach system state s′ ∈ SUCCESSORS(s) do
8 hostId ← HASH-VALUE(s′)
9 foreach property state p′ ∈ P-SUCCESSORS(p,s′) do

10 if id = hostId then
11 if 〈s′, p′〉 /∈ Visited then
12 Visited ← Visited∪{〈s′, p′〉}
13 NLQ ← NLQ∪{〈s′, p′〉}
14 else
15 ACCEPTING-CYCLE-DETECTION(〈s′, p′〉)

16 else
17 SEND(〈s′, p′〉,hostId)

18 SYNCHRONIZE-ALL()
19 CLQ ← NLQ
20 NLQ ← /0
21 allFinished ← ALL-HOSTS-CLQ-IS-EMPTY()

Line 8 of Algorithm 2 shows host assignment based on the random distribution. After finding
the host, if the newly generated state host is the same as its parent’s and it has not yet been
visited, then the state is stored in NLQ. In contrast, if the newly generated state’s host is another
node, the state is sent to it. Then, the host node receives the new state and checks if the state
is visited before. To this aim, the receiving algorithm, i.e. Algorithm 3, is run in parallel with
the Algorithm 2 in each node. Therefore, checking whether a state is visited or not can be done
locally.

The other difference between the centralized and the distributed BFS-MC is in the cluster
nodes synchronization phase at the end of each iteration (line 21). In the synchronization phase,
nodes that finish processing their CLQ wait for other nodes to finish their work. Hence, after

9 / 15 Volume 72 (2015)



State Distribution Policy

Algorithm 3: RECEIVER(NLQ,allFinished) receives the sent states.
Input: Reference to the next level queue NLQ and the termination flag allFinished

1 while ¬allFinished do
2 〈s, p〉← RECEIVE-FROM-NETWORK()
3 if 〈s, p〉 /∈ Visited then
4 Visited ← Visited∪{〈s′, p′〉}
5 NLQ ← NLQ∪{〈s′, p′〉}

synchronization, all nodes have processed their CLQ states and are ready to continue the search
for the next level. If none of the nodes have any new state to explore, the value of allFinished
is set to true in line 24 to terminate the model checking.

3.3 States Distribution Policy based on CDG

In the new state distribution policy, we find the set of active cycles for each state. The active
cycles of each state are found in the CDG of the model and are based on the messages which can
be executed in that state. Without loss of generality, we base the definition of our distribution
policy on the simple cycles in a CDG (i.e., cycles with no repetition of vertices). When exploring
the transitions of a state, we store the states that belong to a cycle of the CDG on the same cluster
node, (i.e., states with the same active cycles).

Definition 8 (Active cycles of a state) Consider an actor model A and its CDG CDG(A) =
(V,v0,Act,↪→). For a given state v∈V , the set of active cycles of v is the subset of Cycles(CDG(A))
containing all cycles in which the label m j appear, where m j is a label of one of the outgoing
edges of state v.

The implementation of the new distribution policy is given in Algorithm 4. As shown in the
input section, the CDG of the model is generated before model checking and it is given as an
input to the algorithm. The main difference between Algorithms 2 and the new algorithm is in
the way of finding hosts in Algorithm 4. Namely, line 8 of Algorithm 2 is replaced with the
CDG-based distribution policy of lines 8 to 11.

4 Experimental Results

We implemented CDG-based distribution policy for the BFS-based distributed model checking
engine of Rebeca, an actor-based language with a Java-like syntax 1. We studied the impacts of
using CDG in the state space generation and the analysis against reachability properties, using
the current implementation of the Rebeca distributed model checking toolset. The test platform
has been Ubuntu 9.10 on a cluster of 2.2GHz Pentium 4 Core2 Duo with 2GB of RAM storage

1 A brief description about Rebeca and how the CDG of a Rebeca model is obtained is described in the full version
of this paper in the Rebeca homepage

Proc. AVoCS 2015 10 / 15



ECEASST

Algorithm 4: DISTRIBUTED-BFS-MODEL-CHECKING(initState,id,CDG) traverses a
given state space level by level.
Input: The initial state initState (which is null if this node is not the host of the initial state),

the node’s id, and CDG as the call dependency graph of the model
Output: The result of the model checking

1 CLQ ←{〈systemInitState,propertyInitState〉}
2 NLQ ← /0
3 Visited ← /0
4 allFinished ← f alse
5 while ¬allFinished do
6 foreach state 〈s, p〉∈CLQ do
7 foreach system state s′ ∈ SUCCESSORS(s) do
8 activeCycles ← /0
9 foreach message msg ∈ ENABLED-MESSAGE(s′) do

10 activeCycles ← activeCycles∪CDG-CYCLES(CDG,msg)
11 hostId ← CHOOSE-CYCLE(activeCycles)
12 foreach property state p′ ∈ P-SUCCESSORS(p,s′) do
13 if id = hostId then
14 if 〈s′, p′〉 /∈ Visited then
15 Visited ← Visited∪{〈s′, p′〉}
16 NLQ ← NLQ∪{〈s′, p′〉}
17 else
18 ACCEPTING-CYCLE-DETECTION(〈s′, p′〉)

19 else
20 SEND(〈s′, p′〉,hostId)

21 SYNCHRONIZE-ALL()
22 CLQ ← NLQ
23 NLQ ← /0
24 allFinished ← ALL-HOSTS-CLQ-IS-EMPTY()

11 / 15 Volume 72 (2015)



State Distribution Policy

for each cluster node. We chose the size of each cluster based on the number of simple cycles in
the CDG of each case study.

Three different case studies are used to compare the execution time and the memory consump-
tion among centralized model checking, distributed model checking with random distribution
policy, and distributed model checking with distribution policy based on CDG. The examples
are the asynchronous resource manager, dining philosophers, and train controller models.

In the dining philosophers model, there are a number of philosophers sitting at a round table.
Between each adjacent pair of philosophers, there is a chopstick. To model such a behavior, each
philosopher can be in one of the following states: thinking, hungry, or eating. A philosopher
thinks for a while, and then stops thinking and becomes hungry. When the philosopher becomes
hungry, she cannot eat until he owns both of the chopsticks to her left and right. When the
philosopher is done eating she puts down the chopsticks and begins thinking again.

In the train controller model there are a number of trains on each side of the bridge. Trains
arrive non-deterministically and the controller has to manage them in such a way that only one
train passes the bridge at a time, because there is one railway on the bridge. Each train announces
its arrival to the controller and the controller lets the train enter the bridge, if there is no other
train on the bridge. If the bridge is full then the arrived train is put in a queue. The waiting trains
will be served respectively. Each train should faithfully declare its departure to the controller.
The Rebeca code of each case study can be found at the Rebeca homepage [fml].

Each example represents different pattern of communication and synchronization: the dining
philosophers example shows a ring topology, the train controller and the asynchronous resource
manager show a star topology. In the dining philosophers example, each actor sends requests and
responses to its left and right neighbors. In the train controller, the bridge controller behaves like
a binary semaphore, whereas in the resource manager, the central node behaves like a counting
semaphore.

The asynchronous resource manager is model checked for deadlock freedom with 4 to 7 clients
(5 to 8 rebecs). The dining philosophers example is model checked for deadlock freedom with
2 to 5 philosophers (4 to 10 rebecs). The train controller model is model checked for deadlock
freedom with 2 to 8 trains (3 to 9 rebecs). Tables 1 and 2 show the results.

In the CDG-based distribution policy in comparison to the random distribution, there is the
overhead of cycle membership check and instead we have fewer split transitions and less com-
munication among cluster nodes for cycle detection. Our results show that time-wise the gain
exceeds the overhead.

As shown in Table 1 in the large enough cases, the number of split edges in the CDG-based
distribution policy is 50% to 70% of the random distribution policy. In addition, memory con-
sumption is reduced, because storing the split transitions requires storing endpoints host ids of
the edges. This improvement is about 10% for the asynchronous resource manager and 5% for
the train controller.
Table 2 shows the gain in the execution time that is about 8% for the asynchronous resource
manager and 13% for the train controller in their largest versions. For the dining philosophers
model, although the split cycles for the CDG-based policy are 52% of the random-based policy,
the execution time remains the same. This is due to the many back edges and the big cycles in
the state space. In this case the CDG-based policy reduces the split edges but the effect of the
reduction is negligible comparing to the time spent for backward search in detecting accepting

Proc. AVoCS 2015 12 / 15



ECEASST

Problem Size #Transitions #Split Transitions
Random CDG improvement

Asynch. Resource Manager

2 clients 94 39 36 8%
3 clients 818 540 432 20%
4 clients 7,76K 5,83K 4516 23%
5 clients 83,19K 66,52K 50,46K 25%
6 clients 1,02M 850,74K 635,14K 26%
7 clients 14,34M 12,30M 9,01M 27%

Dining Philosophers

2 phils 408 196 107 46%
3 phils 10,30K 6,97K 4,81K 31%
4 phils 206,00K 154,76K 75,86K 51%
5 phils 3,78M 3,02M 1,60M 47%

Train Controller

2 trains 86 46 36 22%
3 trains 620 433 296 32%
4 trains 4,46K 3,35 2,29K 32%
5 trains 33,30K 26,66K 18,17K 32%
6 trains 265,89K 221,61K 148,32K 34%
7 trains 2,30M 1,97M 1,30M 35%
8 trains 21,83M 19,11M 12,40M 36%

Table 1: Split edges in the random and the CDG-based distribution policies.

cycles.
We also measured load balancing of cluster nodes for the two distributed policies. Random

distribution results in balanced load for each node. In our experimental results, we could see that
in random distribution, the deviation from the best distribution starts from 9% in small models
and reduces to less than 1% for the larger one. In the CDG distribution this deviation starts from
13% and reduces to 1.28% for larger models.

In general the experimental results show that our technique outperforms random distribution
when the size of the model is large enough. The gain increases as the size of the model grows.
Also in our approach, the load balancing of cluster nodes converges to the optimum point in
larger examples.

5 Discussion, Conclusion and Future Work

In this paper we introduced the Call Dependency Graph (CDG) for the actor-based modeling
languages. The CDG is generated by a static analysis of the model and is an abstract graph
capturing the causality of message passing among actors. We designated and proved a relation
between the cycles in the CDG and the cycles in the state space. We devised a distribution policy
for the distributed model checker of Rebeca based on the CDG. The new distribution policy
increases the efficiency of distributed model checking by increasing the locality of the accepting
cycles. Our new policy is implemented as an extension of breadth first search distributed model
checking. Experimental evidence supports that this new policy improves cycle locality, and
decreases model checking time and memory in practice.

As future work, we plan to improve our algorithm by duplicating states to avoid split cycle
creation such that all cycles can be detected locally. This comes at the cost of more memory
consumption, and we need to define a set of criteria to balance between the increase in the size of
state space, due to duplicating states, and the decrease in the verification time, due to localizing

13 / 15 Volume 72 (2015)



State Distribution Policy

Problem Size #States Time (sec)
Centralized Random CDG

Asynch. Resource Manager

2 clients 51 0 0 0
3 clients 344 0 1 1
4 clients 2,86K 0 4 4
5 clients 28,78K 1 6 6
6 clients 344,24K 157 24 21
7 clients 4,71M > 6 hour 1846 1704

Dining Philosophers

2 phils 183 0 1 1
3 phils 3,06K 2 8 8
4 phils 46,01K 381 209 209
5 phils 675,56K > 6 hour 4821 4818

Train Controller

2 trains 46 0 0 0
3 trains 250 0 1 1
4 trains 1,51K 0 2 2
5 trains 10,19K 1 3 3
6 trains 76,64K 9 4 4
7 trains 641,74K 1147 26 24
8 trains 5,96M > 6 hour 3192 2789

Table 2: Time consumption for centralized and distributed model checking with the random and
the CDG-based distribution policies.

cycles. Moreover, we look for property classes for which our distribution policy guarantees
localized cycles. Finally, we would like to investigate the effect of incorporating CDG into other
analysis and reduction techniques such as slicing.

Acknowledgments. We thank the anonymous reviewers of AVoCS 2015 for their useful com-
ments. The work of M.R. Mousavi has been partially supported by the Swedish Research Council
(Vetenskapsrådet) with award number 621-2014-5057 (Effective Model-Based Testing of Paral-
lel Systems) and the Swedish Knowledge Foundation (Stiftelsen för Kunskaps- och Kompeten-
sutveckling) in the context of the AUTO-CAAS project.

Bibliography

[AMST97] G. Agha, I. A. Mason, S. F. Smith, C. L. Talcott. A Foundation for Actor Computa-
tion. J. Funct. Program. 7(1):1–72, 1997.

[BBC05] J. Barnat, L. Brim, I. Cerná. Cluster-Based LTL Model Checking of Large Systems.
In Boer et al. (eds.), FMCO. Lecture Notes in Computer Science 4111, pp. 259–279.
Springer, 2005.

[BBS01] J. Barnat, L. Brim, J. Strı́brná. Distributed LTL Model-Checking in SPIN. In Dwyer
(ed.), SPIN. Lecture Notes in Computer Science 2057, pp. 200–216. Springer, 2001.

[BC06] J. Barnat, I. Cerná. Distributed breadth-first search LTL Model Checking. Formal
Methods in System Design 29(2):117–134, 2006.

Proc. AVoCS 2015 14 / 15



ECEASST

[BCKP01] L. Brim, I. Cerná, P. Krcál, R. Pelánek. Distributed LTL Model Checking Based
on Negative Cycle Detection. In Hariharan et al. (eds.), FSTTCS. Lecture Notes in
Computer Science 2245, pp. 96–107. Springer, 2001.

[BCMS06] L. Brim, I. Cerná, P. Moravec, J. Simsa. How to Order Vertices for Distributed LTL
Model-Checking Based on Accepting Predecessors. Electr. Notes Theor. Comput.
Sci. 135(2):3–18, 2006.

[BHR13] J. Barnat, J. Havlı́cek, P. Rockai. Distributed LTL Model Checking with Hash Com-
paction. Electr. Notes Theor. Comput. Sci. 296:79–93, 2013.

[CES86] E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatic Verification of Finite-State
Concurrent Systems Using Temporal Logic Specifications. ACM Transaction on
Programming Languages and Systems 8(2):244–263, 1986.

[Cli81] W. D. Clinger. Foundations of Actor Semantics. Technical report, Cambridge, MA,
USA, 1981.

[fml] Rebeca Home Page - Distributed Model Checking Section. http://www.rebeca-
lang.org/wiki/pmwiki.php/Tools/RebecaDistributedModelChecker.

[GHS01] O. Grumberg, T. Heyman, A. Schuster. Distributed Symbolic Model Checking for
µ -Calculus. In Berry et al. (eds.), CAV. Lecture Notes in Computer Science 2102,
pp. 350–362. Springer, 2001.

[GMS13] H. Garavel, R. Mateescu, W. Serwe. Large-scale Distributed Verification Using
CADP: Beyond Clusters to Grids. Electr. Notes Theor. Comput. Sci. 296:145–161,
2013.

[Hew72] C. Hewitt. Description and Theoretical Analysis (Using Schemata) of PLANNER: A
Language for Proving Theorems and Manipulating Models in a Robot. MIT artificial
intelligence technical report 258, Department of Computer Science, MIT, 1972.

[LT88] K. G. Larsen, B. Thomsen. A Modal Process Logic. In LICS. Pp. 203–210. IEEE
Computer Society, 1988.

[OPE05] S. Orzan, J. van de Pol, M. V. Espada. A State Space Distribution Policy Based on
Abstract Interpretation. Electr. Notes Theor. Comput. Sci. 128(3):35–45, 2005.

[SMSB04] M. Sirjani, A. Movaghar, A. Shali, F. S. de Boer. Modeling and Verification of Re-
active Systems using Rebeca. Fundamenta Informaticae 63(4):385–410, 2004.

[VVFB11] S. Vijzelaar, K. Verstoep, W. Fokkink, H. E. Bal. Distributed MAP in the SpinJa
Model Checker. In Barnat and Heljanko (eds.), Proceedings 10th International
Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011, Snow-
bird, Utah, USA, July 14, 2011. EPTCS 72, pp. 84–90. 2011.

15 / 15 Volume 72 (2015)


	Introduction
	Call Dependency Graphs of Actor Models
	Using CDG in Distributed LTL Model Checking Algorithms
	BFS-based LTL Model Checking algorithm
	Distributed BFS Model Checking Algorithm
	States Distribution Policy based on CDG

	Experimental Results
	Discussion, Conclusion and Future Work