Universität Leipzig    Institut für Informatik    Automaten und Sprachen    Karin Quaas
Wintersemester 2012/13 Vorlesung Echtzeitautomaten
	Echtzeitautomaten sind eine Erweiterung endlicher Automaten um eine endliche Menge reellwertiger Uhrenvariablen. Eine Uhrenvariable misst die Zeit, die in einem Zustand des Automaten verbracht wird. Die Transitionen eines Uhrenautomaten können mit Uhrenbedingungen z.B. der Form x>2, versehen werden: die Transition darf nur ausgeführt werden, wenn der aktuelle Wert der Uhr x größer 2 ist. Echtzeitautomaten eignen sich zur Modellierung von Echtzeitsystemen, d.h. Systemen deren korrekte Funktionsweise von zeitlichen Bedingungen abhängen. Die formale Verifikation solcher Echtzeitsysteme stellt eine wesentliche Motivation für die Beschäftigung mit Echtzeitautomaten dar.
	In dieser Vorlesung lernen Sie zunächst das Modell der Echtzeitautomaten kennen. Wir untersuchen Eigenschaften und Entscheidungsprobleme, die Sie bereits aus der Theorie der Automaten und Sprachen kennen: Abschlusseigenschaften unter Operationen wie Schnitt und Komplement, das Erreichbarkeitsproblem oder das Sprachinklusionsproblem. Da der Zustandsraum eines Echtzeitautomaten im Gegensatz zu dem von endlichen Automaten unendlich ist, stellt die Bewältigung dieser Probleme eine ganz neue Herausforderung dar! Wir werden uns mit temporalen Logiken wie CTL und LTL, bzw. deren zeitlichen Erweiterungen, und dem Model Checking von Echtzeitautomaten beschäftigen. Weiterhin ist eine kleine Einführung mit weiterführenden praktischen Arbeiten in das Verifikationswerkzeug UPPAAL geplant.
	Voraussetzungen: Kenntnisse in Diskrete Strukturen, Automaten und Sprachen sowie Berechenbarkeit sind hilfreich.
Termine
	Vorlesung montags 13.15-14.45, SG 1-10.
	Übungen montags 15:15-16:45, SG 3-10 (aller 2 Wochen)
Übungen
	Serie 1 (Besprechung am 18.10.2012)
	Serie 2 (Besprechung am 05.11.2012)
	Serie 3 (Besprechung am 26.11.2012)
	Serie 4 (Besprechung am 17.12.2012)
	Serie 5 (Besprechung am 14.01.2013)
	Serie 6 (Besprechung am 28.01.2013)
Neuigkeiten
	Reading Group im Rahmen des Graduiertenkollegs zum Thema temporale Echtzeitlogiken
Literatur
	Rajeev Alur, David Dill: Automata for Modeling Real-Time Systems. In Automata, Languages and Programming, 17th International Colloquium (ICALP 1990), 322-335, Springer LNCS, Volume 443.
	Rajeev Alur, David Dill: A Theory of Timed Automata. In Theoretical Computer Sciences, 183-235, Volume 126, 1994.
	Costas Courcoubetis, Mihalis Yannakakis: Minimum and Maximum Delay Problems in Real-Time Systems. In Formal Methods in System Design, 385-415, Volume 1, 1992.
	Olivier Finkel: Undecidable Problems About Timed Automata. In CoRR, Volume abs/0712.1363, 2007.
	Joel Ouaknine, James Worrell: On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. In LICS Proceedings, 54-63, IEEE Computer Society, 2004.
	Rajeev Alur, Costas Courcoubetis, David Dill: Model-Checking in Dense Real-time. In Inf. Comput., 2-34, Volume 104, 1993.
	Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. In ACM Trans. Program. Lang. Syst., 244-263, Volume 8, 1986.