@phdthesis{Tovchigrechko2009, author = {Tovchigrechko, Alexey}, title = {Efficient symbolic analysis of bounded Petri nets using Interval decision diagrams}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:co1-opus-10294}, school = {BTU Cottbus - Senftenberg}, year = {2009}, abstract = {Der Schwerpunkt dieser Arbeit liegt bei verschiedenen Techniken, die Effizienz der symbolischen Petrinetzanalyse steigern k{\"o}nnen. Reduced ordered interval decision diagrams (ROIDDs) werden eingesetzt um Zustandsmengen von k-beschr{\"a}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{\"a}sentieren einen neuen Saturation-Ansatz, der Strukturen von ROIDDs und k-beschr{\"a}nkten P/T-Netzen ausnutzt. Der Ansatz erlaubt Diagrammgr{\"o}ßen kleiner zu halten und kann Effizienz der symbolischen Analyse drastisch steigern. Saturation-basierte Techniken werden bei den Aufz{\"a}hlungen von stark zusammenh{\"a}ngenden Komponenten und Modelchecking eingesetzt. Implementierung von symbolischen Modelcheckers f{\"u}r k-beschr{\"a}nkte P/T-Netzte wird beschrieben. Wir betrachten CTL- und einen neuartigen LTL-Modelchecker. Eine Reihe von Techniken zur Effizienzsteigerung der Implementierung wird betrachtet.}, subject = {Petri-Netz; Model Checking; Petrinetze; Symbolische Analyse; Entscheidungsdiagramme; Model Checking; Petri nets; Symbolic analysis; Decision diagrams; Model checking}, language = {en} }