Koalgebren und verallgemeinerte reguläre Ausdrücke

In diesem Vortrag gebe ich einen Überblick über meine aktuellen Forschungsthemen. Der Schwerpunkt wird dabei auf der Theorie der zustandsbasierten Systeme liegen.

Zustandsbasierte Systeme verschiedenen Typs modellieren Phänomene in vielen verschiedenen Gebieten der Informatik, der Mathematik oder auch in der Biologie und Physik. Ein wichtiges Problem ist dabei, zu entscheiden, ob zwei vorgelegte Systeme semantisch äquivalent sind und ggf. einen formalen Beweis in einem geeigneten logischen Kalkül dafür zu konstruieren. Für endliche Automaten ist dies beispielsweise mit Hilfe von Kozen's Kleene Algebren, die die Äquivalenz regulärer Ausdrücke axiomatisieren, möglich.

In dem Vortrag wird erklärt, wie man Koalgebren benutzt, um für eine große Klasse von Systemen verschiedenen Typs jeweils den passenden korrekten, vollständigen und entscheidbaren "regulären" Ausdruckskalkül für Bisimilarität in generischer Art und Weise zu erhalten. Darüberhinaus zeige ich, wie man daraus durch Hinzufügen von Axiomen Kalküle für Sprachäquivalenz konstruiert. Letztere ist zwar gröber als Bisimilarität aber für viele Systemtypen die "gewünschte" Äquivalenz - z.B. für nichtdeterministische oder gewichtete Automaten.

Als konkrete Anwendung betrachte ich (1) Rabinovichs Erweiterung von Milners Kalkül für Prozesse mit endlichem Zustandsraum, (2) den ersten korrekten und vollständigen Kalkül für gewichtete Automaten und (3) einen Kalkül für die Äquivalenz von Stream-Schaltkreisen, einer grafischen Repräsentation linearer Systeme.