Eingang zum Volltext
Urheberrechtshinweis / Copyright notice Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgendeURN: urn:nbn:de:kobv:co1-opus-10294
URL: http://opus.kobv.de/btu/volltexte/2009/1029/
Tovchigrechko, Alexey
Efficient symbolic analysis of bounded Petri nets using Interval decision diagrams
Effiziente symbolische Analyse von beschränkten Petrinetzen mit Hilfe von Interval decision diagrams
| pdf-Format: |
|
Kurzfassung in Deutsch
Der Schwerpunkt dieser Arbeit liegt bei verschiedenen Techniken, die Effizienz der symbolischen Petrinetzanalyse steigern können.Reduced ordered interval decision diagrams (ROIDDs) werden eingesetzt um Zustandsmengen von k-beschränkten Netzen zu codieren. Wir beschreiben Implementierung eines ROIDD-Packetes und spezielle ROIDD-Operationen, die in symbolischen Algorithmen verwendet werden. Wir untersuchen dann wie Effizienz der symbolischen Erreichbarkeitsanalyse verbessert werden kann und präsentieren einen neuen Saturation-Ansatz, der Strukturen von ROIDDs und k-beschränkten P/T-Netzen ausnutzt. Der Ansatz erlaubt Diagrammgrößen kleiner zu halten und kann Effizienz der symbolischen Analyse drastisch steigern. Saturation-basierte Techniken werden bei den Aufzählungen von stark zusammenhängenden Komponenten und Modelchecking eingesetzt.
Implementierung von symbolischen Modelcheckers für k-beschränkte P/T-Netzte wird beschrieben. Wir betrachten CTL- und einen neuartigen LTL-Modelchecker. Eine Reihe von Techniken zur Effizienzsteigerung der Implementierung wird betrachtet.
Kurzfassung in Englisch
The research in this thesis focuses on different techniques which can improve efficiency of the symbolic analysis of Petri nets.Reduced ordered interval decision diagrams (ROIDDs) are employed to encode sets of states of k-bounded nets. We discuss implementation of an ROIDD package and special ROIDD operations needed in symbolic algorithms. We study then how to improve efficiency of the reachability analysis and propose a new saturation approach, which exploits the structure of ROIDDs and the structure of k-bounded P/T nets. It manages to keep sizes of intermediate diagrams smaller than other approaches and can drastically improve efficiency of the symbolic analysis. Saturation techniques are applied in the enumeration of strongly connected components and in model checking.
Implementation of symbolic model checkers for k-bounded P/T nets are discussed. We consider CTL and a novel LTL model checker. A number of techniques to improve efficiency of the implementation are considered.
| SWD-Schlagwörter: | Petri-Netz , Model Checking | |
| Freie Schlagwörter (deutsch): | Petrinetze , Symbolische Analyse , Entscheidungsdiagramme , Model Checking | |
| Freie Schlagwörter (englisch): | Petri nets , Symbolic analysis , Decision diagrams , Model checking | |
| Collection | BTU / Wiss. Publikationen | |
| Institut: | LS Informatik / Datenstrukturen und Softwarezuverlässigkeit | |
| Fakultät: | Fakultät für Mathematik, Naturwissenschaften und Informatik | |
| DDC-Sachgruppe: | Informatik | |
| Dokumentart: | Dissertation | |
| Hauptberichter: | Heiner, Monika Prof. Dr.-Ing. | |
| Sprache: | Englisch | |
| Tag der mündlichen Prüfung: | 16.10.2008 | |
| Erstellungsjahr: | 2009 | |
| Publikationsdatum: | 05.10.2009 |
