<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>9013</REFNUM><AUTHORS><AUTHOR>Donaldson,A.F.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2008</YEAR><TITLE>Automatic Symmetry Detection for Promela</TITLE><PLACE_PUBLISHED>Journal of Automated Reasoning, Volume 41, Issue 3-4</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>251--293</PAGES><ISBN>1573-0670</ISBN><LABEL>Donaldson:2008:9013</LABEL><KEYWORDS><KEYWORD>Symmetry reduction</KEYWORD></KEYWORDS<ABSTRACT>We introduce a specification language, Promela-lite, which captures the essential features of Promela but which, unlike Promela, has a formally defined semantics. We show how we can detect symmetry in specifications defined in Promela-lite by constructing a directed, coloured bipartite digraph called a static channel diagram, and applying computational group theoretic techniques. We extend our approach to Promela and introduce a tool, SymmExtractor, for automatically detecting symmetries of Promela specifications. We demonstrate the effectiveness or our approach via experimental results for a suite of Promela specifications. Unlike previous approaches our technique is fully automatic, and not restricted to fully symmetric systems.</ABSTRACT><URL>http://www.springerlink.com/content/h81k12633l323g36/</URL></RECORD></RECORDS></XML>