Seminar Automaten über unendlichen Wörtern (WiSe 2017/18)

Dozent Lutz Schröder
Daten Di, 12:30 – 14:00, 01.151-128
Zielgruppe WPF INF-MA (ECTS-Credits: 5)
WPF INF-BA-V-THI (ECTS-Credits: 5)
WF M-BA (ECTS-Credits: 5)
WF M-MA (ECTS-Credits: 5)

Das temporale Verhalten nebenläufiger Systeme wird in der linearisierten Sicht auf die Zeit mittels unendlicher Wörter modelliert. Dementsprechend gibt es zahlreiche sowohl logische als auch automatentheoretische Formalismen zur Spezifikation unendlicher Wörter, zwischen denen zum Teil überraschende Querverbindungen bestehen. Gegenstand des Seminars sind die Semantik, Axiomatik und inbesondere Algorithmik solcher Systeme.

Termine

(Vorläufig!)

Miriam Polzer: Automatenbegriffe und Übersetzungen, 7.11., 14.11., 21.11.

Johannes Kern: Determinisierung von Büchi-Automaten, 5.12., 12.12. und 19.12.

Philipp Reger: Unendliche Spiele und Determiniertheit, 19.12., 9.1. und 16.1.

Helene Gsänger: Algorithmen für Paritätsspiele, 23.1., 30.1. und 6.2.

Themen

Die folgende Themenliste ist weder notwendigerweise erschöpfend noch wird sie zwingend vollständig abgearbeitet:

  • Büchi-Automaten
  • Müller-, Rabin-, Streett-Automaten
  • Paritätsautomaten
  • Determinisierung
  • Leerheitsprüfung
  • Lineare Temporallogik
  • Modellprüfung
  • Modaler mu-Kalkül
  • Monadische Logik zweiter Stufe

Literatur

  • E. Grädel, W. Thomas, T. Wilke (eds.): Automata, Logics, and Infinite Games. Vol. 2500 of LNCS, Springer, 2002.
  • Nir Piterman: From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. Logical Methods in Computer Science 3, 2007
  • S. Miyano and T. Hayashi. Alternating finite automata on omega-words. Theoret. Comput. Sci., 32:321–330, 1984
  • J. Esparza, J. Kretínský, J.-F. Raskin, S. Sickert: From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, vol 10205 of LNCS, Springer 2017; full version available as CoRR abs/1701.06103, 2017