Date 
Description 
References/Lecture Notes 
July 24 
Introduction to cyberphysical systems modeling and verification
[Slides ] 

July 26 
Green Sheduling and Multimode Systems [Slides] 
Green scheduling, Constantrate Multimode systems 
July 31 
Green Sheduling and Multimode Systems (Contd.) [Slides] 
Green scheduling, Constantrate Multimode 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 modelchecker 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 
Languagetheoretic 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 Midsemester exams 

September 13 
No class due to Midsemester 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
EventClock 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
