Dokument: On Symmetry Reduction in Model Checking via Graph Canonicalisation

Titel:	On Symmetry Reduction in Model Checking via Graph Canonicalisation
URL für Lesezeichen:	https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=13949
URN (NBN):	urn:nbn:de:hbz:061-20100202-120537-6
Kollektion:	Dissertationen
Sprache:	Englisch
Dokumententyp:	Wissenschaftliche Abschlussarbeiten » Dissertation
Medientyp:	Text
Autor:	Spermann, Corinna [Autor]
Dateien:	[Dateien anzeigen] Adobe PDF [Details] 23,86 MB in einer Datei [ZIP-Datei erzeugen] Dateien vom 29.01.2010 / geändert 29.01.2010
Beitragende:	Prof. Dr. Michael Leuschel [Betreuer/Doktorvater] Prof. Dr. Rothe, Jörg [Gutachter]
Stichwörter:	Model Checking, Symmetry Reduction
Dewey Dezimal-Klassifikation:	500 Naturwissenschaften und Mathematik » 510 Mathematik
Beschreibungen:	Diese Doktorarbeit setzt die Arbeit über Symmetriereduktion für Modelchecking in B fort. Sie nimmt die Idee auf, Zustände in Graphen zu übersetzen, sodass symmetrische Zustände 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 Lösung dieses Problems erst noch gefunden werden muss. Jedoch gibt es Werkzeuge, die fähig sind isomorphe Graphen mittels Graph Normalisierung zu entdecken. Eines dieser Werkzeuge heißt NAUTY und wird über 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. This thesis continues the work on symmetry reduction for model checking in B. It picks up the idea of translating states into graphs, such that symmetric states correspond exactly to isomorphic graphs. This reduces the orbit problem in symmetry reduction to the graph isomorphism problem. The graph isomorphism problem is a well-studied mathematical problem, although a polynomial time algorithm to solve it has yet to be found. However, existing tools are capable of detecting isomorphic graphs via graph canonicalisation very efficiently. One of these tools, named NAUTY, is integrated through an interface into the ProB model checker. This new way of applying graph canonicalisation in model checking is then compared empirically with the already existing symmetry reduction approaches in ProB.
Lizenz:	Urheberrechtsschutz
Fachbereich / Einrichtung:	Mathematisch- Naturwissenschaftliche Fakultät » WE Informatik » Softwaretechnik und Programmiersprachen
Dokument erstellt am:	29.01.2010
Dateien geändert am:	29.01.2010
Promotionsantrag am:	30.11.2009
Datum der Promotion:	20.01.2010