Überreichung des Fakultätspreises Mathematik und Informatik

Dr. Robin Bergenthum vom Lehrgebiet Softwaretechnik und Theorie der Programmierung erhält seine Auszeichnung im Rahmen des öffentlichen Fakultätskolloquiums am 24. November.


Preisträger referiert über die „Verifikation von halbgeordneten Abläufen in Petrinetzen“

Am Montag, 24. November, erhält Dr. Robin Bergenthum, Lehrgebiet Softwaretechnik und Theorie der Programmierung (Prof. Dr. Jörg Desel) den Preis der Fakultät Mathematik und Informatik der FernUniversität in Hagen überreicht. Die Ehrung, bei der der Preisträger auch den Vortrag „Verifikation von halbgeordneten Abläufen in Petrinetzen“ hält, findet im Fakultätskolloquium Mathematik und Informatik unter dem Dach des Hagener Forschungsdialogs der FernUniversität statt. Veranstaltungsort ist ab 17 Uhr das Seminargebäude der FernUniversität, R. 4. und 5, Universitätsstr. 33, 58097 Hagen. Die Veranstaltung ist öffentlich.

Illustration

Bei dem Vortrag von Dr. Bergenthum geht es um 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.

Weitere Informationen: Dekanatsbüro der Fakultät für Mathematik und Informatik, Tel.: 02331/987 – 1700 oder – 2594, oder Dr. Bergenthum, Tel.: 02331/987 – 1773.

Gerd Dapprich | 22.10.2014