<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>8558</REFNUM><AUTHORS><AUTHOR>Miller,A.</AUTHOR><AUTHOR>Donaldson,A.</AUTHOR></AUTHORS><YEAR>2007</YEAR><TITLE>Symmetry Reduction Methods for Model Checking</TITLE><PLACE_PUBLISHED>Proceedings of the 14th workshop on Automated Reasoning</PLACE_PUBLISHED><PUBLISHER>N/A</PUBLISHER><LABEL>Miller:2007:8558</LABEL><KEYWORDS><KEYWORD>Verification</KEYWORD></KEYWORDS<ABSTRACT>Model checking is a widely used automatic method for system verification. Verification of even moderately large systems can be difficult due to an exponential growth in the number of states with the number of components. This phenomenon is known as state space explosion. Many systems, however, consist of clusters of sets of identical (up to process id) components, resulting in symmetry of the underlying state space. If this symmetry can be detected it can often be exploited to reduce the cost of model checking sufficiently to allow for full verification. We describe what is meant for a model checker to be explicit state or symbolic, timed or probabilistic, and illustrate these terms via an overview of four of the most widely used model checkers: SPIN, SMV, PRISM and UPPAAL. We then show, via a simple example, how symmetry reduction can be helpful to reduce the cost of model checking in the explicit state case, and describe two problems associated with symmetry reduced model checking, namely symmetry detection and the orbit problem. We show how we have addressed these problems with our own symmetry detection and reduction tools for SPIN: SymmExtractor and TopSpin, and discuss the problems associated with symmetry reduction methods in the symbolic case.</ABSTRACT></RECORD></RECORDS></XML>