Coinduction Meets Algebra For the Axiomatization of System Equivalence (COAX)

Ein wichtiges Problem im Bereich der Spezifikation und Verifikation sowohl sequentieller als auch paralleler Programme ist die Prüfung von Programmäquivalenz. Während Programmäquivalenz im Allgemeinen unentscheidbar ist (z.B. für Turing-vollständige Sprachen), lässt sich Entscheidbarkeit für geeignet abstrahierte Ausdruckssprachen, die nur Teilaspekte des Programmverhaltens beschreiben, wieder herstellen. Ein klassisches Beispiel hierfür sind reguläre Ausdrücke, die lediglich den Kontrollfluss eines sequentiellen Programms beschreiben und deren äquivalenz PSPACE-vollständig ist. Für Systeme mit endlichem Zustandsraum gibt es neuerdings generische Verfahren, die ein Ausdruckskalkül mit entscheidbarer äquivalenz aus dem Systemtyp ableiten; diese liefern z.B. das o.g. Ergebnis für reguläre Sprachen als Spezialfall. Das Ziel von COAX ist die Entwicklung von Ausdruckssprachen, Beweiskalkülen und Algorithmen für die äquivalenz von Systemen, deren Zustandsraum zwar unendlich, aber finitär ist, d.h. eine endliche algebraische Präsentation hat. Zum Beispiel ist der Zustandsraum eines gewichteten Automaten ein endlich dimensionaler Vektorraum über einem Körper; er ist somit im Allgemeinen unendlich, hat aber eine endliche Präsentation durch seine Basis. Wie schon o.g. Resultate über endliche Systeme werden unsere Arbeiten auf dem Prinzip der universellen Koalgebra basieren, die große Klassen zustandsbasierter Systeme, neben klassischen (nicht)deterministischen Automaten z.B. auch gewichtete, probabilistische und spieltheoretische Systeme, in einer vereinheitlichten Sicht behandelt. Die geplante Entwicklung kombiniert und erweitert verschiedene aktuelle Forschungsrichtungen: Turi und Plotkins mathematische operationelle Semantik; die von Rutten et al. initiierte koalgebraische Vereinheitlichung automatentheoretischer Konstruktionen; die von Pattinson und einem der Antragsteller (Schröder) entwickelte koalgebraische Logik der Prädikatenliftings; Silvas koalgebraische Ausdruckskalküle für Mengenfunktoren; und die von einem der Antragsstellers (Milius) und Koautoren eingeführte generische Semantik finitärer Systeme. Wir werden hierbei über allgemeinen algebraischen Kategorien arbeiten und somit über den bisher üblichen rein mengentheoretischen Ansatz hinausgehen. Damit erhalten wir generische Sprachen und koinduktive Methoden für automatische äquivalenzbeweise über finitären Systemen mit entsprechend strukturierten Zustandsräumen. Diese generischen Resultate werden für wichtige konkrete Systemtypen instanziiert: arbeitet man z.B. über Halbverbänden, Moduln über Semiringen oder positiv konvexen Algebren, erhält man Verifikationsmethoden für verschiedene Typen nichtdeterministischer, gewichteter bzw. probabilistischer Systeme; über Prägarben oder nominalen Mengen erhält man Sprachen mit Bindungs- und Kommunikationsoperationen für Variablen bzw. Namen, bis hin zum pi-Kalkül.