Model Checking: Theory and Practice
Paritosh K. Pandya
(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
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
Fixed point operators (muPTnL)
Embedding and expressive power of temporal logics for discrete and
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
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
Lecture 26 (omitted)
** Proof of Rabin's tree theorem.
Remaining Lectures on abstraction, induction and reduction to be planned.
References (highly incomplete)
Clarke and Wing survey for strategic directions.
Thomas handbook of TCS article
Thomas handbook of formal langauges article.
Madhavan Tutorial on omega automata
Madhavan Tutorial on LTL model checking
Narayan Kumar Tutorial on CTL* and CTL model checking
Vardi papers on alternating automata and modelchecking
McMillan book on symbolic model checking
Alur-Dill paper on "Theory of timed automata" TCS 126
Uppaal papers on convex region representation