<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>7904</REFNUM><AUTHORS><AUTHOR>Donaldson,A.F.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2005</YEAR><TITLE>Automatic Symmetry Detection for Model Checking Using Computational Group Theory</TITLE><PLACE_PUBLISHED>Proceedings of the 13th International Symposium on Formal Methods Europe (FME 2005). Lecture Notes in Computing Science volume 3582.</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>481--496</PAGES><LABEL>Donaldson:2005:7904</LABEL><KEYWORDS><KEYWORD>Promela/SPIN; symmetry reduction; communicating processes; distributed systems; formal modelling; GAP; concurrency</KEYWORD></KEYWORDS<ABSTRACT>We present an automatic technique for the detection of structural symmetry in a model directly from its Promela specification. Our approach involves finding the static channel diagram of the model, a graphical representation of channel-based communication; computing the group of symmetries of this diagram; and computing the largest possible subgroup of these symmetries which induce automorphisms of the underlying model. We describe a tool, SymmExtractor, which, for a given model and LTL property, uses our approach to find a group of symmetries of the model which preserve the property. This group can then be used for symmetry reduction during model checking using existing quotient-based methods. Unlike previous approaches, our method can detect arbitrary structural symmetries arising from the communication structure of the model.</ABSTRACT></RECORD></RECORDS></XML>