Employing symmetry reductions in model checking

This paper presents a survey of research work that has been done over the last decade on exploiting symmetry in model checking of concurrent systems. It describes the techniques based on Quotient Structures, Annotated Quotient Structures and Guarded Quotient Structures. It also briefly describes some of the implemented systems.