Seminar Automaten über unendlichen Wörtern (WiSe 2020/21)

Dozent Lutz Schröder
Daten Mo, 14:15 – 15:45, 00.131-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)

 

Achtung: Aufgrund der sich verschlechternden Pandemiesituation findet der Kurs zunächst online via Zoom statt; den Link finden Sie im Studon-Kurs, dem Sie idealerweise beitreten.

 

 

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

TBA

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