Verbotsmuster für Logik mit zwei Variablen über endlichen und unendlichen Wörtern

Abstract

Die Varietät DA, die mit der Logik erster Stufe über zwei Variablen übereinstimmt, bildet das höchste Level der Trotter-Weil-Hierarchie. Varietäten in dieser Hierachie können algebraisch über l-Gleichungen charakterisiert werden und haben teilweise äquivalente Klassen in der Quanto- renalternierungshierarchie innerhalb FO2. Um Sprachen mit diesen Klassen in Verbindung zu bringen, ist es möglich, das syntaktische Monoid auszurechnen und für alle möglichen Belegungen die l-Gleichung zu überprüfen. Aus komplexitätstheoretischer Sicht ist dieser Ansatz aufwändig und diese Arbeit befasst sich mit Kriterien, mit denen man die gesuchte Verbindung direkt auf den Automaten der Sprachen prüfen kann. Das zentrale Konzept stellen dabei Verbotsmuster dar. In dieser Arbeit wird eine Definition für Verbotsmuster bei nicht notwendigerweise minimalen DEAs und CMAs gegeben. Damit werden explizite Verbotsmuster für Sprachen über endlichen Wörtern für die Varietäten an den Enden der Hierarchie konstruiert und ein allgemeines Schema für die inneren Level angepasst. Aus diesen Mustern werden Verbotsmuster für fin-syntaktische Monoide von Sprachen über unendlichen Wörtern abgeleitet. Zusammen mit einem Verbotsmus- ter, das die Zugehörigkeit zu DA für inf-syntaktische Monoide entscheidet, lässt sich damit die Trotter-Weil-Hierarchie vollständig für DEAs und CMAs charakterisieren. Für alle konstruierten Verbotsmuster werden NL- und P-Algorithmen erstellt, die Automaten auf das Enthalten dieser Verbotsmuster prüfen. Dies beinhaltet sowohl Algorithmen, bei denen ein festes Verbotsmuster gegeben ist, als auch Algorithmen, bei denen es Teil der Eingabe ist. Für die Varietäten der Trotter-Weil-Hierarchie existieren auch Verbotsmuster mit Teilwortbeziehungen, die von Henriksson und Kufleitner definiert wurden. Die beiden Verbotsmusterarten werden in dieser Arbeit verglichen. Dabei werden insbesondere die Größen der Muster, die Komplexitätsschranken der Algorithmen und die gefundenen Zeugen berechnet. Es ergibt sich ein Größenvorteil der Teilwortmuster gegenüber den Faktormustern bei vergleichbaren Komplexitäten der Algorithmen.