TY - THES A1 - Tovchigrechko, Alexey T1 - Efficient symbolic analysis of bounded Petri nets using Interval decision diagrams T1 - Effiziente symbolische Analyse von beschränkten Petrinetzen mit Hilfe von Interval decision diagrams N2 - 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. N2 - 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. KW - Petri-Netz KW - Model Checking KW - Petrinetze KW - Symbolische Analyse KW - Entscheidungsdiagramme KW - Model Checking KW - Petri nets KW - Symbolic analysis KW - Decision diagrams KW - Model checking Y1 - 2009 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:co1-opus-10294 ER -