A topical course in Computer Science

Automata and Verification

Instructor:  Paritosh K. Pandya
Room A249
Phone: (tifr) Ext. 2551
Email:  pandya@tifr.res.in
Time:  Tuesday 11:00 to 13:00 a.m  In Room No. A212
Friday 11:00 to 13:00 a.m. In Room No. A21 

First Lecture: 21 January 2006.
 

Theory of Computation deals with foundational questions about compurational mechanisms and their  computing power culminating in in the treatment of questions "what are limits to computation". Verification of system explores mathematical techniques to analyse and guarantee the desirable properties of system behaviour. This course will cover some basic foundations of automata based verification of systems.

An emphasis in the course will be on Seminar presentations and Solution to Exercises.

Key words / areas: Automata, automata and logics, omega-automata, timed automata.

The course will start with a quick overview of theory and applications of finite state automata.

Different variants of omega-automata (Buchi, Muller, Rabin,...) will then introduced and their relations will be investigated.

Connections between automata and logics will be explored. Monadic and temporal logics as well as their automata based decision procedures will be presented.

The course will also cover theory and applications of timed automata and their usage for reasoning on real time systems.  Some real-time logics may also be presented.

Textbooks

Dexter Kozen, Automata and Computability

Hopcroft and Ullman, Introduction to Automata Theorey, Languages and Computation

Clarke, Peled, Grumberg, Model Checking.

Sections

  • Syllabus
  • Lecture Schedule
  • Homework Assignments
  • Seminar topics
  • References
  • Links

    • Lecture Slides

    Last modified by Paritosh Pandya on 22 January 1999.