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.

    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