Automata for Real-time Systems

January - April 2014

Announcements


Course description

Timed automata are an extension of finite automata that recognize words with time-stamps. These automata are useful to model and verify a number of embedded systems that work under real-time constraints. Over the years, timed automata have been implemented in many software tools, one of which is the award-winning industry-strength tool UPPAAL.

Behind these tools lies a solid theory of timed automata, that comes with its own set of challenging questions. The goal of this course is to understand timed automata deeply and get acquainted with the different mathematical techniques used in its analysis.

A shorter version of this course can be found here.

Prerequisites

Theory of Computation

Logistics

The course will be held at Lecture hall 4 on Tuesdays and Thursdays at 2 PM.

Here is a tentative grading scheme.

Mid-semester exam 50%
End-semester exam 50%

Tutorials

Tutorial 1       Tutorial 2       Tutorial 3       Tutorial 4       Tutorial 5       Tutorial 6

Lectures

Number Date Subject Reading Material
1 Jan 7 Introduction to timed automata Slides
2 Jan 9 Timed languages and timed automata Slides
3 Jan 16 Language emptiness for timed automata Notes
4 Jan 21 Undecidability of inclusion Slides
5 Jan 23 A decidable case of language inclusion Slides
6 Jan 28 Discussion of Tutorial 2
7 Jan 30 Determinizing timed automata Slides
8 Feb 4 Discussion of Tutorial 3
9 Feb 6 Alternating timed automata Slides       Paper
10 Feb 13 Case-study: Pacemaker verification Slides       Jiang's slides       Paper
11 Feb 18 Timed automata with diagonal constraints Notes
Feb 25 Mid-semester Exam Question paper
12 Mar 11 Reachability algorithm using zones Notes
13 Mar 13 Operations on zones Partial notes
14 Mar 18 Non-convex abstractions Notes
15 Mar 21 Better abstractions through better constants Slides
16 Mar 25 Non-Zenoness
17 Apr 1 Discussion of Tutorial 4
18 Apr 3 Problem session Notes
19 Apr 8 Discussion of Tutorial 5
20 Apr 10 Discussion of Tutorial 6
21 Apr 15 Timed automata reachability is PSPACE-complete
22 Apr 17 Problem session