Automatentheorie und ihre Anwendungen
-
Vortragender
-
Dr. Thomas Schneider
-
Art der Veranstaltung
-
K4, Master-Ergänzung, Wahlbereich: Spezielle Themen der Logik
-
Zeit und Ort
-
Mo. 12:30–14:00, MZH 1470
Mi. 8:30–10:00, SFG 2020
siehe auch Eintrag im
Vorlesungsverzeichnis Informatik fürs Sommersemester 2014
-
Zusätzliche Termine
-
Do., 17. 7., 8:30–10:00, MZH 1110
Do., 17. 7., 12:30–14:00, Cartesium 2.43 (Besprechungsraum 2. Etage)
dafür Ausfall am 21. 7. und 23. 7.
Kurzbeschreibung
Automatentheoretische Techniken haben nützliche Anwendungen in der Informatik:
mit ihnen kann man beispielsweise sicherheitsrelevante Eigenschaften eines Systems überprüfen (Verifikation),
robuste XML-Sprachen definieren oder Anfragen auf XML-Bäumen auswerten.
Dazu muss man den Standard-Begriff von endlichen Automaten auf Wörtern verallgemeinern,
indem man von endlichen Wörtern zu unendlichen Wörtern oder Bäumen übergeht.
Diese Erweiterung des Automatenbegriffs sowie die damit verbundenen theoretischen Resultate und praktischen Anwendungen
sind Gegenstand dieses Kurses.
Kurzübersicht der Themen:
-
Wiederholung von endlichen Automaten und formalen Sprachen
Anwendungen: Textsuche, Patternsuche, Textersetzung
-
Automaten auf endlichen Bäumen
Anwendung: Einschließung bei Termersetzungssystemen
Anwendung: XML-Schemasprachen
-
Automaten auf unendlichen Wörtern
Anwendung: Verifikation und Temporallogik (LTL)
-
Automaten auf unendlichen Bäumen
Anwendung: Verifikation und Temporallogik (CTL)
Wissen aus der Veranstaltung "Theoretische Informatik 1" ist hilfreich,
wird aber nicht vorausgesetzt – wir werden die wichtigsten Aspekte am Anfang kurz wiederholen.
Material
Folien
Einführung
4 pro Seite
Teil 1
4 pro Seite (Version vom 20. 5., 10:30 Uhr, kleine Korrekturen F. 51–53)
Teil 2
4 pro Seite (Version vom 27. 5., 12:30 Uhr)
Teil 3
4 pro Seite (Version vom 16. 7., 12:05 Uhr)
Teil 4
4 pro Seite (Version vom 16. 7., 16:00 Uhr)
Übungsblätter
Übungsblatt 1 (Abgabe am 30. 4. 5. 5.)
Übungsblatt 2 (Abgabe am 19. 5.)
Übungsblatt 3 (Abgabe am 2. 6.)
Übungsblatt 4 (Abgabe am 23. 6.)
Übungsblatt 5 (Abgabe am 9. 7.)
Übungsblatt 6 (Besprechung am 17. 7.)
Weiteres Material
XML, DTDs und Validierung
conference.xml mit unzulässiger DTD —
Validierungsergebnis
conference2.xml mit zulässiger DTD und gültigem XML-Dokument —
Validierungsergebnis
conference3.xml mit zulässiger DTD, aber ungültigem XML-Dokument —
Validierungsergebnis
Externer Link zum W3C-Validierer
Minimierung von Büchi-Automaten
Literaturangaben zum Nachlesen (PDFs sind auch in StudIP):
-
Sudeep Juvekar, Nir Piterman:
Minimizing Generalized Büchi Automata.
Proc. of CAV-06, vol 4144 of LNCS, pp. 45–58, Springer-Verlag, 2006.
SpringerLink
-
Christof Löding:
Efficient minimization of deterministic weak ω-automata.
Information Processing Letters, 79 (2001) 105–109.
ScienceDirect
AG Theorie der künstlichen Intelligenz
16. 7. 2014
Thomas Schneider
