Kompositionalität in der koalgebraischen Prozesstheorie

Prozesstheorie beschäftigt sich mit formalen Methoden zur Modellierung und Analyse von nebenläufigen Prozessen. Im Mittelpunkt steht dabei die präzise Semantik der Modelle. Weitverbreitete Prozessmodelle sind Transitionssysteme (und Varianten von solchen). Spezifischere Prozessmodelle wurden in verschiedenen Richtungen entwickelt, zum Beispiel probabilistische oder zeitabhängige Modelle, oder Modelle die zusätzliche Daten beinhalten. Oft werden komplexe Modelle aus einfacheren Bausteinen zusammengesetzt. Da zusammengesetzte Modelle oft durch Analyse ihrer Bausteine verifiziert werden können, ist es von großem Interesse Operationen zur Komposition von Modellen zu untersuchen. Das Ziel der Untersuchungen ist es dann zu zeigen, dass solche Kompositionsoperatoren mit diversen Eigenschaften verträglich sind. Die Theorie der Koalgebren ist auf einem höheren Abstraktionsniveau angesiedelt. Koalgebren sind ein kategorielles Konzept, welches konkrete Prozessmodelle verallgemeinert. Verschiedene Aspekte wie zum Beispiel Determinismus, Nichtdeterminismus, Wahrscheinlichkeit, Zeit, oder auch Daten im Standardmodell können lediglich durch die richtige Wahl eines Parameters der betrachteten Koalgebren ausgedrückt werden. Der Erfolg des Einsatzes dieses abstrakten Konzepts beruht zu einem wesentlichen Teil auf der Existenz eines natürlichen Begriffes von "behaviour" Semantik in Koalgebren (koalgebraische Bisimulation). Diese induziert in vielen konkreten Fällen bekannte Semantiken auf elegante Weise. Die Theorie der koalgebraischen Modallogiken umfasst ausserdem viele bekannte und zum Teil sehr unterschiedliche Modallogiken. Kompositionalität ist ein wesentlicher Bestandteil der Theorie der Koalgebren. Er kann in zweifacher Weise verstanden werden: Kompositionalität in der koalgebraischen Prozesstheorie, oder, auf einem Meta-Niveau, als Modularität der Typen welche die Koalgebren definieren. Vom mehr praxisorientierten Standpunkt aus sind kompositionelle Algorithmen wesentlicher Bestandteil der Untersuchung von Echtzeitsystemen und solchen Anwendungen wo Vorhersagbarkeit und beschränkte Reaktionszeiten von Bedeutung sind. Kompositionelle Algorithmen zu entwerfen ist oft eine grosse Herausforderung, da die Lösungen vieler algorithmischer Probleme für Echtzeitsysteme, zum Beispiel die Planbarkeitsanalyse, im allgemeinen Fall nicht kompositionell sind. Ziel dieses Projektes ist es die verschiedenen Aspekte der Kompositionalität in Koalgebren zu untersuchen, und die erhaltenen Erkenntnisse auf konkrete Modelle anzuwenden. Besonderes Augenmerk soll dabei auf die Behandlung probabilistischer Systeme gelegt werden. Weiters sollen Konzepte herausgearbeitet werden, welche kompositionellen Algorithmen in Echtzeitsystemen zugrundeliegen, und die abstrakten, theoretischen Untersuchungen mit der Praxis solcher Algorithmen zusammengeführt werden.