Kolloquium der Fakultät für Mathematik und Informatik und Verleihung des Fakultätspreises 2014

Termin: 24.11.2014

 

• Einführung
• Vortrag
• Verleihung des Förderpreises

Der Vortrag fand im Rahmen des Hagenener Forschungsdialogs statt.

Abstract:
Die vorliegende Arbeit behandelt das Problem der Verifikation eines halbgeordneten Ablaufs in einem Petrinetz. Petrinetze sind ein anerkannter Formalismus, um nebenläufige Systeme integriert darzustellen.

Ein Ablauf formuliert eine Verhaltens-Spezifikation und es stellt sich die Frage, ob diese im Petrinetz wahr bzw. erfüllt ist. Petrinetze werden in dieser Arbeit in ihrer allgemeinen Form der markierten Stellen/Transitions-Netze verwendet, der Ablauf wird als Szenario dargestellt. Ein Szenario ist eine Menge von Ereignissen zusammen mit einer Halbordnung auf dieser Menge. Ein Szenario beschreibt im Gegensatz zu sequentiellen Ablaufmodellen nicht nur eine Folge von Ereignissen, sondern stellt beliebige Abhängigkeiten und Unabhängigkeiten zwischen Ereignissen dar. Aus diesem Grund lässt sich nebenläufiges oder verteiltes Verhalten mithilfe eines Szenarios intuitiv und leicht spezifizieren. Die Frage danach, ob ein Szenario Verhalten eines Stellen/Transitions-Netz beschreibt, ist das Szenario-Verifikations-Problem.

Ein Szenario beschreibt Verhalten eines markierten Stellen/Transitions-Netzes, wenn es in dessen Szenario-Sprache enthalten ist. In der Literatur existieren drei verschiedene Möglichkeiten, diese Sprache zu charakterisieren. Aus jeder Charakterisierung kann man einen Verifikations-Algorithmus ableiten, mit dem sich das Szenario-Verifikations-Problem entscheiden lässt. Je nach Probleminstanz besitzen diese Algorithmen sehr unterschiedliche Laufzeiten. In dieser Arbeit werden die Charakterisierungen der Szenario-Sprache vorgestellt und die sich aus ihnen ergebenden Verifikations-Algorithmen verglichen.

Außerdem wird eine vierte, für das Problem der Verifikation optimierte Charakterisierung der Szenario-Sprache entwickelt, und mit deren Hilfe ein Verfahren vorgestellt, dass das Szenario-Verifikations-Problem für jede Probleminstanz effizient entscheidet.

FernUniversität in Hagen, ZMI, 58084 Hagen, E-Mail: viedeostreaming(at)fernuni-hagen.de