Einladung zur hochschulöffentlichen Disputation

von Herrn Frank Heitmann

Mittwoch, 3. Juli 2013, 10 Uhr s.t.

Informatikum, Vogt-Kölln-Str. 30, Haus C, Raum 221

“Algorithmen und Komplexitätsresultate für Objektnetze”

Zusammenfassung:

Objektsysteme sind Petrinetze, deren Marken eine innere Aktivität haben können und dazu selbst wieder als Petrinetz modelliert werden. Das dadurch entstehende Netzsystem hat eine mehrstufige Struktur und erlaubt in einer Variante ferner den vertikalen Transport von Marken. Diese Formalismen, die Spezialfälle und Erweiterungen eines ursprünglich von Valk eingeführten Formalismus sind, sowie ähnliche von anderen Arbeitsgruppen eingeführte Formalismen, sind bei der Modellierung von Anwendungen nützlich, bei denen die Mobilität von Objekten und die Interaktionen zwischen diesen Objekten von Bedeutung sind.

Im Zentrum dieser Arbeit steht die Frage, wie der im allgemeinen Fall Turing-mächtige Formalismus so eingeschränkt werden kann, dass die Möglichkeiten der Modellierung weitestgehend erhalten bleiben, Eigenschaften des Objektsystems aber automatisch und effizient überprüft werden können.

Zahlreiche strukturelle und dynamische Einschränkungen werden eingeführt und untersucht, wobei im Fokus der Betrachtung stets die Komplexität des Erreichbarkeitsproblems liegt, eines der wichtigsten Verifikationsprobleme. Es wird gezeigt, dass strukturelle Einschränkungen alleine nicht genügen, dass es aber für die in dieser Arbeit eingeführten sogenannten sicheren elementaren Objektnetzsysteme und stark sicheren Objektnetzsysteme, die einen zwar sehr großen aber endlichen Zustandsraum besitzen, möglich ist, jede Eigenschaft, die in LTL oder CTL ausgedrückt werden kann, in polynomialen Platz zu entscheiden.

Mit diesen Formalismen ist es somit möglich, Mobilität und Interaktionen zu modellieren und gleichzeitig wichtige Eigenschaften automatisch und mit einem vertretbaren Aufwand zu überprüfen.

Kontakt:

Prof. Dr. Christopher Habel
Vorsitzender des Fach-Promotionssausschusses Informatik