M2 Course, ENSLyon
 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:

Lecture 1 (September 13th, Denis Kuperberg)

Overview of verification: systems, specifications, modelchecking, 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 SecondOrder 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): 169209 (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

NLcompleteness for DFA emptiness, inclusion of NFA into DFA.

PSPACEcompleteness for universality of NFA.

EXPSPACEcompleteness 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)

FirstOrder Logic (FO)

StarFree Expressions

Equivalence LTL<=>FO<=>StarFree (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 <=> Starfree (admitted)

LTLdefinability is decidable (and PSPACEcomplete if input is a DFA)

Lecture 6 (October 18th, Matteo Mio)

omegawords, MSO (over omegawords), omegaregular expressions, Buchi automata (DBA and NBA).

Example of MSOdefinable languages of omegawords.

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.

Omegaregular expressions.

Equivalence between Omegaregular 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: omegaregular 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)

Omegasemigroups

Signature, axioms

Free omegasemigroup

Language recognized by an omegasemigroup

Equivalence between finite omegasemigroups and finite Wilke algebras.

Equivalence between finite Wilke algebras and omegaregular languages

From finite Wilke algebra to omegaregular 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 stateautomata

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:

Lecture 10 (December 6th, Denis Kuperberg)

Omegaregular synthesis

Büchi games

Parity games
 Positional determinacy
 Nondeterministic algorithm
 Deterministic algorithm, by recurrence

Omegaregular games: composing a game with an automaton

Goodforgames automata
 Definition [HP06]
 Use for solving omegaregular games
 Example of a Büchi GFG automaton [BKKS13]

References:

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(13): 183220 (1992)

Another nice (different) proof: Eryk Kopczynski, Damian Niwinski:
A simple indeterminate infinite game. Logic, Computation, Hierarchies 2014: 205212.

Nonconstructive proof that the down/up closures of any language of finite words are regular.

Application of the theory of Büchi automata:
 Decidability of FirstOrder 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): 614633 (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: