Deterministische endliche Automaten und Zwei-Variablen-Logik erster Stufe

Abstract

Therien und Wilke zeigten in einer Arbeit von 1998, dass 2-Variablen-Logik erster Stufe (FO^2) einer entscheidbaren Klasse endlicher Monoide entspricht. Damit läßt sich insbesondere für jede reguläre Sprache entscheiden, ob sie in FO^2 definierbar ist. Dieses Entscheidbarkeitsresultat konnte 2012 in einer Arbeit von Weil und Kufleitner auf die Alternierungshierarchie innerhalb von FO^2 ausgedehnt werden. Im Rahmen dieser Arbeit wird untersucht, wie effizient sich diese Entscheidbarkeitsresultate umsetzen lassen, wenn die reguläre Sprache durch deterministische endliche Automaten gegeben ist. Als Vorstufe hierzu werden geeignete algebraische Charakterisierungen der Alternierungshierarchie innerhalb von FO^2 recherchiert. Basierend darauf werden Entscheidungsverfahren auf Basis sogenannter Verbotsmuster entwickelt.