Title: Symmetry and Model-checking
                             A. Prasad Sistla

Electronic mail: sistla@surya.eecs.uic.edu

Abstract: Much research has been conducted on using temporal logic
model checking for automatic verification of finite state concurrent
programs. In this approach, the global state graph of a concurrent
program is constructed (explicitly or implicitly) and then its
correctness against a temporal logic specification is checked using
efficient algorithms.  The main bottleneck for this approach is the
state explosion problem, i.e. the rapid explosion (exponential) in the
number of states to be explored.

One of the major techniques for containing the state explosion problem
is to exploit symmetries in the concurrent program.  We outline a
number of results on exploiting such symmetries for model-checking.
Symmetries in the concurrent program induce an equivalence relation on
the state space. One approach is to construct a quotient structure
corresponding to this equivalence relations and perform model-checking
on the quotient structure.  In order to make this approach work, in
general, we also need to consider the symmetries in the temporal logic
formula. We show how the symmetries in the program as well as the
formula can be used for model-checking purposes.  We also outline a
second approach where we only consider program symmetry and construct
a Annotated Quotient Structure (AQS).  The AQS can be partially
unwound to check the correctness of any given formula. More
importantly, it can be used to check for correctness under different
fairness conditions.  The AQS can be extended and used for
verification of asymmetric systems also.