Seminar Automaten über unendlichen Wörtern (SoSe 2024)
| Dozent | Lutz Schröder |
| Daten | Do, 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) |
Es gibt einen Studon-Kurs.
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
- Paritätsspiele
- 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