Navigation

ba_unerreichbarkeit

Implementierung eines Algorithmus zur Feststellung von Unerreichbarkeit bei Petrinetzen

Bachelor-Arbeit

Betreuer: Harro Wimmel

Zusammenfassung der Abschlusspräsentation:

Petrinetze bieten eine Vielzahl an Modellierungsmöglichkeiten in der Informatik, aber auch in anderen Bereichen finden Petrinetze Verwendung zur Beschreibung von dynamischen Systemen. Viele Eigenschaften von Petrinetzen lassen Rückschlüsse auf das System, welches sie beschreiben, zu. So kann auch die Feststellung, ob eine Markierung in einem Petrinetz erreichbar oder unerreichbar ist, eine wichtige Information für das Petrinetz darstellen. Diese Fragestellung ist als das
Erreichbarkeitsproblem bekannt.

Einen Algorithmus zur Entscheidung des Erreichbarkeitsproblems stellt
Jérôme Leroux in seinem Paper  The General Vector Addition System Reachability Problem by Presburger Inductive Invariants  vor. Der Algorithmus besteht aus zwei nebenläufigen Teilalgorithmen, von denen einer die Erreichbarkeit und der andere die Unerreichbarkeit einer Markierung in einem Petrinetz feststellt. Die Feststellung der Erreichbarkeit basiert auf dem Aufspannen eines Erreichbarkeitsgraphen mittels Breitensuche. Die Unerreichbarkeit wird festgestellt, indem eine Presburger Formel gesucht wird, welche Invariant bezüglich des Feuerns von Transitionen ist, jedoch Start- und Zielmarkierung unterscheidet. Da potentiell eine unendliche Menge von Presburger Formeln auf dieses Verhalten untersucht werden muss, ist eine Effiziente Erzeugung von Presburger Formeln nötig, um ein möglichst performante Implementierung des Algorithmus von Jérôme Leroux zu ermöglichen.

Ziel der Bachelorarbeit war es, Presburger Formeln zur Verwendung im Algorithmus von Jérôme Leroux optimiert zu Erzeugen. Der Vortrag wird eine kurze Einführung in Petrinetze und Presburger Arithmetik beinhalten, welche notwendig für das weitere Verständnis des Vortrags sind. Anschließend wird der zweite Teilalgorithmus zur Feststellung der Unerreichbarkeit vorgestellt, um danach die Vorgehensweise zur Erzeugung der Presburger Formeln und die dabei vorgenommenen Optimierungen zu erläutern.

Zusammenfassung der ersten Präsentation:

Das Erreichbarkeitsproblem von Petrinetzen ist ein zentrales Problem der Petrinetztheorie, auf welches sich viele rechenintensive Probleme zurückführen lassen. Während sich die Erreichbarkeit vergleichsweise intuitiv durch das Aufspannen eines Erreichbarkeitsgraphen semientscheiden lässt, fällt der Algorithmus zum Nachweis der Nichterreichbarkeit wesentlich komplexer aus. Thema der Bachelorarbeit ist die Implementierung des von Jérôme Leroux in seiner Publikation "The General Vector Addition System Reachability Problem by Presburger Inductive Invariants" vorgestellten Algorithmus. Im Vortrag wird es zum besseren Verständnis einen kurzen Exkurs zu Petrinetzen und zur Presburger Arithmetik geben, um danach den Algorithmus von Jérôme Leroux in groben Zügen vorzustellen. Anschließend wird die bisherige und geplante Vorgehensweise präsentiert. Dabei wird auf die verwendeten Tools,Optimierung bezüglich der Laufzeit sowie erwartete oder aufgetretene Problemstellungen eingegangen.

Webmay6asaclter (mahyorcoobzz.grawjiundet9tr@uhgtvol.dechud1) (Stand: 07.11.2019)