ISBN 9783843934442

978-3-8439-3444-2, Reihe Informatik

Sebastian Küpper
Behavioural Analysis of Systems with Weights and Conditions

327 Seiten, Dissertation Universität Duisburg-Essen (2017), Softcover, A5

Zusammenfassung / Abstract

Zustandsbasierte Systeme sind bereits seit langer Zeit ein mächtiges Werkzeug um Computersysteme zu analysieren und zu modellieren. Neben vielen anderen Anwendungen sind zustandsbasierte Systeme einer der Formalismen, die in UML enthalten sind, sie werden in der Verarbeitung natürlicher Sprache verwendet und spielen eine wichtige Rolle beim Design von Compilern. Allerdings sind viele zustandsbasierte Systemmodelle, die bislang ausführlich untersucht wurden, nur auf das Verhalten einzelner Systeme, statt auf eine einheitliche Beschreibung von Klassen von Systemen ausgerichtet. Weiterhin werden oft nur Systemmodelle betrachtet, die erfassen, welche Aktionen durchgeführt werden, ohne die benötigten Ressourcen oder die Wahrscheinlichkeit einer Transition zu beachten. Daher wurden zuletzt auch zustandsbasierte Systeme mit einem Gewicht, das über den Ablauf des Systems akkumuliert wird, oder Bedingungen, die es erlauben, Klassen von Systemen zu spezifizieren, ausgiebig untersucht.

Das Ziel dieser Arbeit ist es, die Gemeinsamkeiten zwischen der klassischen Verhaltensanalyse für nichtdeterministische Automaten und Transitionssystemen auf der einen Seite und gewichteten Automaten sowie bedingten Transitionssystemen auf der anderen Seite, in einem koalgebraischen Kontext zu identifizieren. Koalgebra bietet eine einheitliche Theorie, die es erlaubt, Prototyp-Algorithmen zu entwerfen und verschiedene zustandsbasierte Systeme zu modellieren, um diese auf einheitliche Art mit Instanzen des gleichen grundlegenden Algorithmus zu analysieren.

In dieser Arbeit wird ein koalgebraischer Algorithmus, der auf der bekannten Final Chain beruht, vorgestellt. Dieser Algorithmus kann für eine große Zahl von Automatenmodellen instanziiert werden. Zudem wird gezeigt, wie man Automaten mit Gewichten und Bedingungen koalgebraisch so modellieren kann, dass dieser Algorithmus die gewünschte Art der Verhaltensäquivalenz ermittelt.

Aus einer konkreteren Perspektive werden Wege diskutiert, um das Laufzeitverhalten von Prozeduren zur Überprüfung der Verhaltensäquivalenz von gewichteten Automaten und bedingten Transitionssystemen, zu optimieren. Diese Techniken werden nicht im Kontext koalgebraischer Modellierung angegeben, sind aber von der grundlegenden Arbeit inspiriert. Insbesondere werden Up-to-Techniken für gewichtete Automaten entworfen und Algorithmen auf Basis von Matrixmultiplikation, sowie optional mit der Unterstützung von BDDs, für bedingte Transitionssysteme erläutert.