Automatic Structures
Final Report Abstract
Automatische Strukturen sind unendliche Strukturen, welche aber endliche Präsentationen durch Automaten erlauben. Eine Struktur ist dann automatisch, wenn man ihre Elemente so durch Wörter einer regulären Sprache repräsentieren kann, dass alle Funktionen und Relationen der Struktur (inklusive die Gleichheit) durch endliche Automaten erkennbar sind. Wichtige Gründe fär das Interesse an automatischen Strukturen sind in ihren guten algorithmischen Eigenschaften begründet. Insbesondere hat jede automatische Struktur eine entscheidbare Theorie. Die automatische Präsentation der atomaren Relationen und die Abschlusseigenschaften endlicher Automaten liefern effektive Auswertungsalgorithmen für beliebige Formeln der Prädikatenlogik und gewisser Erweiterungen davon. Die wichtigsten Ergebnisse dieses Vorhabens betreffen Erweiterungen des Begriffs automatischer Strukturen in drei verschiedene Richtungen: w-automatische Strukturen, ressourcen-beschränkte automatische Strukturen, und parameter-automatische Strukturen. Wir haben die Tragweite dieser Erweiterungen (also die Frage, welche Strukturen in diesem Sinn automatisch sind), und ihre modelltheoretischen und algorithmischen Eigenschaften untersucht. Die günstigen algorithmischen und modelltheoretischen Eigenschaften automatischer Strukturen übertragen sich auf parameter-automatische Strukturen dann, wenn der Parameter als unendliches Wort selbst eine entscheidbare monadische Theorie hat. Insbesondere ist dann sogar für Logiken, welche die Prädikatenlogik um Zählkonstrukte und Ramseyquantoren erweitern, die Theorie der Struktur entscheidbar. Der Begriff der parameter-automatischen Strukturen führt ausserdem auf den neuen, vorher nicht zur Verfügung stehenden Begriff einer uniform automatischen Klasse von Strukturen, und hebt damit den Begriff der Automatizität auf eine höhere Stufe: von einzelnen Strukturen auf ganze Strukturklassen. Dies führt zu neuen Fragestellungen und Anwendungen, insbesondere auch im Bereich endlicher Strukturen. Die algebraischen und kombinatorische Methoden zur Untersuchung von w-automatischen Strukturen, ressourcen-beschränkten automatischen Strukturen und parameter-automatischen Strukturen, die wir in diesem Vorhaben entwickelt haben, liefern Einsichten in die Eigenschaften der in solchen Strukturen definierbaren Funktionen und Relationen. Damit können auch Grenzen der Theorie automatischer Strukturen aufgezeigt werden. Eine fundamentale Einsicht, die sich aus diesem Vorhaben ergibt ist, dass eine der wichtigsten mathematischen Strukturen mit entscheidbarer Theorie, der Körper der reellen Zahlen, in keiner der bisher untersuchten Varianten dieses Begriffs automatisch ist.
Publications
- Model-Theoretic Properties of ω-Automatic Structures, Theory of Computing Systems 55(4): 856-880 (2014)
F. Abu Zaid, E. Grädel, L. Kaiser, and W.Pakusa
(See online at https://doi.org/10.1007/s00224-013-9508-6) - A Unified Approach to Boundedness Properties in MSO, Computer Science Logic (CSL 2015), 441–456, 2015
L. Kaiser, M. Lang, S. Lessenich, and C. Löding
(See online at https://doi.org/10.4230/LIPIcs.CSL.2015.441) - Counting Logics and Games with Counters, Doctoral Dissertation, RWTH Aachen University, 2015
S. Lessenich
- Algorithmic Solutions via Model Theoretic Interpretations, Doctoral Dissertation, RWTH Aachen University, 2016
F. Abu Zaid
(See online at https://doi.org/10.18154/RWTH-2017-07663) - Advice Automatic Structures and Uniformly Automatic Classes, Computer Science Logic (CSL), 2017
F. Abu Zaid, E. Grädel, and F. Reinhardt
(See online at https://doi.org/10.4230/LIPIcs.CSL.2017.35)
