Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

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

Fachliche Zuordnung Theoretische Informatik
Förderung Förderung von 2014 bis 2023
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 259234802
 
Erstellungsjahr 2023

Zusammenfassung der Projektergebnisse

Zustandsminimierung ist eine wichtige Aufgabe bei der Verifikation von zustandsbasierten Systemen. Ferner hat man häufig syntaktische Ausdruckskalküle, die die Äquivalenz von zustandsbasierten Systemen axiomatisieren, z.B. reguläre Ausdrücke für endliche Automaten. Ziel von COAX war es, generische semantische Grundlagen für die Beschreibung von Systemen und Algorithmen zur Minimierung und Äquivalenzprüfung, die parametrisch im Transitionstyp sind, zu entwickeln. Diese Parametrisierung basiert auf Methoden der universellen Koalgebra, die eine einheitliche Sicht auf ein breites Spektrum zustandsbasierter Systeme ermöglicht. In der zweiten Projektphase COAX2 haben wir die Modularitätsmechanismen und die Komplexitätsanalyse eines in der ersten Projektphase entwickelten Partitionsverfeinerungsalgorithmus verallgemeinert. Zudem haben wir die Generizitätsmechanismen des Algorithmus erweitert, so dass auch gewichtete Systeme mit abdeckt werden. Auf Grundlage dieses Algorithmus haben wir ein generisches und modulares Werkzeug, den Coalgebraic Partition Refiner (CoPaR), implementiert und anschließend durch Vorschaltung einer generischen Erreichbarkeitsanalyse zu einem Minimierer erweitert. Als Erweiterung des generischen Partititionsverfeinerungsalgorithmus haben wir einen Algorithmus entwickelt, der unterscheidende Modalformeln für verhaltensinäquivalente Zustände berechnet. In konkreten Instanzen realisieren diese Algorithmen entweder die beste bekannte Komplexität oder verbessern diese sogar. In Arbeiten über generische Ausdruckskalküle zur Beschreibung von Systemverhalten haben wir gezeigt, dass Ausdruckskalküle für Branching-Time-Semantik als Fragmente des koalgebraischen µ-Kalküls verstanden werden können. Als Instanzen fallen hier sowohl ein bekanntes Resultat für den klassischen Fall markierter Transitionssysteme als auch neue Ergebnisse für gewichtete und probabilistische Systeme ab. In COAX haben wir weiterhin ein generisches Rahmenwerk entwickelt, in dem die Semantik nebenläufiger Systeme mittels einer Kombination von universeller Koalgebra und gradierten Monaden sowohl über den Verzweigungstyp der zugrundeliegenden Transitionssysteme als auch über die Granularität der Prozessäquivalenz parametrisiert werden kann. Wir erfassen somit Spektren von Verhaltensäquivalenzen, wie van Glabbeeks klassisches Linear-Time/Branching-Time-Spektrum auf markierten Transitionssystemen, in koalgebraischer Allgemeinheit. Darüber hinaus erlaubt unser Rahmenwerk eine systematische Extraktion von charakteristischen Modallogiken, für die man Expressivitätsresultate mittels eines generischen Hennessy-Milner-Satzes erhält. Des weiteren haben wir Ergebnisse über die Spezifikation von endlichen algebraischen Strukturen erzielt, für die der klassische Satz von Reiterman eine Charakterisierung durch profinite Gleichungen liefert. In COAX haben wir einen auf Monadenalgebren beruhenden generischen kategoriellen Rahmen für die Theorie profiniter Gleichungen und Sätze vom Reiterman-Typ entwickelt. Als Instanzen erhält man sowohl den klassischen Satz von Reiterman als auch eine Version für geordnete Algebren sowie ein Ergebnis von Pin und Weil über relationale Strukturen.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2025 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung