Universität Leipzig    Institut für Informatik    Automaten und Sprachen    Karin Quaas
Summer 2014 Course Real-timed automata
	Real-timed automata extend finite automata with a finite set of real-valued clock variables. A clock can be used to measure the time that the automaton spends in a state. The transitions of a real-timed automaton may be labelled with clock constraints. For instance, the clock constraint x>2 means that the transition may only be executed if the current value of the clock variable x is greater than 2. Real-timed automata are useful for modelling real-timed systems, i.e., systems whose behaviour depend upon timing constraints. Studying real-timed automata is mainly motivated by formal verification of such real-timed systems.
	In this course, you learn how to model real-timed systems by timed automata. We investigate fundamental properties and decision problems that you already know from the theory of finite automata: closure under intersection, union, complement, as well as the reachability problem, or the language inclusion problem. The state-transition system induced by a timed automaton is infinite (in contrast to finite automata), and hence the management of these problems is a real challenge! Further, we will concern ourselves with real-timed extensions of temporal logics like LTL and CTL.
Requirements
	The course is part of the Kernmodul (10-202-2107), Angewandte Automatentheorie. Basic knowledge in discrete structures, automata and formal languages, as well as complexity theory is very useful. The course will be given in English.
When and Where
	Lecture: Mondays 13.15-14.45, SG 3-14.
	Exercises: Mondays 15:15-16:45, SG 3-14 (every second week, A-Woche)
	Consultation: If you have any questions or problems, you can email me or come to my office on Wednesdays, from 10:45 to 11:10.
	Schedule
	7.7.2014 The lecture must be cancelled. Please put the exercises under my door or give them our secretary.
Overview
	Lecture 1: Formal Verification, EEL Protocol, Timed Languages and Timed Automata (Alur and Dill, 1990)
	Lecture 2: The reachability problem, history, clock region equivalence relation
	Lecture 3: Representation of clock regions, time successors of clock regions
	Lecture 4: Region graph construction, Bisimulation Lemma, Untime operator, Script
	Lecture 5: PSPACE-hardness of the reachability problem for timed automata with two clocks, part 1
	Lecture 6: PSPACE-hardness of the reachability problem for timed automata with two clocks, part 2
	Lecture 7: Closure properties of recognizable timed languages: Union, Intersection, Complement; Further decision problems: The universality problem, part 1.
	Lecture 8: Universality problem, part 2, complementability problem.
	Lecture 9: The language inclusion problem for single-clock timed automata
	Lecture 10: Well-structured transition systems, part 1.
Exercise Sheets
	Exercises 1, submit by 5.5.2014
	Exercises 2, submit by 19.5.2014
	Exercises 3, submit by 2.6.2014
	Exercises 4, submit by 23.6.2014
	Exercises 5, submit by 7.7.2014
Literature
	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.
	John Fearnley, Marcin Jurdzinski: Reachability in Two-Clock Timed Automata is PSPACE-complete. In ICALP 2012, 212-223, 2012.
	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.