Analyse von Petri-Netz Modellen mit Entscheidungsdiagrammen

Petri-Netze sind ein gut geeignetes Beschreibungsmittel füur verteilte Systeme. Sie vereinen die Vorteile eines grafischen Beschreibungsmittels und eines mathematisch präzisen und daher analysierbaren Formalismus. Das Ziel der Arbeit war es, Algorithmen für ein Werkzeug zur automatischen Verifikation von Eigenschaften eines Petri-Netz Modells zu entwickeln. Die zu überprüfenden Eigenschaften der Modelle werden dazu je nach Netzklasse durch Aussagenlogik, Prädikatenlogik oder Intervallogik, ergänzt um den modalen mu-Kalkül, formuliert. Der Algorithmus zur Auswertung der Formeln des modalen mu-Kalküls orientiert sich in naheliegender Weise an der Definition der Semantik. Um diesen Algorithmus (effizient) implementieren zu können, ist eine geeignete Datenstruktur zur Repräsentation von Markierungsmengen erforderlich. Hierzu werden zwei Varianten von geordneten binären Entscheidungsdiagrammen (Ordered Binary Decision Diagrams, OBDDs) entwickelt. OBDDs sind eine Datenstruktur zur kompakten und kanonischen Repräsentation von Booleschen Funktionen. Sie eignen sich daher auch sehr gut zur Darstellung von Markierungsmengen in B/E-Netzen. Zur Repräsentation von Markierungsmengen in S/T-Netzen werden geordnete natürliche Entscheidungsdiagramme (Ordered Natural Decision Diagrams, ONDDs) entwickelt. Pr/T-Netze werden hier auf der Basis ihrer Entfaltung analysiert. Die Tatsache, daß bei dieser Entfaltung viele sich wiederholende Teilnetze mit gleicher Struktur entstehen, hat die Entwicklung von geordneten hierarchischen Entscheidungsdiagrammen (Ordered Hierarchical Decision Diagrams, OHDDs) motiviert. An den untersuchten Beispielen wird deutlich, daß OHDDs einen wesentlichen Effizienzgewinn gegenüber den OBDDs mit sich bringen. Die vorgestellten Datenstrukturen und Algorithmen sind jedoch keinesfalls auf die Verwendung bei der Analyse von Petri-Netz Modellen beschränkt. Vielmehr können sie bei vielen Problemen, die sich auf der Basis von Booleschen Funktion formulieren lassen, hilfreich sein. Weiterhin wird in der Arbeit diskutiert, inwieweit die Konvergenz der Fixpunktalgorithmen zur Auswertung der Formeln des modalen mu-Kalküls durch strukturelle Analysetechniken für Petri-Netze beschleunigt werden kann.