M2 Course, ENS-Lyon

• Title: Logic, Automata and Games for Advanced Verification
• Lecturers: Matteo Mio and Denis Kuperberg.
• Period: from September 2018 to December 2018.
• Number of Lectures: 12, 2h long.

Short Description:

The field of verification is concerned with proving properties of systems, for instance in order to avoid bugs in software.
Typically, a specification is given in a logical formalism, together with the description of a system, and an algorithm must decide whether the system complies with the specification.
It is also possible to give only a specification, and ask the algorithm to build a system complying with it. This is called the Synthesis Problem.

In this course, we will explore such formalisms, and show how the wanted algorithms can be obtained thanks to constructions using different models of automata and games.

Prerequisites: ideally the students need to have some basic knowledge on standard finite automata and regular languages. We will anyway provide some notes during the course to refresh these notions. The students are also supposed to have already been exposed to (first order and propositional) logic, be familiar with the meaning of the usual connectives (and, or, not, exists, forall).

Documents:

• the Midterm Homework . The solutions.
• the Final Exam with solutions .
• From CR05: Logic, Automata and Decidability in 2017-2018
  • The midterm exam
  • The final exam

• Lecture 1 (September 13th, Denis Kuperberg)
  
  • Overview of verification: systems, specifications, model-checking, synthesis
  • Modelling with Automata
    • NFA, DFA, regular expressions, regular languages.
    • Equivalence of NFA with DFA. Equivalence with expressions admitted.
    • Specifying systems and specifications as regular languages.
    • Model checking algorithm: checking that system S satisfies specification L.
  • Monadic Second-Order Logic (MSO)
    • Syntax of MSO.
    • Valuations, Semantics of MSO, language of a formula.
    • Syntactic sugar.
    • Exercises: building formulas for specific languages.
    • References: Automata theory, an algorithmic approach, Lecture notes by Javier Esparza



• Lecture 2 (September 20th, Matteo Mio)
  
  • Equivalence between MSO and finite automata.
  • From MSO to automata
    • Alternative presentation of MSO using only second order quantifiers. Interpretation over (N,<) with quantification over finite subsets.
    • Proof by induction that every MSO formula can be expressed by a NFA (interpreting a finite subset with a finite word over {0,1}).
      Critical case: existential quantifier is handled by nondeterminism.
    • References: Sasha Rubin: Automata Presenting Structures: A Survey of the Finite String Case. Bulletin of Symbolic Logic 14(2): 169-209 (2008)
  • From Automata to MSO
  • Write a sentence in MSO: there exists a run such that the run is accepting
  • Express the run as quantification over a tuple of finite subsets (coding a sequence of states)



• Lecture 3 (September 27th, Denis Kuperberg)
  
  • Clarification on different flavours of MSO.
    • Equivalence between MSO on finite words and finite automata.
    • Existential normal form for MSO formula.
  • Complexity considerations for DFA, NFA, MSO
    • NL-completeness for DFA emptiness, inclusion of NFA into DFA.
    • PSPACE-completeness for universality of NFA.
    • EXPSPACE-completeness for universality of regular expressions with squaring.
    • Nonelementary hardness for MSO emptiness (admitted)
    • Size complexity of operations: Complement, Projection, Union.



• Lecture 4 (October 4th, Denis Kuperberg)
  
  • Reactive systems, deterministic transducers
  • Function and language associated to a deterministic transducer
  • Transducer realizing a specification (on finite words)
  • The Church Synthesis problem (on finite words)
  • Safety games
    • Plays, strategies, positional strategies
    • Positional determinacy
    • Algorithm for finding winning regions in linear time.
  • Solution to the synthesis problem.



• Lecture 5 (October 11th, Denis Kuperberg)
  
  • Linear Temporal Logic (LTL)
  • First-Order Logic (FO)
  • Star-Free Expressions
  • Equivalence LTL<=>FO<=>Star-Free (admitted except LTL=>FO)
  • Monoids
    • Definitions: monoids, morphisms, quotient, submonoids
    • Language recognized by a triplet (M,h,P),
    • Equivalence with regular languages via transition monoid
    • Syntactic monoid, syntactic congruence (on Σ* or on any monoid)
    • Aperiodic monoids
  • Finite aperiodic monoid <=> LTL <=> FO <=> Star-free (admitted)
  • LTL-definability is decidable (and PSPACE-complete if input is a DFA)



• Lecture 6 (October 18th, Matteo Mio)
  
  • omega-words, MSO (over omega-words), omega-regular expressions, Buchi automata (DBA and NBA).
  • Example of MSO-definable languages of omega-words.
  • Examples and properties of NBA and DBA
    • NBA are closed under union (easy) and intesection (not just straigthforward product construction).
    • Fact (without proof, see Lecture 7): NBA are closed under complementation.
    • Corollary: Equivalence between MSO and NBA.
    • Decidability of emptyness of NBA. Corollary: decidability of MSO.
    • There are NBA languages ("contains only finitely many a's ") not definable by DBA (proof was given).
    • Equivalence between DBA and limits languages of finite words.
  • Omega-regular expressions.
    • Equivalence between Omega-regular expressions and NBA.
  • Muller automata. Equivalence with NBA.



• Lecture 7 (October 25th, Matteo Mio)
  
  • Parity Condition
    • Nondeterministic Parity automata = NBA (proof)
    • Theorem (without proof): Nondeterministic Parity automata = Deterministic Parity automata.
    • Theorem (without proof): Parity Games are positionally determined.
    • Corollary: omega-regular games can be solved automatically.
  • Infinitary Ramsey Theorem (with proof).
  • Buchi's theorem: NBA are effectively closed under complementation (proof using Ramsey theorem)



• Lecture 8 (November 8th, Denis Kuperberg)
  
  • Omega-semigroups
    • Signature, axioms
    • Free omega-semigroup
    • Language recognized by an omega-semigroup
    • Equivalence between finite omega-semigroups and finite Wilke algebras.
  • Equivalence between finite Wilke algebras and omega-regular languages
    • From finite Wilke algebra to omega-regular expression
    • From NBA to finite Wilke algebra via transition matrices.
    • Exercise: Finish the above translation, find accepting set P.
  • Reference: Semigroups and automata on infinite words, by Perrin and Pin.



• Lecture 9 (November 22nd, Matteo Mio)
  
  • Probabilistic (Rabin) finite state-automata
    • Definitions and interpretation as [0,1]-valued functions and as languages of words using cutoffs.
    • Some basic closure properties: product and (1-)
    • Every regular language is a probabilistic language L(A,0).
    • Theorem (with proof): there exists a prob. automaton A and real r such that L(A,r) is not regular.
  • Overview of results from [2]:
    • Construction of a probabilistic automaton A such that L(A,r) is not regular for all r.
    • Proof (by reduction to an undecidable problem, see [3]) that the problem of determining if L(A,r) is regular is generally undecidable.
  • References:
    • [1] Seminal 1963 paper of Rabin.
    • [2] Nice paper of Fijalkow and Skrzypczak.
    • [3] Nice paper of Gimbert and Oualhadj.


• Lecture 10 (December 6th, Denis Kuperberg)
  
  • Omega-regular synthesis
    • Büchi games
    • Parity games
    • Positional determinacy
    • Nondeterministic algorithm
    • Deterministic algorithm, by recurrence
    • Omega-regular games: composing a game with an automaton
    • Good-for-games automata
    • Definition [HP06]
    • Use for solving omega-regular games
    • Example of a Büchi GFG automaton [BKKS13]
  • References:
    • Wikipedia page on parity games: useful information, algorithms and example.
    • [HP06] Solving games without determinization, by Henzinger and Piterman: original definition of GFG automata
    • [BKKS13] Nondeterminism in the presence of diverse or unknown future, by Boker, Kupferman, Kuperberg and Skrzypczak: examples and properties of GFG automata.


• Lecture 11 (December 13th, Matteo Mio)
  
  • Existence of nondetermined games of infinite duration
    • Idea of copycat strategy and strategy stealing arguments.
    • Parallel (concurrent) composition of games, from Game Semantics.
    • Proof that the "Ultrafilter game" is not determined.
    • Proof source: Andreas Blass: A Game Semantics for Linear Logic. Ann. Pure Appl. Logic 56(1-3): 183-220 (1992)
    • Another nice (different) proof: Eryk Kopczynski, Damian Niwinski: A simple indeterminate infinite game. Logic, Computation, Hierarchies 2014: 205-212.
  • Nonconstructive proof that the down/up closures of any language of finite words are regular.
  • Source: L. H. Haines. On free monoids partially ordered by embedding, Journal of Combinatorial Theory, 6(1), 1969.
  • See also Wikipedia page on Higman's lemma.
  • Application of the theory of Büchi automata:
    • Decidability of First-Order logical theories.
    • Main example: FO( Reals, +, 0, Nat(_) )
    • Reference: B. Boigelot, S. Jodogne, P. Wolper: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3): 614-633 (2005)



• Lecture 12 (December 20th, Denis Kuperberg)
  
  • Simulation games
  • Succinctness of GFG automata
    • GFG NFA determinization is linear (from midterm homework)
    • coBüchi GFG automata determinization is exponential (sketched, see [KS15])
    • Büchi GFG automata determinization is quadratic (admitted, see [KS15])
  • GFGness problem
  • NFA GFGness problem is in P (from midterm homework)
  • coBüchi GFGness problem is in P (admitted, see [KS15])
  • Büchi GFGness problem is in P (proved, see [BK18])
  • Parity GFGness problem is in EXPTIME (proved, see [HP06])
  • References:
    • [KS15] Determinisation of good-for-games automata, by Kuperberg and Skrzypczak
    • [BK18] Büchi good-for-games automata are efficiently recognizable, by Bagnol and Kuperberg