We present four versions of a new heuristic for coping with the problem of finding (canonical) representatives of symmetry equivalence classes (the so-called orbit problem), in symmetry techniques for model checking. The practical implementation of such techniques hinges on appropriate workarounds of this hard problem, which is equivalent to graph isomorphism. We implemented the four strategies on top of the Spin model checker, and compared their performance on several examples, with encouraging results.
|Title of host publication||FME 2001: Formal Methods for Increasing Software Productivity (International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings)|
|Editors||J. Nuno Oliveira, P. Zave|
|Place of Publication||Berlin|
|Publication status||Published - 2001|
|Name||Lecture Notes in Computer Science|