On symmetry reduction in model checking via graph canonicalisation.
Corinna Spermann · Univ. Duesseldorf: Duesseldorfer Dokumenten- und Publikationsserver · 2009
Diese Doktorarbeit setzt die Arbeit uber Symmetriereduktion fur Modelchecking in B fort. Sie nimmt die Idee auf, Zustande in Graphen zu ubersetzen, sodass symmetrische Zustande genau isomorphen Graphen entsprechen. Dies reduziert das Orbit Problem in Symmetriereduktion auf das Graph Isomorphie Problem. Das Graph Isomorphie Problem ist ein gut studiertes mathematisches Problem, obwohl ein polynomialer Algorithmus zur Losung dieses Problems erst noch gefunden werden muss. Jedoch gibt es Werkzeuge, die fahig sind isomorphe Graphen mittels Graph Normalisierung zu entdecken. Eines dieser Werkzeuge heist NAUTY und wird uber ein Interface in den ProB Model Checker integriert. Dieser neue Weg die Graph Normalisierung in Model Checking anzuwenden, wird dann mit den bereits existierenden Methoden zur Symmetriereduktion in ProB verglichen.