Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-64099
URL: http://www.freidok.uni-freiburg.de/volltexte/6409/


Eisinger, Jochen

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

Automata-based decision procedures for first-order logical theories with addition

Dokument1.pdf (800 KB) (md5sum: d5ea42f985fdf89c346b9d8ad5c42911)

Kurzfassung in Deutsch

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(N,+) bzw. FO(Z,+,<). Büchi-Automaten
ermöglichen einen ähnlichen Ansatz für die gemischte lineare Arithmetik, d.h.
FO(R,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(R,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.


Kurzfassung in Englisch

Büchi observed, in the 1960s, that automata over finite words can not only be
used to decide various sequential and modal logics. Automata-based methods can
also be used to analyze arithmetical theories. For example, automata over
finite words can represent addition of natural numbers. Since automata are
closed under boolean operations and projection, one immediately obtains a
decision procedure for Presburger arithmetic, i.e., the first-order logical
theory over the natural numbers with addition FO(N,+) or FO(Z,+,<). A similar
approach works for mixed linear arithmetic, i.e., FO(R,Z,+,<) using Büchi
automata. Boigelot et. al. have shown that even weak deterministic Büchi
automata suffice to decide this logical theory.

Although there exist efficient implementations of these automata-based
decision procedures for FO(R,Z,+,<), many research questions are still only
partially answered, and it turns out that a limiting factor in the
automata-based representation is the size of the automata.

This thesis aims at both, increasing the applicability of automata-based
decision procedures and improving the theoretical understanding of such
decision procedures.


SWD-Schlagwörter: Büchi-Automat , Automatentheorie , Entscheidungsverfahren , Beschränkte Arithmetik
Freie Schlagwörter (englisch): Büchi automata , automata theorie , decision procedures , bounded arithmetic
CCS Klassifikation F.4.3 , F.4.1 , F.1.1
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Becker, Bernd (Prof. Dr.)
Sprache: Deutsch
Tag der mündlichen Prüfung: 13.03.2009
Erstellungsjahr: 2009
Publikationsdatum: 24.03.2009
Indexliste