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: |
| |||||||
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 |