Efficient symbolic analysis of bounded Petri nets using Interval decision diagrams
Alexey A. Tovchigrechko · 2008
Der Schwerpunkt dieser Arbeit liegt bei verschiedenen Techniken, die Effizienz der symbolischen Petrinetzanalyse steigern konnen. Reduced ordered interval decision diagrams (ROIDDs) werden eingesetzt um Zustandsmengen von k-beschrankten 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 prasentieren einen neuen Saturation-Ansatz, der Strukturen von ROIDDs und k-beschrankten P/T-Netzen ausnutzt. Der Ansatz erlaubt Diagrammgrosen kleiner zu halten und kann Effizienz der symbolischen Analyse drastisch steigern. Saturation-basierte Techniken werden bei den Aufzahlungen von stark zusammenhangenden Komponenten und Modelchecking eingesetzt. Implementierung von symbolischen Modelcheckers fur k-beschrankte P/T-Netzte wird beschrieben. Wir betrachten CTL- und einen neuartigen LTL-Modelchecker. Eine Reihe von Techniken zur Effizienzsteigerung der Implementierung wird betrachtet.