Automatenbasierte Entscheidungsverfahren für Theorien der Logik erster Stufe mit Addition

Jochen Eisinger

Büchi erkannte bereits 1960, dass Automaten über endlichen Wörtern nicht nur verwendet werden können, um verschiedene sequentielle und modale Logiken zu entscheiden. Sie können auch für arithmetische Theorien eingesetzt werden. Zum Beispiel kann mit Automaten über endlichen Wörtern die Addition natürlicher Zahlen dargestellt werden. Da Automaten unter booleschen Operationen und Projektion abgeschlossen sind, erhält man so ein Entscheidungsverfahren für die Presburger Arithmetik, d.h. die Theorie der Logik erster Stufe über den natürlichen Zahlen mit Addition FO(ℕ,+) bzw. FO(ℤ,+,<). Büchi-Automaten ermöglichen einen ähnlichen Ansatz für die gemischte lineare Arithmetik, d.h. FO(ℝ,Z,+,<). Boigelot et. al. haben gezeigt, dass bereits eine Teilklasse der Büchi-Automaten ausreicht, so genannte schwache deterministische Büchi-Automaten, um diese Logik zu entscheiden.

Obwohl Implementierungen automatenbasierter Entscheidungsverfahren für FO(ℝ,Z,+,<) existieren, sind noch viele Forschungsfragen offen bzw. nicht vollständig beantwortet, und die praktische Anwendbarkeit scheitert häufig an der Größe der Automaten.

Ziel der vorliegenden Arbeit ist es, sowohl die praktische Anwendbarkeit automatenbasierter Entscheidungsverfahren zu erhöhen, als auch zu einem besseren theoretischen Verständnis solcher Entscheidungsverfahren beizutragen.

back