On-the-Fly Model Checking Under Fairness that Exploits Symmetry.
An on-the-fly algorithm for model checking under fairness is presented. The algorithm utilizes symmetry in the program to reduce the state space, and employs novel techniques that make the on-the-fly model checking feasible. The algorithm uses state symmetry and eliminates parallel edges in the reachability graph. Experimental results demonstrating dramatic reductions in both the running time and memory usage are presented.
Introduction
The state explosion problem is one of the major bottlenecks in temporal logic model
checking. Many techniques have been proposed in the literature [6, 5, 9, 8, 13, 11,
12, 16, 17] for combating this problem. Among these, symmetry based techniques
have been proposed in [5, 9, 13]. In these methods the state space of a program
is collapsed by identifying states that are equivalent under symmetry and model
checking is performed on the reduced graph. Although the initial methods of [5, 9]
could only handle a limited set of liveness properties, a more generalized approach
for checking liveness properties under various notions of fairness has been proposed
in [10]. This method, however, does not facilitate early termination, it supplies an
answer only after the construction of all the required data structures is complete.
Many traditional model checking algorithms ([3, 11, 12, 17]) use on-the-fly techniques
to avoid storing the complete state space in the main memory. However,
none of these techniques employ symmetry. [13] uses on-the-fly techniques together
with symmetry for model checking. There the focus is on reasoning about a simple
but basic type of correctness, i.e., safety properties expressible in the temporal logic
CTL by an assertion of the form AG:error.
In this paper, we present an on-the-fly model checking algorithm that checks for
correctness under weak fairness and that exploits symmetry. computation is said
* A preliminary version of this paper appeared in the Proceedings of the 9th International
Conference on Computer Aided Verification held in Haifa, Israel in June 1997. The work presented
in this paper is partially supported by the NSF grants CCR-9623229 and CCR-9633536
to be weakly fair if every process is either infinitely often disabled or is executed
infinitely often). This work is an extension of the work presented in [10]. Here
we develop additional theory leading to novel techniques that make the on-the-
fly model-checking feasible. We not only exploit the symmetry between different
states, but also take advantage of the symmetric structure of each individual state;
this allows us to further reduce the size of the explored state space.
The other major improvement is gained by breaking the sequential line of the
algorithm. The original algorithm constructed three data structures (the reduced
state space, the product graph and the threaded graph - details are given below)
one after the other and performed a test on the last one. We eliminated the construction
of the third data structure by maintaining some new dynamic information;
the algorithm constructs parts of the first structure only when it is needed in the
construction of the second; finally we store only the nodes in the second structure.
This on-the-fly construction technique and up-to-date dynamic information maintenance
facilitates early termination if the program does not satisfy the correctness
specification and allows us to construct only the minimal necessary portion of the
state space when the program satisfies the correctness specification. The on-the-fly
model checking algorithm has been implemented and experimental results indicate
substantial improvement in performance compared to the original method.
The algorithm, given in [10], works as follows. It assumes that the system consists
of a set I of processes that communicate through shared variables. Each variable is
associated with a subset of I , called the index set, that denotes the set of processes
that share the variable. Clearly, the index set of a local variable consists of a single
process only. A state of the system is a mapping that associates appropriate values
to the variables. A permutation - over the set I of processes, extends naturally
to a permutation over the set of variables and to the states of the system. A
permutation - is an automorphism of the system if the reachability graph of the
system is invariant under - (more specifically, if s ! t is an edge in the reachability
graph then -(s) ! -(t) is also an edge and vice versa). Two states are equivalent
if there is an automorphism of the system that maps one to the other. Factoring
with this equivalence relation compresses the reachable state space.
The original method consists of three phases. First it constructs the reduced
state space. Then it computes the product of the reduced state space and the finite
state automaton that represents the set of incorrect computations. It explores
the product graph checking for existence of "fair" and "final" strongly connected
components; these components correspond to fair incorrect computations. Checking
if a strongly connected component is fair boils down to checking if it is fair with
respect to each individual process. This is done by taking the product of the
component and the index set I . The result is called the threaded graph resolution
of the component. A path in the threaded graph corresponds to a computation of
the system with special attention to one designated process. Fairness of a strongly
connected component in the product graph is checked by verifying that each of the
strongly connected components of its threaded graph are fair with respect to the
designated process of that component.
Our on-the-fly algorithm has two layers: the reduced state space and the product
graph construction. The successors of a node in the reduced state space are constructed
only when the product graph construction requests it. The product graph
construction is engined by a modified algorithm for computing strongly connected
components (scc) using depth first search (see [2]). During the depth first search,
with each vertex on the stack it maintains a partition vector of the process set I .
The partition vector associated to a product state u captures information about
the threaded graph of the strongly connected component of u in the already explored
part of the product graph. Intuitively, if processes i and j are in the same
partition class then it indicates that the nodes (u; i) and (u; are in the same scc
of the threaded graph. This reveals that the infinite run of the system corresponding
to the strongly connected component of u in the already explored part of the
product graph is either fair with respect to both processes i and j or it is not fair
with respect to any of the mentioned processes. The partition vectors are updated
whenever a new node or an edge to an already constructed node is explored. The
correctness of the above algorithm is based on new theory that we develop as part
of this paper; this thoery connects the partition vectors of the algorithm with the
strongly connected components of the threaded graph.
A permutation - 2 AutM on processes is a state symmetry of a state s, if
(state symmetry was originally introduced in [9]). Suppose that - maps process i
to j. In that case, transitions ignited by process i are in one-to-one correspondence
with those caused by process j. Hence, we can save space and computation time
by considering only those that belong to process i. This is one of the forms state
symmetry is exploited in our algorithm. Another way is the initialization of the
partition vector with the state symmetry partition. If - maps process i to j then
the threads corresponding to process i and j are certainly in the same situation:
they are either both fair or none is fair.
Our paper is organized as follows. Section 2 contains notation and preliminaries.
In Sect. 3 we develop the necessary theory and present the on-the-fly algorithm.
We describe various modifications of the algorithm that take state symmetry into
consideration. Section 4 presents experimental results showing the effectiveness of
our algorithm and dramatic improvements in time as well as memory usage. Section
5 contains concluding remarks.
2. Preliminaries
2.1. Programs, Processes, Global State Graph
Let I be a set of process indices. We consider a system
running in parallel. Each process K i is a set of transitions. We assume that
all variables of P are indexed by a subset of I indicating which processes share
the variable. A system P , that meets the above description, is called an indexed
transition system (or briefly program).
A global state of an indexed transition system is an assignment of values to the
variables. We assume that each variable can take only a finite number of values.
This assumption ensures that the number of global states of the system is also
finite. We define an indexed graph M on the set of global states that captures the
behavior of the program. The indexed global state graph is
is the set of global states, s 0 is the initial state, and R ' S \Theta I \Theta S is the transition
relation, i.e., s i
there is a transition in process i that is enabled in state
s and its execution leads to state t.
2.2. Strongly Connected Subgraphs and Weak Fairness
Infinite paths in M starting from the initial state denote computations of P . An
infinite path p in M is weakly fair if for each process i, either i is disabled infinitely
often in p or it is executed infinitely often in p. Unless otherwise stated, we only
consider weak fairness throughout the paper. The implementation, however, is
capable of handling strong fairness. (An infinite execution of the program is strongly
fair if every process that is enabled infinitely often is executed infinitely often.)
A strongly connected subgraph of a graph is a set of nodes such that there is a
path between every pair of nodes passing only through the nodes of the subgraph.
A strongly connected component (scc for short) is a maximal strongly connected
subgraph.
The set of states that appear infinitely often in an infinite computation of a finite
state program P forms a strongly connected subgraph of M . Many properties
of infinite computations, such as fairness, are in one-to-one correspondence with
properties of the associated strongly connected components of M . Therefore, all of
our efforts will be directed towards finding an scc of M with certain properties.
We can formulate weak fairness as a condition on scc's.
Definition 1. An scc C of M is weakly fair if every process is either disabled in
some state of C or executed in C. (Process i is disabled in state s if all of its
transitions are disabled in s; process i is executed in C if there are states s; t in C
such that s i
For a given program P , we are interested in checking the absence of fair and
incorrect computations. Here we assume that incorrectness is specified by a Buchi
automaton A; the set of computations accepted by A is exactly the set of incorrect
computations. The problem of checking whether the program P has any incorrect
weakly fair computation can be decided by looking at the product graph B 0 of M
and A. If B 0 has an scc whose A projection contains a final automaton state and
whose M projection is weakly fair then P has a weakly fair incorrect computation.
Here it is sufficient if we construct the product of the reachable part of M and A.
2.3. Annotated Quotient Structure
The previously suggested method, i.e., of analyzing the reachable part of M , can
be very expensive since, for many systems, the reachable part of M is huge. For
systems that exhibit a high degree of symmetry, the state space can be reduced
by identifying states that are equivalent under symmetry and by constructing the
quotient structure as given below.
Denote the set of all permutations on I by Sym I , let - 2 Sym I . - induces
an action on the set of variables and on the set of global states in the following
way. For every variable v
, its image under - is -(v
course,
may not be a variable of the program. We say that - respects the
set of variables if the image of every variable is a variable of the program. Assume
that - has that property. The image of a global state s under - is defined to be
the global state -(s) that satisfies that the value of
in s is the same as
the value of -(v
in -(s) for every variable v
of the program. We say
that - is an automorphism of the indexed global state graph M if - respects the
exactly when -(s) -(i)
R. The set
of automorphisms of M is denoted by AutM . Certainly, AutM is a subgroup of
Sym I .
Given any subgroup G of AutM , we can define an equivalence relation on S.
State s is equivalent to t if there is a - 2 G such that t. Using G, M can
be compressed to a smaller structure called the annotated quotient
structure (AQS) for M , as follows.
ffl S is a set of representative states that contains exactly one state from each
equivalence class of S=G, in particular, it contains s 0 itself from s 0 's class.
ffl R is a set of triples s -;i
\Gamma! t denoting edges between representative states annotated
with permutations from G and with process indices. To define R
formally, with each state t 2 S, we define t rep to be the unique representative
state of the equivalence class of t; with each such t, we also associate
a canonical permutation - t 2 G such that
Rg.
Remark. In many cases it is useful to allow multiple initial states to capture
nondeterminism of the program. In [10] M is defined to have a set S 0 of initial
states and it is required that for every automorphism - and s
concept of multiple initial state can be simulated in our system by introducing a
new, fully symmetric initial state s 0 and for every s 2 S 0 and i 2 I an edge s 0
2.4. Checking for Fairness and the Threaded Graph
We briefly outline the approach taken in [10] for checking if a given concurrent
program P exhibits a fair computation that is accepted by an automaton A. Assume
that the automaton A refers to variables whose index set involve processes
specifies a property of the executions of these processes
only. These processes are called global tracked processes. If we traverse in
the compressed M these global tracked processes are represented by different sets
in each state of the path. Formally, the local tracked processes in a state t after
passing through the path p are - is the product of
the permutations found on the edges of p. For example, if the first edge of the
path is s 0
\Gamma! t then, since t is only a representative of the real successor state, the
global tracked processes are represented by the processes -
t. After some steps in the path we may return to state t again but at that time
we encounter a different set of local tracked processes. This property makes M not
feasible for model checking purposes. M is too compact, we need a less compressed
version of M where the set of local tracked processes in a given state t does not
depend on the path that lead to t from the initial state. We need to unwind M
partially; the threaded graph construction captures this unwinding.
be any graph whose edges are labeled with permutations of a set
I , and possibly with other marks. The k-threaded graph H k-thr corresponding to H
is hV \Theta I k consists of edges of the form (s;
\Gamma!
k. Note that if H has
labels on its edges (denoted by - in the previous line) other than the permutations
of a I then H k-thr inherits them. The 1-threaded graph corresponding to H is
denoted by H thr . The second component in a state (s; i) of H thr is called the
designated process. The following simple example depicts these concepts. Here, and
throughout the paper, id denotes the identity permutation, - ij the transposition
that interchanges i and j.
Graph H
A
Graph H thr (edge labels are not indicated)
@
@
@
@I 6
@
@
@ @R
\Gamma\Psi

Figure

1. The threaded graph construction
The original algorithm first constructs the annotated quotient structure M corresponding
to P . In the second step, a product graph
\Theta A is
constructed. Each state of this product graph is of the form (s;
is an edge of B 0 if (s;
\Gamma!
is an edge of M k-thr
and the automaton A has a transition from
state a to a 0 on the input consisting of the program state obtained by simultaneously
replacing index c l by i l for each l 2 k.
In the third step the product graph B 0 is checked for existence of fair strongly
connected components (these are called subtly fair sccs in [10]). This checking is
done by constructing the threaded graph resolution of every scc of B 0 . Every scc
of the threaded graph is checked if it is fair with respect to the designated process.
In Sect. 3 below we show that, using techniques based on new and deeper theoretical
results, the above method can be considerably enhanced.
OEAE
"!
#/
iii
rii
rrr
OEAE
oe id; 1id\Gamma
\Gamma\Psi
cri
\Gamma\Psi
crrid6
\Gamma\Psi
Figure

2. The AQS M for the simplified Resource Controller
StartingState A0;
FinalState
True
oe STATE[1] != C
OEAE
ae-
oe True

Figure

3. The automata A
2.5. The Simplified Resource Controller Example
To illuminate our general concepts we present the instructive example of the simplified
Resource Controller.
The program consists of a server and 3 client processes running in parallel. Each
client is either in idle (i), request (r) or critical (c) state. The variable STATE[c]
indicates the status of client c ( 3). Clients can freely move between idle
and request state. The server may grant the resource to a client by moving it to
critical state, provided that that client is in request state and no client is in critical
state yet.
For this simple example, M has 20 states (all combinations of values i, r and c
except those that contain more than one c.) As a contrast, M has only 7 states.
(as illustrated in Fig. 2.)
The initial state is the one marked with iii in the lower left side of the figure.
All three process are in idle (i) state. Any of them can move to request state (r),
hence it has three successors in the state space: rii, iri and iir. All of these states
are equivalent, we chose rii to be the representative of them. The three edges
departing from iii correspond to the three enabled transitions. Edge iii -01 ;1
\Gamma! rii
for example indicates that process 1 has an enabled transition and the execution
of that transition leads to state - \Gamma1
Similarly, state rri represents 3
states: itself, rir and irr.
Suppose that we want to check the (obviously false) property that Client 1 never
gets to critical state. The negation of that property can be captured by the automaton
given in Figure 3; this automaton states that Client 1 eventually gets
to a critical state. The global tracked process is 1. The product graph B 0 has
states. A depth first search on B 0 reveals that it has a strongly
connected subgraph that is weakly fair and contains a final automaton state.
3. Utilizing State Symmetry
The original algorithm, briefly described in subsection 2.4, constructed B together
with the threaded graph B thr
0 . This method can be improved by applying the
following three new ideas.
In constructing M k-thr
our goal was to define a less compressed version of M with
the property that if we visit a state t multiple times by an infinite path then we
encounter the same set of local tracked processes. In that sense, we can link the set
of local tracked processes to that state. The k-threaded graph unwinding of M was
not the optimal solution. We can define an equivalence relation on M \Theta I k that
usually results in greater compression: M \Theta I k still has the desired property, and
it is smaller than M k-thr
in cases where the program exhibits some symmetry. (It
is possible for two states (s;
to be equivalent
and be represented by a single state in M \Theta I k .)
The second improvement is the application of an on-the-fly algorithm. Here we
incrementally construct B and simultaneously explore it. By this exploration we
analyze the threaded graphs without constructing them. If the partially explored B
contains a required subgraph then the algorithm immediately exits saving further
computation time. Because of the on-the-fly nature of the algorithm, we do not
need to store the complete B. Specifically, no edges need to be stored.
Finally, the third idea is to use the symmetry of a single global state. Using state
symmetry we can reduce the number of edges by eliminating the redundant parallel
ones. Such redundant parallel edges can be removed from M also. This results in
further reduction in memory usage.
For keeping the presentation simple, we assume that we are tracking only one
process. Doing so, we do not loose generality. All the results, that are presented
below, apply (with the obvious modifications) to the case with many tracked pro-
cesses. In the actual implementation of the algorithm given below, we used the
general case.
3.1. Compressing M \Theta I
In Subsect. 2.3 we defined an equivalence relation on S. Now, we extend it to
S \Theta I as follows. We say that are equivalent if there is a
permutation - 2 G such that Obviously,
this equivalence relation partitions the set S \Theta I into a set of equivalence classes.
Let S aqsi be a set of representative states that contains exactly one state from
each equivalence class. To ensure that S aqsi and S are closely related we adopt the
convention that (s; i) 2 S aqsi implies s 2 S, that is, S aqsi ' S \Theta I . This containment
may be strict as it is possible for two states of the form (s; i) and (s; j) to be
equivalent. The annotated quotient structure of M with a tracked index (AQSI) is
\Gamma! (t;
(i)g.
In a state (s; i), i is the local tracked process. Note that the indicated initial state
s 0 is formaly not an element of the set of states S aqsi , no specific tracked process
is assigned with it. This seemingly unnatural definition was adopted because we
did not want to encorporate information on the automaton A into the definition of
M \Theta I .
\Theta I can be considerably smaller than M thr
. In the best
case, we may achieve a reduction in the number of nodes and number of edges by
a factor of n and n 2 , respectively. (Here, n is the size of I.)
In our simplified Resource Controller example M thr has 7 states. To
calculate the size of S aqsi note first that in state iii all 3 processes are in the same
local state, hence (iii, 0), (iii, 1) and (iii, 2) are equivalent in M \Theta I so only one
of them needs to be included in S aqsi . Similarly, only one of (rrr, 0), (rrr, 1)
and (rrr, 2) is in S aqsi . If s is any of rii, rri, crr or iic then two of (s; 0), (s; 1)
and (s; 2) are equivalent, hence only two need to be stored in S aqsi . Finally, in
the case of s = cri all processes are in different local state, therefore, all (s; 0),
(s; 1) and (s; 2) should be in S aqsi . This counting shows that S aqsi contains only 13
representative states.
Let B be the product of M \Theta I and A. Formally,
0 with the property that (s; i 0
0 ) is the representative of
. Recall that i 0 is the process being tracked by the automaton A.
R pr consists of edges (s; i; a) -;l
\Gamma! (t; j; a 0 ) such that (s; i) and (t; are in S aqsi ,
(s; i) -;l
\Gamma! (t; and the automaton A moves from state a to a 0 on the input
gained from s after replacing all occurrences of index i with i 0 .
Definition 2. Let C be an scc of B. An scc D of C thr is weakly fair if there is
a state (u; k) in D such that process k is disabled in u or D has an edge of type
Using slightly modified versions of arguments found in [10] we deduce that B
contains all the information needed to decide if the program P satisfies the complement
of the property given by A. This is stated in the following theorem which
can be proved exactly on the same lines as theorem 3.3 and lemma 3.8 of [10] by
using our new definition of B.
Theorem 1 P satisfies the complement of the property defined by A if and only if
there is no scc C of B such that C contains a final automaton state and every scc
of C thr is weakly fair.
4. On-the-Fly Model Checking
The main contribution of the present paper lies in showing that we can search for
an scc of B without requiring the complete B to be previously constructed. B can
be explored while we are constructing it in an on-the-fly manner.
As it was mentioned earlier, B is constructed to be the product of M \Theta I and
A. One of the first improvements is that we do not construct M \Theta I but only the
smaller M . By the construction of B we implicitly create M \Theta I and store it as part
B. This is based on the observation that, after a careful choice of representative
states, M \Theta I is a threaded graph resolution of M . By the construction, each of the
nodes of the threaded graph are checked for equivalence against all the nodes stored
already (implicitely, as part of B). The new node is stored only if it is the first
one in its equivalence class. This is done in command 6 of the algorithm presented
below.
In our implementation we can control the way M is constructed. In the default
(and most efficient) case the successors of an M state together with the edges leading
to them are created (stored) when they are first needed in the construction of B. If
we want to avoid storing the edges of M we can use the second option that recreates
them temporarily each time when a B state construction requires it. As a third
possible option, the implementation allows us to construct M in advance. This can
be usefull when the program is tested against multiple correctness properties.
The second component, used by the construction of B, is the automaton A representing
the correctness property. As A is small in size compared to other data
structures involved, its construction in an on-the-fly manner is not motivated.
After these general introductory lines, let us turn to presenting the actual al-
gorithm. As explained earlier, our on-the-fly model-checking algorithm explores
simultaneously as it constructs it. During this process, in order to analyze the
threaded graph without explicitly constructing it, we maintain a partition of I with
each B node on the stack. This partition indicates which processes are known to
be in the same strongly connected component of the threaded graph.
4.1. Partitions
First, we would like to adopt the following conventions concerning partitions. We
identify equivalence relations and the corresponding partitions on a given set. In
that sense, we say that a partition contains another partition if the equivalence
relation corresponding to the first partition is a superset of the equivalence relation
corresponding to the second partition. The join of two partitions is the smallest
partition containing both.
The following two lemmas prove some important properties of sccs in B.
C be an scc in B. Then the following properties hold.
ffl If are nodes in C and there is a path from (r; i) to (r thr then there
is a path from (r 0 ; j) to (r; i) as well.
ffl The sccs in C thr are disjoint, i.e., no two distinct sccs are connected by a path
in C thr .
Proof: The first part of the lemma is proved as follows. Assume that are
nodes in C and there is a path from (r; i) to (r 0 ; in C thr . This means that there
exists a path p from r to r 0 in C such that is the product
of all the permutations on the path p. Since C is an scc, there exists a path
p 0 from r 0 to r in C. Let - 0 be the product of the permutations on p 0 . There
exists an n ? 0 such that (- is the identity permutation. Now, consider
the path (p This path creates a cycle in C thr starting from (r; i) back to
passing through (r obviously, this cycle contains a path from (r 0 ;
to (r; i). The second part of the lemma follows trivially from the first part.
a) be a state in B and C be the scc of B that contains r. We define
the equivalence relation
- r on I as follows:
are in the same component of C thr .
It is easy to see that a class of the partition
- r identifies a unique component of
thr , and every component of C thr is identified by a class of
- r . Thus, we will use
these partitions to represent the sccs of C thr . A class of
- r is called weakly fair if
the corresponding scc of C thr is weakly fair. Note that the tracked process l in r
always forms a class of size 1.
Suppose that if r and r 0 are nodes in the same scc in B. The partitions of
- r and

are not equal in most cases, but fortunately one can be obtained from the other
by a permutation belonging to G. This problem motivates the use of a common
referential base. A possible nominee for this is the initial state s pr of B.
Assume that we have explored B in a depth first manner starting from the initial
state, until all reachable states have been visited. Let T be the resulting depth
first spanning tree. Now, for each state u 2 B, let - u denote the product of the
permutations on the unique s pr ! u path in T . Now, for each state r in B, we
define an equivalence relation - r on I as follows.
r
r
are nodes in the same scc C of B then -
Proof: To prove the lemma, it is enough if we show that, for every
implies vice versa. We show this by proving that, for every i,
r
and (r
are in the same scc in C thr . This will automatically imply the
following: for every i and j, if i - r j, i.e., there is a path in C thr from
r
to
r
(j)), then there is also a path from (r
r 0 (j)) and hence
To show that
r (i)) and (r
are in the same scc in C thr , we take the
following approach. Let u be the root of the scc C, i.e., u is the first node in C
that was visited during the depth-first search that induced the forest F . Let T be
the tree in F that contains u and r, and let the initial state s pr be the root of T .
It can be shown that the unique path in T from s pr to r passes through u (see
[7]). Hence, there exists a path in C thr from (u; - \Gamma1
(i)) to
r
(i)). Hence, by
Lemma 1, we see that these two nodes are in the same scc in C thr . By a similar
argument, we see that
are in the same scc. This shows
that
r
are in the same scc.
Intuitively, indicates that the threads of (s pr ; i) and (s pr ; enter the same
scc of the threaded graph after they passed r. To illustrate these concepts consider
the subgraph of the simplified Resource Controller example depicted in Figure 4
below. The tree edges are denoted by boldface arrows.
OEAE
s pr
OEAE
OEAE
OEAE
\Gamma\Psi
Figure

4. A strongly connected subgraph of the product graph B
The nodes strongly connected subgraph. In u 1 we have
is an immediate successor of both in the
threaded graph. Hence,
- u1 is 0 12 . Similarly,
- u2 is 0 12 , but
- u3 is 1 02 .
Using that -
Returning to the general argument, we show how to compute - r by exploring
using depth first search. For each edge
\Gamma! v in B, let - e denote the
permutation - u
. Note that if e is an edge of T then - e is the identity
permutation. The permutation - e satisfies the following property.
e is an edge in the scc C containing r, then - e
Proof: Since T is a depth first search tree, it enters an scc of the graph in a unique
vertex. According to Lemma 2, - in the same scc, therefore, we
may assume that r is the root of the scc that contains e. Hence, there are paths p 1
and p 2 on T from r to both endpoints u; v of e. Let - be the products of all
the permutations on the paths p 1 and p 2 respectively. It should be easy to see that
r
r
Now, to demonstrate that i - r j, it is enough if we show that there is a path
in C thr from
r
(j)) to
r
(i)). By substituting - u
(i) for j and
replacing - \Gamma1
r
r
(i). Let - 00 denote the
permutation
r
Hence - \Gamma1
r
r
(i).
Since r and v are in the same scc, there exists a path p 0 from v to now, the
path cycle and there exists an n ? 0 such that (p 2 is also a cycle
and the product of all the permutations on this cycle is the identity permutation.
This big cycle can be written as
2 is the path
it should be obvious that the product of all the permutations on p 0
.
Finally, consider the cycle
2 in C. The product of all permutations on
this cycle equals - 1
2 , which is - 00 . This cycle creates a path in C thr from
r
(i)) to
r
(i)).
r
r
(i), it follows that there is
a path in C thr from
r
(j)) to
r
(i)).
Let ae be a permutation on I . We define the orbit relation of ae to be the reflexive,
transitive closure of the binary relation Ig. Obviously, the orbit
relation of ae is an equivalence relation; we define the orbit partition of ae to be the
partition induced by the orbit relation of ae. Now Proposition 1 can be reformulated
as: If e is an edge in the scc of r, then the orbit partition of - e is smaller than or
equal to (i.e. a subset of) - r . The following stronger result characterizes - r .
Theorem 2 - r is the join of all orbit partitions of - e , where e ranges over the
edges of the strongly connected component of r, i.e. it is the smallest equivalence
relation containing the orbit relation - e , for each edge e in the scc containing r.
Proof: We need to show that i - r j implies that there are processes
and edges e in the scc of r such that - ek (i k+1
and This would indicate that (i k ; i k+1 ) is in the orbit relation of - ek ;
hence, (i; j) is in the smallest equivalence relation containing the orbit relations of
all the edges in the scc.
The relationship
r
r
(j). Therefore,
r
(i)) and
r
(j)) are in the same scc of the threaded graph. Let
r
r
(j)) be a path that connects them. Take i k to
be - rk (l k ). Certainly,
be the permutation labeling the edge e k
(note that - 0
is different from - ek ). Now we have - ek (i k+1
(i
(i k+1 ), we get - ek (i k+1
(l
Substituting l
(l (from the definition of the threaded graph), we get
This completes the proof.
In our illustrating example in Figure 4 we can compute - e for the 4 edges in the
component g. e
\Gamma!
\Gamma! u 3 are tree edges so
\Gamma! u 1 we find that -
In a similar way, we compute for e
\Gamma! u 2 that
u2
. The orbit partition of -
while that of - e4 is 1 02 . The join of these partitions is 1 02 that coincides
with
The next theorem follows immediately from Definition 2 and is a necessary and
sufficient condition for checking if a class of - r is weakly fair. Let C be the scc of
r in B.
Theorem 3 A class K of the partition - r is weakly fair if and only if there is an
(i) is disabled in u or it is executed (that is,
there is an edge
\Gamma! v in C).
We have gathered together all the necessary tools to present the on-the-fly algorithm

4.2. The Algorithm
Our algorithm is a modification of the strongly connected component computation
using depth first search presented e.g. in [2].
For each vertex a) of the product graph B, we maintain the following
information.
ffl u:dfnum is a unique id (or depth first number) of the node, used for the strongly
connected component computation.q
ffl u:lowlink is the id of a reachable node lower than u itself.
ffl u:onstack is a flag indicating that u is still on stack.
ffl u:perm is the vector - u as defined in the previous subsection.
ffl u:partition is an approximation of - u .
ffl u:status is a vector of flags that indicate which partition classes are known to
be weakly fair.
ffl u:final is a flag that indicates if u is in an scc that contains a final automaton
state. This information is propagated down on the depth first tree.
The variables u:dfnum, u:lowlink and u:onstack are maintained as in the algorithm
given in [2]. u:perm is set when u is created, while u:partition, u:status
and u:final are updated every time an edge to a successor state of u is explored.
On-tye-fly Model Checking
M1. Set the depth-first-counter to zero.
M2. Set (the initial state of B).
Set u:perm to be the identity permutation.
Conduct DF-Search(u).
M3. Exit with a No answer.
DF-Search(u) (Note that
1. Push u on to the stack, set u:onstack.
Set u:dfnum and u:lowlink to the depth-first-counter.
Increase the depth-first-counter.
2. Initialize u:partition to be the identity partition.
3. Initialize u:status with the information on disabled processes stored in the
AQS state s.
u:final if a is a final automaton state.
4. (Idle command. Later modification will use it.)
5. For each AQS edge
\Gamma! t do
7. For each automaton transition a!a 0 that is enabled in s do
8.
9. If v is already constructed and v:onstack is set then do
10. Compute the join of u:partition and the orbit partition of - e and
store it in u:partition.
Update u:status using that process i was executed.
Set u:lowlink to the minimum of u:lowlink and v:lowlink.
11. If v is not constructed yet then do
12.
13. Conduct DF-Search(v).
14. If v:onstack is still set then do
15. Compute the join of u:partition and v:partition and store it
in u:partition.
Combine v:status to u:status.
Update u:status using that process i was executed.
Set u:lowlink to the minimum of u:lowlink and v:lowlink.
u:final if v:final is set.
16. If all the partition classes are weakly fair (use u:status) and u:final
is set then exit with Yes answer.
17. If u:dfnum = u:lowlink then do
18. Pop all elements above u (inclusive) from the stack and mark the popped
vertices off-stack.
In command M2, we construct the initial state of B and invoke DF-search on this
vertex. In DF-search, the algorithm may exit with a Yes answer if a fair and final
scc is discovered. If none of the recursively called invocations of DF-search exit
with a Yes answer, the algorithm outputs a No answer and exits in command M3.
DF-search works as follows. Commands 1-3 initialize variables appropriately.
The two "for" loops in commands 5 and 7 generate the successors of the B state u.
In command 6, we invoke the routine FindEquiv to find the equivalent representative
of (t; - \Gamma1 (l)) in S aqsi . The returned (l 0 ; ae) has the property that (t; - \Gamma1 (l))
and (t; l 0 ) are equivalent under the permutation ae and the later belongs to S aqsi .
This equivalence test becomes very easy if we store the state symmetry partition
of the underlying M state t. For definition and details consult Subsect. 4.4 below.
(It is to be noted that we need this equivalence checking since we are constructing
B to be the product of M \Theta I and the automaton A, and we are doing this using
M and A. However, if we want to construct B to be M \Theta I \Theta A, as in [10], then we
do not need this equivalence checking, and in this case we may have more states in
the resulting B. For this, command 6 needs to be changed to set l 0 to - \Gamma1 (l) and
to set ae to the identity permutation.)
In command 9, we check if u ! v is a non-tree edge and u, v are in the same scc;
this is accomplished by testing that v has already been constructed (i.e. visited)
and v is still on stack. If the test is passed, the orbit partition of - e is joined with
u:partition and the result is stored in u:partition. Commands 12 through 15 are
executed if the edge is a tree edge, i.e., v is constructed (and hence visited) for
the first time. In command 12, v:perm is set; in command 13, DF-search is invoked
on v. If v and u are in the same scc (indicated by the condition in command 14)
then the partitions are joined, u:status is updated and other updates are carried
out. After processing the edge u ! v, in command 16, we check if the partially
explored scc containing u is weakly fair and has a final state; if so the algorithm
exits with a Yes answer indicating a fair computation accepted by the automaton
A is found. In command 18, after detecting the scc, we pop all the states of the scc
from the stack.
Theorem 4 The algorithm described above outputs Yes if and only if the original
program has a weakly fair computation that is accepted by A.
Proof: The proof relies on the theory developed in Subsect. 4.1 and on the correctness
of the strongly connected component algorithm of [2].
Suppose that the algorithm halts with a Yes answer. At termination the stack
contains a strongly connected subgraph of the product graph. That subgraph is
weakly fair with respect to all processes because u:partition's classes are all weakly
fair and u:partition is an approximation of (it is smaller than) - u yielding that
- u is weakly fair itself. This subgraph defines a fair run of the program that is
accepted by the automaton.
If the program terminates with a No answer then it explored the entire B graph
and found that none of the strongly connected components are satisfactory (they either
lack a final automaton state or are not fair with respect to one of the processes).
Hence, the original program had no fair run that is accepted by the automaton.
To analyze to complexity of the algorithm, we use the following notation. If K
is a graph or an automaton, then jKj denotes the number of nodes and E(K) the
number of edges or transitions. Execution of commands M1, M2 and M3 together
takes O(jI time. Commands 1-4, 12-15, 17 and are executed once for each
node. The number of B nodes is at most jM \Theta I j \Delta jAj and a single execution
of the above listed commands takes O(jI time. Thus these commands contribute
O(jM \Theta I j \Delta jAj \Delta jI j) to the over all complexity.
Now consider the execution of the commands 8-11 and 16. Every time these
commands are executed, the triple (e; l; a ! a 0 ) has a different value. Hence these
commands are executed no more than E(M) times. Each execution
of commands 8 and 16 takes O(jI time. We have implemented an algorithm for
joining the two partitions mentioned in command 10; this algorithm uses graph
data structures and has complexity O(jI j). Commands 9 and 11 require checking if
the node v has already been constructed. In our implementation, with each M state
s, we maintain a linked list of all B states whose first component is s; obviously, the
length of this list is at most jI j \Delta jAj and searching this list takes O(jI j \Delta jAj). Thus, we
see that execution of commands 8-11 and
to the over all complexity.
Finally consider command 6. Each time it is executed, the triple (e; l; a) has a
different value. Hence, the number of times it is executed is bounded by E(M) \Delta jI j \Delta
jAj. Thus command 6 contributes O(E(M ) to the over all complexity,
where x denotes the complexity of a single execution of command 6.
From the above analysis, we see that the over all complexity of the algorithm is
Note that, in the most general case, checking for state symmetry in command
6 can have exponential complexity, and hence the value of x can be exponential.
However, in our implementation we only checked for restricted forms of symmetries,
namely for those symmetries that swap two processes, and we also used the state
symmetry partitions generated during the construction of M (see next subsections).
This implementation has complexity O(jI j). Hence, for this implementation, the
over all complexity of the algorithm is O(E(M) \Delta jI
It is to be noted that if we do not invoke the equivalence check in command 6, as
explained earlier, then we will be constructing B as M \Theta I \Theta A, and exploring it.
In this case the over all complexity will also be O(E(M
4.3. State Symmetry in B, Partition Initialization, Parallel Edges
This subsection is devoted to showing that the equivalence relation - u (defined
in Subsect. 4.1, computed in u:partition) can be computed more efficiently than
presented in the basic algorithm. Improvements can be achieved by sophisticated
initialization of - u and by considering only a portion of the edges in command 5.
Let a) be a vertex of the product graph B. Processes i and j are called
u-equivalent, denoted by i
- u j, if there is a permutation ae 2 G such that
and
- u is called the local state symmetry partition at u. Intuitively,
shows that processes i and j are interchangeable in state u. Let u -;l
be an edge of B. Then u aeffi-;ae(l)
\Gamma! v is also an edge yielding that (v; - \Gamma1 (i)) is a
successor of both nodes (u; i) and (u; j) in the threaded graph B thr
. From lemma
4, it follows that (u; i) and (u; are in the same scc of B thr
. Hence, i
- u j. This
proves the next lemma.
Lemma 3 The partition
- u is smaller than
- u for every state u of the product
graph B.
This fact allows an improvement to the algorithm. First we need to project
- u to the common referential base. We define
(j).
Command 2 in DF-Search can be changed to
Initialize u:partition to be - u .
Now we describe how state symmetry can be used to remove parallel edges. Let
\Gamma! v and e
\Gamma! v be edges in B. We say that e and e 0 are parallel if
there is a permutation ae 2 G such that Surely, being
parallel is an equivalence relation on the edges. Let R r
pr be a set of representative
edges that contains at least one edge from each parallel class. When the partitions
are initialized as presented in command 2 0 , the orbit partition of - e 0 does not give
any new information after the orbit partition of - e has been considered. It is
reflected in the next lemma.
Lemma 4 If r is in an scc of B then - r is the smallest partition that contains - v
(the initial value of v:partition) for every v in the scc of r as well as the orbit
partition of - e for every edge e 2 R r
pr .
Proof: Let
\Gamma! v be an edge of the scc of r whose representative is
\Gamma! v in R r
pr . Suppose - e We show that (i; j) is contained in
the join of the orbit partition of - e 0 and - u . Using the definition of - e , we have
is the identity
permutation. Let
(i). Now - e 0
The later implies ae
(j). Hence - \Gamma1
(l)
giving l - u j.
Summing up, - e implies that there is an l such that (i; l) is in the orbit
partition of e 0 while (l; j) is in - u . Therefore, the orbit partition of e is contained
in the join of - u and the orbit partition of e 0 .
This proves that the smallest partition that contains - v for every v in the scc of
r as well as the orbit partition of - e for every edge e 2 R r
pr actually contains the
orbit partition of all edges in the scc of r. Using Theorem 2 we conclude that it
contains - r as well. The other direction follows from Proposition 1 and Lemma 3.
These ideas can be applied as follows. From each class of - u pick a representative
process and call it the leader of that class. Put R r
l is a leaderg. Since every edge is parallel to one that was caused by a leader pro-
cess, this R r
pr is a satisfactory set of representative edges. We introduce the new
vector u:leader of flags. The next improvement in the algorithm is the introduction
of command 4 and the modification of command 5.
4. Initialize u:leader.
5'. For each AQS edge
\Gamma! v if u:leader[i] is set do
4.4. State Symmetry in M
In this subsection, we show how state symmetry can also be used to reduce the
number of edges of M that are generated and stored. Let - be a state symmetry
of s, i.e.,
\Gamma! t is an edge of M , then s -ffi-(j)
\Gamma! t is also an
edge of M . This simple observation shows that we need not store both s -;j
\Gamma! t and
\Gamma! t provided that - can be efficiently computed for s.
The above idea is employed by first introducing, for each AQS state s, an equivalence
(called state equivalence) relation
among process indices defined as follows.
there is a - 2 G with
Note that in Subsect. 4.3 we introduced local state symmetry partition for B states;
the local state symmetry partition of a B state a) is denoted by
- u . (Note
that the subscript distinguishes the two notations.) We recall that i
there
is a - 2 G with j. Observe that i
Therefore, the local state symmetry partition for a B state is usually smaller than
the state equivalence relation of the underlying M state. This is caused by the fact
that a state symmetry permutation of a B state fixes not only the underlying M
state but the tracked processes as well. Nevertheless, having
- s in hand,
- u can
be easily computed.
Unfortunately, the problem of computing
- s can be a difficult task since it is
equivalent to the graph isomorphism problem. (With any given graph H , we can
associate a program P and a state s of P in a straightforward way. P has as many
processes as many nodes H has; for each pair of processes v; w, P has a variable
a[v; w] indexed by v and w; a[v; w] takes value 1 if v ! w is an edge of H , otherwise
it is 0. Now v

exactly when H has an automorphism that maps node v to
That later problem is equivalent to the graph isomorphism problem.) In many
important special cases the symmetry detection can be performed efficiently. In
general, however, only approximating solutions are available.
Let s -;j
\Gamma! t be an edge of M ,
\Gamma! t is an edge as well.
This simple observation shows that we need not store both s -;j
\Gamma! t and s -ffi-(j)
provided that - can be efficiently computed for s.
We are ready to present the last improvement to our algorithm. In the construction
of M (not shown in the algorithm) we do the following modifications. When
a new node s is created, we compute
- s . A vector s:repr is defined such that, for
every index j, it points to a representative of the
s -class of j. By the construction
of the edges of M , we store only those edges that are caused by a representative
process. (So s -;j
\Gamma! t is stored if
In our original algorithm commands 5', 12 should be changed to 5'' and 12' below,
respectively.
5 00 . For each stored AQS edge
\Gamma! t and each process i with
and u:leader[i] is set, compute some - 2 G with
then do
As it has been pointed out earlier, in general, computing
- s is computationally
hard. However, we have implemented a method where we only look for state sym-
metries, i.e. permutations, which only interchange two process indices; computing
all such symmetries and the corresponding equivalence relation
- s can be done ef-
ficiently. The same approach is employed in computing the state symmetries in B.
Also note that in step 5" of the algorithm, it is enough if we find one permutation
- satisfying the given property; we do not have to compute all such permutations.
Since, for the case of state symmetry, we are restricting the class of permutations to
be those that only interchange two process indices, step 5" can also be implemented
efficiently.
Concluding this section, we illustrate the concept of state symmetry and redundant
edges by showing M of our simplified Resource Controller after deleting all
redundant edges.
OEAE
iii-
rii
OEAE
oe id; 1id\Gamma
\Gamma\Psi
\Gamma\Psi
\Gamma\Psi
Figure

5. The AQS M without redundant edges
Consider Figure 5. The top row in each circle shows the local states of the three
processes while the bottom row lists the representative processes. The compressed
M has 16 edges while the original had 27.
5. Implementation
We have developed a prototype of the on-the-fly model checker implementing the
above presented algorithm. We have used efficient approximation techniques to
check equivalence of two states when generating the AQS and also in the main
algorithm where we had to check for equivalence of B states. For the case of
complete symmetries, as in the Resource Controller and Readers/Writers examples,
this approximation algorithm will indicate two states to be equivalent whenever
they are equivalent. For other types of symmetry, these approximation methods
may sometime indicate two states to be inequivalent although they are equivalent.
In such cases, we may not get maximum possible reduction in the size of the state
space; however, our algorithm will still correctly indicate if the concurrent system
satisfies the correctness specification or not.
We used the implemented system to check for the correctness of the Resource
Controller example, the Readers Writers example, and the Ethernet Protocol with
various number of users.
We contrasted our new system with the old model checker that implements the
results presented in [10] on the Resource Controller example. We checked many
properties including the liveness property that every user process that requests a
resource will eventually access the resource, and the mutual exclusion property.
Dramatic improvement was detected in all performance measures as indicated in

Table

below. The product graphs constructed by the old and new model
checker are referred to as B 0 and B respectively. Each statistic is given as a=b
where a and b are the numbers corresponding to the old and new model checker
respectively.

Table

1. Statistics for checking a liveness property
Eventually Access 10 50 100
AQS states 38 / 38 198 / 198 398 / 398
AQS transitions 235 / 107 6175 / 1567 24850 / 5642
Explored
Total memory used (kbyte) 31 / 13 1219 / 216 6878 / 830
Total CPU time used (sec) 0 / 0 37 / 6 481 / 42

Table

2. Statistics for checking a safety property
Mutual
AQS states 38 / 38 198 / 198 398 / 398
AQS transitions 235 / 107 6175 / 1567 24850 / 5642
Explored
Total memory used (kbyte)
Total CPU time used (sec) 0 / 0
The liveness property we checked is not satisfied by the Resource Controller.
Both model checkers found a fair incorrect computation. From the table, we see
that the number of AQS states are the same, while the number of AQS transitions
is much smaller in the new model checker due to the use of state symmetry. The
number of product states explored in the on-the-fly system is much smaller since
it terminated early. On the other hand the original model checker constructed the
before checking for an incorrect fair computation.
For the mutual exclusion property, both model checkers indicated that the Resource
Controller satisfies that property. In this case, early termination does not
come into effect. Furthermore, since we do not track any process (mutual exclusion
is a global property), the number of states explored in B 0 and B are the same.
However, the number of transitions is much smaller in M as well as in B due to
the effect of state symmetry. The over all CPU time and the memory usage are
substantially smaller for the new model checker.
6. Conclusions
In this paper, we have presented an on-the-fly model checking system that exploits
symmetry (between states as well as inside a state) and checks for correctness under
fairness.
Symmetry based reduction has been shown to be a powerful tool for reducing the
size of the state space in a number of contexts. For example, such techniques have
been employed in the Petri-net community [14, 15] to reduce the size of the state
space explored. Such techniques have also been used in protocol verification [1, 16]
and in hardware verification [13] and in temporal logic model checking [5, 9, 10].
There have been on-the-fly model checking techniques [3, 11, 12, 17] that employ
traditional state enumeration methods. Some of them [11, 12, 17] also use other
types of state reduction techniques. To the best of our knowledge, ours is the first
approach that performs on-the-fly model checking under fairness for the full range
of temporal properties and that exploits symmetry.
As part of future work, we plan to explore techniques to automatically detect
symmetries and integrate these techniques with the model checker. Also, algorithms
for checking equivalence of global states under other types of symmetry need to be
further explored.



--R

"A Calculus for Protocol Specification and Validation"
"The Design and Analysis of Computer Algorithms"
"Efficient On-the-Fly Modelchecking for CTL"
"Automatic Verification of Finite State Concurrent Programs Using Temporal Logic: A Practical Approach"
"Exploiting Symmetry in Temporal Logic Model Check- ing"
"Analyzing Concurrent Systems using the Concurrency Workbench, Functional Programming, Concurrency, Simulation, and Automated Reasoning"
"Introduction to Algorithms"
"Generation of Reduced Models for checking fragments of CTL"
"Symmetry and Model Checking"
"Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach"
"Partial-Order Methods for the Verification of Concurrent Systems"
"The State of SPIN"
"Better Verification through Symmetry"
"Colored Petri Nets: Basic Concepts, Analysis Methods, and Practical Use"
"High-level Petri Nets: Theory and Application"
"Testing Containment of omega-regular Languages"
"Computer Aided Verification of Coordinated Processes: The Automata Theoretic Approach"
--TR

--CTR
A. Prasad Sistla , Patrice Godefroid, Symmetry and reduced symmetry in model checking, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.4, p.702-734, July 2004
Sharon Barner , Orna Grumberg, Combining symmetry reduction and under-approximation for symbolic model checking, Formal Methods in System Design, v.27 n.1/2, p.29-66, September 2005
Alice Miller , Alastair Donaldson , Muffy Calder, Symmetry in temporal logic model checking, ACM Computing Surveys (CSUR), v.38 n.3, p.8-es, 2006
model checking;automata;symmetry reduction;state explosion;verification