Shibashis Guha (firstname@tifr.res.in)
Tuesday, Thursday: 9:30 - 11
Please send a mail to the instructor for attending lectures/seminars or to get course updates.
This course deals with foundations of automatic verification. The lectures will broadly include topics from automata over infinite words, model-checking, and synthesis of reactive systems. In addition, there will be seminars by students on more advanced topics from research papers in the field.
Automata over Omega-words, omega-regular languages, model-checking with nondeterministic Buchi automata (NBW): intersection and emptiness checking for Buchi automata, complementation of NBWs: Kupferman and Vardi’s construction, Michel's lower bound, Buchi’s theorem and monadic second-order logic (MSO) with 1-successor, other acceptance conditions (Co-Buchi, Parity, Rabin, Muller, Streett), alternating Buchi automata and Miyano Hayashi construction
Kripke structure, Linear Time Temporal Logic (LTL), LTL model-checking: LTL to NBW (Vardi-Wolper construction), computational tree logic (CTL) and its model-checking, symbolic model-checking and BDD, notions of program equivalence: traces, bisimulation etc, Hennessy-Milner logic,model-checking probabilistic systems, Markov chains: Reachability and limit behaviours, probabilistic CTL
Reactive synthesis: infinite games on graphs: two-player zero-sum games, reachability and safety games, Buchi and CoBuchi games, parity games and memoryless determinacy, NP-coNP membership, Zielonka's algorithm, Rabin games and its NP-completeness
Principles of Model Checking by Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.
Automata Theory and Model Checking, Chapter by Orna Kupferman in Handbook of Model Checking, Springer, 2018.
Lectures in Game Theory for Computer Scientists, Edited by Krzysztof R. Apt and Erich Grädel, Cambridge University Press, 2011
Infinite Games, Lecture notes by Martin Zimmermann, Felix Klein and Alexander Weinert.
Reactive Systems: Modelling, specification and verification by Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jirí Srba, Cambridge University Press, 2007.
LTL synthesis
Counterexample guided abstraction refinement (CEGAR)
Bounded model-checking
| Class # | Date | Topics Covered | Resources |
| 1 | Th, 18/08 | introduction to the course; overview of formal verification and reactive synthesis | |
| 2 | Tu, 23/08 | Omega-regular languages, Büchi automata: NBW, DBW, closure under union and intersection | [2]: Sec 2.1, 2.2.1 |
| 3 | Th, 25/08 | Complementation: DBW, NBW (Kupferman and Vardi construction) | [2]: Sec 2.2.2 |
| 4 | Tu, 30/08 | Complementation of NBW (Kupferman and Vardi construction) | [2]: Sec 2.2.2 |
| 5 | Th, 01/09 | Michell's lower bound proof for NBW complementation, limit of a language and DBW | [2]: Sec 2.2.2, Sec: 2.3 |
| 6 | Tu, 06/09 | CoBuchi, Rabin, Streett, Parity, Muller acceptance conditions | [2]: Sec 3 |
| 7 | Th, 08/09 | Minimization of DBW is NP-complete (Blackboard presentation by students) | FSTTCS 2010 paper by Sven Schewe |
| 8 | Tu, 13/09 | Translations between acceptance conditions, typeness | [2]: Sec3.1 |
| 9 | Th, 15/09 | Lower bound on blow-up from DSW to NBW translation, Decision procedures for NBW and DBW | [2]: Sec3.1, Sec 4 |
| 10 | Tu, 20/09 | Buchi's theorem: NBW and S1S (MSO with one successor) | Chapter by Madhavan Mukund |
| 11 | Th, 29/09 | Alternating Büchi automata (ABW) | [2]: Sec 5.1 |
| 12 | Tu, 04/10 | Closure properties of ABW, weak alternating automata, quadratic blow-up in complementation | [2]: Sec 5.2, TOCL'01 paper by Kupferman and Vardi |
| 13 | Sa, 08/10 | Miyano-Hayashi (breakpoint) construction, expressiveness of nondeterministic, universal, alternating Büchi and CoBüchi automata, decision procedures on ABW | [2]: Sec 5.2, 5.3 |
| 14 | Tu, 11/10 | Linear temporal logic: syntax and semantics, distributive and expansion laws | [1]: Sec 5.1 |
| 15 | Tu, 18/10 | LTL: positive normal form (PNF), weak until PNF, release PNF, LTL to ABW | [1]: Sec 5.1, 5.2, [2]: Sec 6.1 |
| 16 | Th, 20/10 | LTL to generalised NBW (Vardi-Wolper construction) | [1]: Sec 5.2, Notes by Madhavan Mukund |
| 17 | Th, 27/10 | Lower bound for LTL to NBW construction, PSPACE-completeness of LTL model-checking and satisfiability | [1]: Sec 5.2, Lecture handout |
| 18 | Tu, 01/11 | Student presentation: Limit deterministic Büchi automata and its equivalence with NBW | J. ACM 1995 paper by Yannakakis and Courcoubetis |
| 19 | Tu, 03/11 | Student presentation: Good-for-MDP automata and suitable limit deterministic Büchi automata | Summary of the presentation |
| 20 | We, 09/11 | Expressiveness of LTL, computational tree logic (CTL) and its syntax | Lecture handout[1]: Sec 6.1, 6.2.1 |
| 21 | Su, 13/11 | CTL: semantics, existential and positive normal forms, model checking | [1]: Sec 6.2, 6.4 |
| 22 | Tu, 15/11 | Comparison of LTL and CTL, Succinctness of LTL formulae, CTL*, bisimulation | [1]: Sec 6.3, 6.4.3, 6.8, 7.1 |
| 23 | Th, 17/11 | Game characterization of bisimulation, simulation preorder and equivalence, bisimulation and CTL/CTL* equivalence | [1]: Sec 7.1, 7.2, [5]: Sec 3.5 |
| 24 | Th, 24/11 | Binary decision diagram (BDD), reduced ordered BDD, if-then-else normal form | Notes by Andersen |
| 25 | Tu, 29/11 | Symbolic CTL model checking, overview of abstraction refinement, bounded model checking, partial order reduction, symmetry reduction | [1]: Sec 6.7 |
| 26 | Sa, 3/12 | Markov chains, measure and cylinder sets, bottom strongly connected components, model checking, steady-state distribution, PCTL syntax, semantics | [1]: Sec 10.1, 10.2 |
| 27 | Tu, 6/12 | LTL synthesis, 2EXPTime membership, ω-regular games | Notes by Shaull Almagor |
| 28 | Th, 8/12 | Student presentation on modelling and verification using NuSMV, assignment demo on lift models | Slides prepared by student |