Utilizing Symmetry when Model Checking
                 under Fairness Assumptions:
               An Automata-theoretic Approach
    
                      E. Allen Emerson
                University of Texas at Austin
                


One valuable technique for combating the state explosion problem
is to exploit symmetry when performing temporal logic model checking.
In previous work it has been shown how, using some basic notions
of group theory, symmetry may be exploited 
for the full range of correctness properties expressible in the 
very expressive temporal logic CTL*. The method can be particularly
useful for systems composed of many isomorphic processes or subcomponents.
The global state transition graph of such a system often exhibits
a great deal of symmetry, characterized by its group of automorphisms. 
The basic idea is to reduce model checking over the original, 
large structure to model checking over the smaller quotient structure,
where symmetric states are identified.
Surprisingly, while fairness properties are readily expressible
in CTL*, these methods are not powerful
enough to admit any amelioration of state explosion,
when fairness assumptions are involved.
This problem arises from the need to respect not only the symmetry
of the state graph but also the "internal" symmetry of the specification.


We describe an alternative automata-theoretic approach to 
exploiting symmetry of the state graph that is not limited by
the internal symmetry of the specification. The idea is to
annotate the quotient structure  with ``guides'', indicating how coordinates 
are permuted from one state to the next in the quotient. An automaton
for the specification can be modified into another automaton  to run over
the quotient using the guides to keep track of shifting coordinates.
By itself, the automata-theoretic approach is not adequate for
handling fairness; however, we give a nontrival generalization,
where permutations are concretely realized by "threads", which
does cater for efficient model checking over the quotient graph
under fairness assumptions. (This is joint work with A. Prasad Sistla.)