Model Checking: Theory and Practice
Paritosh K. Pandya
(January-May 1999)

Lecture schedule

(Click here for the Next Lecture)

Each lecture denotes a double lecture spanning 2:00 Hours.
** denotes advance topics. I don't promise to cover these!

Lecture 1 (done)

Introduction to Model-checking and course overview.
Monadic second-order logic over finite and infinite words, trees and graphs.

Lecture 2 (done)

Overview of Finite state automata.

Lecture 3 (done)

Decidability of MSO over words.

Lecture  4 (done)

Decidability of WS1S and presburger arithmetic.
Model checker MONA.

Lecture 5,  6 (done)

Omega-automata and its closure properties (except complementation)
Decidability of MSO over omega-words. Complexity.
Reductions between between Buchi, Muller, Rabin, Streett automata
and their complexities.

Lecture 7, 8 (done)

Complementation of omega-regular langauges:
Safra's determinisation construction.

Lecture 9 (by Safra) (done)

Determinisation and complementation of Streett automata

Lecture 10 (done)

Introduction to modal logics.
Linear propositional temporal logic
Embedding PTL in MSO

Lecture 11, 12 (done)

Modelchecking PTL : Vardi - Wolper approach and its complexity.

Lecture 13, 14 (done)

On-the-fly verification of PTL formulae

Lecture 15, 16 (done)

Computation Tree Logic CTL and CTL*
Embedding CTL* in MSO over infinite trees.
Modelchecking  algorithm for CTL* formulae and its complexity

Lecture 17 (5 April, 1999)

Efficient modelchecking algorithm for CTL and its complexity

Lecture 17 (7 April, 1999)

Extensions to Temporal Logic:
Tense logics over arbitrary linear order (PTnL). Monadic theories of various linean orders.
Logic PTnL with strict until and since operators, variety of operators their and expressiveness
Quantification (QPTnL),
Fixed point operators  (muPTnL)
Embedding and expressive power of temporal logics for discrete and dense Time.
Statement of Kamps Theorem.
First order Temporal Logic (FOLTL).

Lecture 18   (12 April)

Interval Temporal Logic of Halpern and Shoham
Quantified Discrete Duration Calculus (Zhou, Moskowski) QDDC
Embedding QDDC in MSO

Tool demonstration  (12 April)

Model checking QDDC using DCVALID and MONA (Minepump Example)
Verification of Esterel programs using DCEST (Bus Arbiter Example)

Tool demonstration (14 April)

Model checker  SPIN
Some examples of verification using SPIN
(Dining philosophers, Dekker's Mutual Exclusion)

Lecture 19  (26 April)

Symbolic model checking of modal mu calculus.
Symbolic model checking of CTL formulae.
Model checker SMV

Lecture 20, 21   (28 April,  10 May)

Real-time systems and their models: Timed state sequences.
Timed automata. Closure properties.
Regions construction and decidability of emptiness.
Symbolic representation of convex time regions using DBM and its manipulation.
Symbolic modelchecking of Timed systems using Uppaal, Hytech.

Lecture 23 (student seminar) (3 May) Rahul Jain

Fair CTL model-checking. Kripke structures with fairness requirements
(generalised Buchi and Streett acceptance sets). Fair paths.
Fair strongly connected components. Modelchecking algorithm.

Tool Demonstration (5 May) Amitava

Uppaal overview and features.
Fischer's mutual exclusion algorithm in Uppaal.

Lecture 24 (student seminar) (6 May) S. Krishnan

Memory efficient graph searching algorithms for model checking.

Lecture 24 (student seminar)  (11 May) Amitava

** Topology of  omega-languages. Borel classes. Rabin index,
       Retrospecitve Operators, Nets ...

Tool Demonstration (12 May)


Lecture 25 (omitted)

Extended Star-free  regular expressions
Characterisation of First-order definable finite and omega-languages
Characterisation of Languages definable in PTL: statement of Kamp's theorem

Lecture 26 (omitted)

Omega-tree automata. Statement of Rabin's tree theorem.
Decidability MSO over infinite trees. Variations (SnS, SwS).
Decidability of various logics based on  MSO over infinite trees.
Monadic Theory  of various linear orders (a la Shelah) and their decidability.

Lecture 26 (omitted)

** Proof of Rabin's tree  theorem.

Remaining Lectures on abstraction, induction and reduction to be planned.

References (highly incomplete)