Masterarbeit MSTR-2023-45

Bibliograph.
Daten
Heindl, Amelie: Verbotsmuster für Logik mit zwei Variablen über endlichen und unendlichen Wörtern.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Masterarbeit Nr. 45 (2023).
67 Seiten, deutsch.
Kurzfassung

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 omega-Gleichungen charakterisiert werden und haben teilweise äquivalente Klassen in der Quantorenalternierungshierarchie 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 omega-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 Verbotsmuster, 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.

Volltext und
andere Links
Volltext
Abteilung(en)Universität Stuttgart, Institut für Formale Methoden der Informatik, Theoretische Informatik
BetreuerKufleitner, PD Dr. Manfred
Eingabedatum15. November 2023
   Publ. Informatik