Ashutosh Trivedi: Courses/CS 620

Logistics

Instructors: Krishna S. (krishnas@cse) and Ashutosh Trivedi (trivedi@cse)
Prerequisites CS 207 (Discrete Structures) and CS208 (Automata Theory and Logic)
Credit structure : Lecture:3, Tutorial:0, Practical:0, Credit:6.
Lectures: Wednesday and Friday (11:00am—12:30pm)
Office hours: Ashutosh Trivedi (Friday 16:00—17:00), SIA 108, KReSIT Bldg.
Krishna S. (Friday 16:00—17:00), CFDVS, Mathematics building basement.
Venue :
- Lectures SIC305, 3nd floor, 'C' Block, KReSIT building
- Office hours: SIA 108, 1st floor, 'A' Block, KReSIT building

Relevant Textbooks

Rajeev Alur. Principles of Embedded Computation. Available online.
Edward A. Lee and Sanjit A. Seshia, Introduction to Embedded Systems, A Cyber-Physical Systems Approach, http://LeeSeshia.org, ISBN 978-0-557-70857-4, 2011.
Clarke, Grumberg, Peled. Model Checking. . MIT Press, 1999.
Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

Grading

Topics

Part I: Formal Modeling

Modeling and verification of discrete systems:
- a short introduction
- Modeling: Finite automata, regular languages, and their properties
- Decidability of emptiness and universality problems
- Specification: reachability, safety, and liveness properties
- Introduction to temporal logics CTL and LTL Verification
- Model-checking and satisfiability problems
Modeling timed systems
- Timed automata, timed regular languages, and their properties
- Decidability of emptiness problem via "region" construction
- Undecidability of universality problem and its implications (language inclusion and complementation)
Some generalizations of timed automata and their decision problems
- Modeling optimal scheduling and planning problems using priced timed automata
- Modeling timed systems under uncertainties using probabilistic timed automata
- Modeling Uncontrollable Non-Determinism using timed games
Introduction to hybrid automata
- Rectangular, Singular, and Stopwatch Hybrid Automata
- Undecidability of reachability problem
- Decidable subclasses and corresponding algorithms

[Mid-semester Exams]

Part II: Tools for Modeling for Cyber-Physical Systems

Timed model-checker UPPAAL
Hybrid model-checker HyTech
Stateflow/Simulink

Part III: Verification and Synthesis

Specification of properties of timed systems
- Reachability, safety, and liveness properties
- Introduction to real-time logics TCTL, TPTL, and MTL
- Decidability results for model checking and satisfiability problems for these logics
Coping with undecidability: time-bounded verication
- bounded-model checking: a success story
- time-bounded model checking for MTL
- time-bounded reachability problem for hybrid automata
Automatic Synthesis
- Controller Synthesis via Two-player Games
- Code-generation from formal models

[End-semester Exams]

Schedule and Lecture Notes

Date	Description	References/Lecture Notes
July 24	Introduction to cyber-physical systems modeling and verification [Slides ]
July 26	Green Sheduling and Multi-mode Systems [Slides]	Green scheduling, Constant-rate Multi-mode systems
July 31	Green Sheduling and Multi-mode Systems (Contd.) [Slides]	Green scheduling, Constant-rate Multi-mode systems
August 2	Extended Finite State Machines [Slides]	class notes and lecture ntoes by Lygeros, Tomlin, and Sastry
August 7	Continuous Dynamical System [Slides]	class notes and lecture ntoes by Lygeros, Tomlin, and Sastry
August 9	Institute Holiday
August 14	Hybrid Automata: Syntax, Semantics, and Examples [Slides]	class notes and lecture ntoes by Lygeros, Tomlin, and Sastry
August 16	Timed Automata: Syntax, Semantics, and Examples	A theory of timed automata
August 21	Guest lecture by Krishna S. region construction and temporal logic LTL/CTL
August 23	Class cancelled due to FORMATS'13 conference
August 28	Introduction to SPIN model-checker by Ganesh K. Narwane	SPIN website and a Tutorial
August 30	Introduction to UPPAAL model checker by Ganesh K. Narwane and Devendra Bhave	UPPAAL website and a tutorial.
September 4	Language Theoretic Properties of Timed Automata: finite automata closure, determinization, and alternation [Slides]	J. E. Hopcroft, R. Motwani and J. D. Ullman. Introduction to Automata Theory, Languages and Computation
September 6	Language-theoretic Properties of Timed Automata: closure under union, intersection, and decidability of emptiness problem via region construction [Slides]	Alur and Dill' 94, Chapter 9 of "Principles of Model Checking" book by Baier and Katoen, Chapter 6 from principles of embedded computation by Rajeev Alur.
September 11	No class due to Mid-semester exams
September 13	No class due to Mid-semester exams
September 16	Quiz 1
September 18	Timed Automata: properties and determinizability (lecture notes first and second by B. Srivathsan)	Alur and Dill' 94, Chapter 9 of "Principles of Model Checking" book by Baier and Katoen, Chapter 6 from principles of embedded computation by Rajeev Alur, and Event-Clock Automata .
September 20	Class merged with the talk by Ansuman Banerje on Counterexample Ranking Using Mined Invariants (Venue: SIC 205, 'C' Block, 02nd Floor from 12noon)
September 25	Abstractions for Timed Automata (guest lecture by B. Srivathsan)	slides

Additional Reading

Page 18 of ( Is your model-checker on time: L. Aceto and F. Laroussinie) for PSPACE-hardness proof of the reachability/emptiness problem for timed automata
Section 3 of (Timed Automata: Semantics, Algorithms and Tools: J. Bengtsson and W. Yi) for algorithms to manipulate Zones
Page 29 (Section 5.2) of (A theory of timed automata: R. Alur and A. Dill for undecidability of the Universality problem

Notes

We are now using Piazza for class discussion. Please use this system to get quick help from classmates, TAs, and instuctors. Rather than emailing questions to the teaching staff, the instructors encourage you to post your questions on Piazza. Find our class page at: https://piazza.com/iitb.ac.in/fall2013/cs620/home
Project grades are available here
Final grades are available here