Generische Implementierung zur Überdeckung in wohlstrukturierten Transitionssystemen

Zusammenfassung

Potentiell unendliche Transitionssysteme  sind im Allgemenien schwierig zu Analysiren, treten aber z.B. bei der Verifikation von Computersystemen natürlicherweise auf.

Sogenannte wohlstrukturierte Transitionsysteme (WSTS) sind eine sehr allgemeine Klasse von unendlichen Transitionsystemen dar.

Diese sind zusätzlich mit einer zur Transitionsrelation kompatiblen Wohlquasiordnung auf dem Zustandsraum ausgestattet. Viele Probleme der Verifikation können auf die Frage reduziert werden ob von einem gegebenen Startzustand in einem WSTS ein Zustand erreichbar ist, der gemäß der Ordnungsrelation größer oder gleich dem Startzustand ist.

Das Ziel der Bachelorarbeit ist die Implementierung einer Sättingungsmethode (in Java oder Scala), die dieses Überdeckungsproblem löst. 

Anforderungen

Die Arbeit soll nicht neue theoretische Konzepte erarbeiten oder bestehende theoretische
Probleme lösen, stattdessen steht das Verständnis und die Anwendung der bereits vor-
handenen Theorie im Vordergrund. Es soll darüber hinaus keine Komplexitätsabschät-
zung erfolgen. Auch ist klarzustellen, dass nicht explizit Petrinetze untersucht werden,
sondern die algorithmische Analyse einer allgemeinen Klasse von Graphen.

Literatur (Auswahl)

• „Well-structured transition systems everywhere“ von A. Finkel und Ph. Schnoebelen. Ein Artikel, welcher eine ausführliche Übersicht über das Gebiet der wohl-strukturierten Transitionssysteme liefert.
• „The Theory of Well-Quasi-Ordering: A Frequently Discovered Concept“ von Joseph B. Kruskal. Erläutert die Theorie der Wohl-Quasi-Ordnung anhand der Definition von partiell geordneten Mengen, auch wohl-partiell-geordnet genannt.
• „Fundamental Structures in Well-Structured Infinite Transition Systems“ von Alain Finkel und Philippe Schnoebelen. Eine Ausführliche Abhandlung über die Definition von Wohl-Strukturierten Transitionssystemen. Es wird u. a. von den Petrinetzen ausgehend eine allgemeine Definition von Wohl-Strukturierten Systemen vorgestellt und erläutert. Auch werden Sättigungsmethoden behandelt, mit deren Hilfe eine wohl-geordnete Menge berechnet werden kann.