Koinduktion und Algebra in der Axiomatisierung und Algorithmik von Systemäquivalenzen

• Antragsteller: Professor Dr. Stefan Milius; Professor Dr. Lutz Schröder
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 259234802

Ein wichtiges Problem bei der Spezifikation und Verifikation sowohl sequentieller als auch paralleler zustandsbasierter Systeme ist die Prüfung auf Systemäquivalenz. Während dies im Allgemeinen unentscheidbar ist (insbesondere für ausdrucksstarke, z.B. Turing-vollständige Modelle), kann die Entscheidbarkeit bei einfachen Automatenmodellen durchaus erhalten bleiben. Für solche Systeme existieren häufig syntaktische Ausdrückskalküle, die die Systemäquivalenz axiomatisieren, z.B. reguläre Ausdrücke und Kleene-Algebren für klassische endliche Automaten. Für Systeme mit endlichem Zustandsraum gibt es neuerdings generische Verfahren, die einen Ausdruckskalkül samt Axiomatisierung sowie Entscheidbarkeitsresultate aus dem Systemtyp ableiten; konkret implementierbare Algorithmen werden aber nach wie vor für jeden Systemtyp neu entworfen.Ziel von COAX ist die Entwicklung von generischen, d.h. über den Transitionstyp parametrisierten Algorithmen für die Äquivalenzprüfung und Minimierung zustandsbasierter Systeme. Die zweite Projektphase konzentriert sich insbesondere auf nominale Systeme und Automaten für Datensprachen. Ferner entwickeln wir generische Sprachen, Beweissysteme und Algorithmen für die Spezifikation und Äquivalenzprüfung nominaler Systeme mit orbit-endlichem oder algebraisch orbit-endlich erzeugtem Zustandsraum.Wie schon in der ersten Projektphase werden unsere Arbeiten auf Prinzipien 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: die koalgebraischen Grundlagen der Trace-Semantik; die von Rutten et al. initiierte und von den Antragstellern in der ersten Phase erweiterte koalgebraische Vereinheitlichung automatentheoretischer Konstruktionen; generische Algorithmen für die Minimierung von Systemen unter Bisimilarität aus der ersten Projektphase von COAX; Bisimulation bis auf Kongruenz; koalgebraische Ausdruckskalküle für Mengenfunktoren; und die von einem der Antragssteller (Milius) und Koautoren eingeführte generische Semantik finitärer Systeme.Wir werden hierbei jenseits des bisher üblichen rein mengentheoretischen Ansatzes über allgemeineren Kategorien arbeiten, insbesondere über nominalen Mengen und nominalen algebraischen Strukturen; wir erhalten damit eine allgemeinere Anwendbarkeit unserer generischen semantische Theorie und der darauf aufbauenden generischen Algorithmik. Diese Resultate werden für wichtige konkrete, insbesondere nominale, Systemtypen instanziiert, inklusive Systemen und Automaten für unendliche Objekte. Insgesamt erhält man somit eine umfassende Sammlung von mathematischen Resultaten, Konstruktionen und Algorithmen für ein breites Spektrum von Systemtypen und -äquivalenzen.

• DFG-Verfahren: Sachbeihilfen