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. |