Unambiguous Automata on Infinite Words

• Applicant: Professor Dr. Thomas Wilke
• Subject Area: Theoretical Computer Science
• Term: from 2013 to 2017
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 233172410

• Final Report Year: 2017

Final Report Abstract

Das Ziel des Vorhabens war die Weiterentwicklung der Theorie der eindeutigen endlichen Automaten auf unendlichen Wörtern, insbesondere der rückwärts deterministischen, auch bekannt als prophetic automata. Insbesondere sollten neue automatentheoretische Konstruktionen gefunden werden und der Zusammenhang zu Logiken (temporalen und Fixpunktlogiken) sowie zur Algebra studiert werden. – Den beschriebenen Automaten kommt eine besondere Bedeutung zu, weil es sich um einfache deterministische Automaten handelt, die alle regulären ω-Sprachen abdecken. Das Vorhaben hat Ergebnisse in drei unterschiedlichen Bereichen hervorgebracht: Temporale Logik. Der enge Zusammenhang zwischen Fragmenten vorwärts gerichteter temporaler Logik und rückwärts deterministischen ω-Automaten war schon in den Vorarbeiten zu dem Vorhaben aufgedeckt worden. Unklar gelieben war, ob diese Automaten auch genutzt werden können, um tiefere Einsichten über den gesamten Sprachumfang der temporalen Logik zu gewinnen. In diesem Zusammenhang wurde eine strukturell einfache Übersetzung von zählerfreien rückwärts deterministischen Automaten in vorwärts gerichtete temporale Logik sowie eine Übertragung von vorwärts und rückwärts gerichteten temporalen Formeln in so genannte aperiodische Bimaschinen entwickelt. Alternierende Automaten und Fixpunktlogiken. Die spezielle Laufrichtung der betrachteten Automaten – von der Zukunft in die Gegenwart – legt es nahe, dass diese Automaten eng mit alternierenden Automaten und modaler Fixpunktlogik verknüpft sind. Das wurde im Rahmen des Vorhabens durch Angabe entsprechender Übersetzungen der Automaten gezeigt und mehrfach genutzt. Neue Automatenkonvertierungen. Zentrale Konstruktionen für ω-Automaten sind durchaus kompliziert, denkt man zum Beispiel an die Determinisierung von Büchi-Automaten oder die Übersetzung von Büchi-Automaten in rückwärts gerichtete deterministische Automaten. Im Vorhaben wurde deshalb die letztgenannte Übersetzung modularisiert und eine neuartie Übersetzung von deterministischen Muller- und Paritätsautomaten in rückwärts deterministische Automaten entwickelt.

Publications

• Effective Characterizations of Simple Fragments of Temporal Logic Using Carton–Michel Automata. Logical Methods in Computer Science 9(2) 2013
  Sebastian Preugschat, Thomas Wilke
  
• Past, Present, and Infinite Future. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP) 2016, July 11-15, 2016, Rom, Italien. LIPIcs, vol. 55, Schloss Dagstuhl, Seiten 95:1-95:14, 2016
  Thomas Wilke
  
• ω-Automata, CoRR
  Thomas Wilke
  
• Backward deterministic and weak alternating ω-automata, CoRR
  Thomas Wilke