Automata, Verification, and Infinite Games (Aug - Dec 2022)

    Instructor

    • Shibashis Guha (firstname@tifr.res.in)

    Lecture Hours

    • Tuesday, Thursday: 9:30 - 11

    Venue

    • STCS seminar room (A 201)

      Please send a mail to the instructor for attending lectures/seminars or to get course updates.

    Course Description

    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.

    Course Topics

      • 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

    References

      1. Principles of Model Checking by Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.

      2. Automata Theory and Model Checking, Chapter by Orna Kupferman in Handbook of Model Checking, Springer, 2018.

      3. Lectures in Game Theory for Computer Scientists, Edited by Krzysztof R. Apt and Erich Grädel, Cambridge University Press, 2011

      4. Infinite Games, Lecture notes by Martin Zimmermann, Felix Klein and Alexander Weinert.

      5. Reactive Systems: Modelling, specification and verification  by Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jirí Srba, Cambridge University Press, 2007.

    Seminar Topics (TBD)

      • LTL synthesis

      • Counterexample guided abstraction refinement (CEGAR)

      • Bounded model-checking

    Schedule

        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