Course CR05: Monadic Second Order Logic, Automata, Expressivity and Decidability

Lecturers: Matteo Mio (CNRS & ENS-Lyon) and Colin Riba (ENS-Lyon)

Lesson 1 (Matteo Mio, 16th Sept. 2016)

• Elements of First order Logic (signatures, models, Tarski truth, compactness theorem, Löwenheim-Skolem theorem, Gödel's completeness theorem)
• Fundamental undecidability results (Gödel, Church, Turing)
• Decidability of logical theories: outline of some methods by examples:
• quantifier elimination (First order theory of dense linear orders without endpoints)
• finite model property (monadic First order logic)

References:

1. Boolos, Burgess and Jeffrey, Computability and Logic (fifth edition), Cambridge University Press
2. D. Scott, M. Rabin, Finite Automata and Their Decision Problems (link)

Lesson 2 (Matteo Mio, 23rd Sept. 2016)

• Finite (nondeterministic) automata, regular languages, regular relations
• Closure properties: Boolean, cylindrification, instantiation, …
• Decidability of logical theories using automata
• Examples: Presburger arithmetic, WMSO, …
• Equivalence between WMSO and regular languages

References:

1. Wolfgang Thomas, “Automata on Infinite Objects”. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 133-192
3. Sasha Rubin, “Automatic Structures”, Phd Thesis 2008, (link)

Lesson 3 (Colin Riba, 30th Sept. 2016)

• Büchi automata, $\omega$-words, $\omega$-regular languages
• Closure under finite unions and finite intersections
• $\omega$-regular expressions, correspondence with $\omega$-regular languages

References:

1. Slides of the lecture course03.pdf
2. Wolfgang Thomas, “Automata on Infinite Objects”. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 133-192
3. D. Perrin and J.E. Pin, Infinite Words, Automata, Semigroups, Logic and Games, Pure and Applied Mathematics. Elsevier, 2004.

Lesson 4 (Matteo Mio, 7th Oct. 2016)

• Complementation of Büchi automata using congruences
• infinite Ramsey theorem
• Monadic Second Order logic of $(\mathbb{N},+1)$

References:

1. Wolfgang Thomas, “Automata on Infinite Objects”. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 133-192
2. A small manuscript describing how to obtain the finite Ramsey theorem from the infinite version using compactness of FO-logic. (LINK).

Lessons 5 and 6 (Colin Riba, 14th and 21th Oct. 2016)

• Deterministic Büchi automata (further results)
• Elements of Descriptive Set Theory (Polish space of infinite sequences, first few levels of Borel hierarchy)
• Muller automata: definitions, examples and basic properties
• Statement of McNaughton theorem
• Proof of McNaughton theorem using Safra construction
• Topological consequences: every $\omega$-regular language is a Boolean combination of $\Pi^0_2$ sets; if a set $L\subseteq A^\omega$ is $\omega$-regular and $\Pi^0_2$ then it is deterministic Büchi.

References:

1. Slides of the lecture course05.pdf
2. Wolfgang Thomas, “Automata on Infinite Objects”. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 133-192
3. D. Perrin and J.E. Pin, Infinite Words, Automata, Semigroups, Logic and Games, Pure and Applied Mathematics. Elsevier, 2004.

Lesson 7 (Matteo Mio, 4th November 2016)

• Applications of Büchi theorem: verification of finite state systems (Model checking).
• Logic LTL: syntax and semantics. Example of branching-time property not expressible in LTL
• MSO of the full binary tree: syntax and semantics.
• Examples of useful formulas: being a path, being a finite set, being a pruned subtree
• Applications: decidability of MSO($\mathbb{Z},\leq$) and of FO(closed subsets of $\{0,1\}^\omega$, $\subseteq$).

References:

1. C. Baier, J.P. Katoen, Principles of Model Checking, The MIT Press, 2008. (chapters 2,3,4,5).
2. Wolfgang Thomas, “Automata on Infinite Objects”. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 133-192
3. D. Perrin and J.E. Pin, Infinite Words, Automata, Semigroups, Logic and Games, Pure and Applied Mathematics. Elsevier, 2004.

The first references covers the material about LTL and Model checking linear time properties. The other two references covers most aspects of the MSO theory of the full binary tree.

EXERCISES (8 Nov 2016)

• First set of exercises. PDF
• More exercises will appear on this page, so make sure to check it out regularly

Lesson 8 (Colin Riba, 18th November 2016)

• Introduction to $\Sigma$-labeled trees, examples.
• Nondeterministic tree-automata (with Büchi and Muller conditions), examples.
• Basic properties: closure under union and intersections.
• Overview of the proof method for proving complementation.
• Infinite games on trees: definition, notion of determinacy, examples (IV.2.1, Ex. IV.3.2, Ex. IV.3.3 of Perrin-Pin)

References:

1. Slides of the lecture (PDF)
2. Chapter V of D. Perrin and J.E. Pin, Infinite Words, Automata, Semigroups, Logic and Games, Pure and Applied Mathematics. Elsevier, 2004.

Lesson 9 (Colin Riba, 25th November 2016)

• Two-player games on graphs and concept of positional strategy
• Positional determinacy of parity games (also on infinite graphs)
• Translation from Muller to parity games
• Complementation of tree automata.

References:

1. Slides of the lecture (PDF)
2. W. Thomas's “Languages, Automata and Logic”
3. - Chapter IV of D. Perrin and J.E. Pin, Infinite Words, Automata, Semigroups, Logic and Games, Pure and Applied Mathematics. Elsevier, 2004.

Lesson 10 (Matteo Mio, 9th December 2016)

• An example MSO-definable subset $A\subseteq\{0,1\}^\omega$ not definable in FO-logic (even positions)
• An example of two-player game which is not determined (due to D. Niwinksi, see reference below).
• $\omega$-product and weak-$\omega$-product of structures. Application: decidability of Skolem arithmetic $FO(\mathbb{N}^+,\times,P,<_{P})$ (see reference 2)
• Use decidability of MSO of the full binary tree to solve games of finite graphs

References:

1. D. Niwinski and E.Kopczynski, A simple indeterminate infinite game, (PDF available here)
2. Françoise Maurin, The Theory of Integer Multiplication with Order Restricted to Primes is Decidable, The Journal of Symbolic Logic, Vol. 62, No. 1 (Mar., 1997), pp. 123-130

Lesson 11 (Denis Kuperberg, 13rd Dec 2016)

• Characterization of regularity by one-sided Myhill-Nerode relation
• Recognition by finite monoid, equivalence with regularity (constructions DFA↔monoid, examples)
• Syntactic monoid, syntactic congruence, minimization, two-sided congruence of L on A*
• algebraic characterization of commutative languages and star-free languages

Lesson 12 (Denis Kuperberg, 16th Dec 2016)

• proof that star-free ⇒ aperiodic (other direction admitted)
• definition of varieties of monoids and languages, correspondence between the two (Eilenberg)
• profinite words, a little topology on the free profinite monoid
• equivalence between varieties of monoids and set of profinite identities (Reiterman)
• other classes (lattices, +-varieties, boolean algebras) and corresponding sets of equations
• examples of classes and their equations: aperiodic, commutative, cyclic, nilpotent, finite, cofinite

Exam: Date 11th of January, 2h long

Exercises (strongly recommended) to prepare for the exam:

• Exercises from 8 Nov prepared by Matteo Mio (and discussed during Lesson 10): PDF
• Exercises prepared by Denis Kuperberg covering the last two lectures: PDF
• Do all the exercises proposed in the slides of the lectures of Colin Riba.

Update: The exam of the 11h of January was the following: main.pdf

Rattrapage:

You can improve the final score of your exam by studying and presenting one of the following 9 papers.

Note 1: Each paper can be assigned to only one student. The rule is: First come, First served. To reserve a paper send an email to Matteo and Colin and Denis (all of us).

Note 2: the maximal improvement is +4 (perfect presentation). More realistically, +2/+3 should be possible with a good presentation.

1) Nondeterminism in the Presence of a Diverse or Unknown Future (LINK)

Automata on infinite words, games, link with infinite trees

2) Deciding Nondeterministic Hierarchy of Deterministic Tree Automata (LINK)

Automata on infinite trees, parity condition, decidability proof

3) Deciding Parity Games in Quasipolynomial Time (LINK)

Very recent result!!!: Complexity of parity games, you can stop at the end of section 2 (page 15)

4) The MSO+U theory of (N,<) is undecidable (LINK)

Extension of MSO on infinite words, undecidability proof.

5) Alternating automata, the weak monadic theory of trees and its complexity (LINK)

Alternating automata, the weak monadic theory of trees and its complexity. This is about an old well-known result about MSO on the infinite trees.

6) Unifying Büchi Complementation Constructions (LINK)

(extended version at : https://arxiv.org/pdf/1302.2675.pdf)

7) Simple Stochastic Parity Games (LINK)

This paper is about Stochastic parity games, a generalization of parity games where some moves can be made probabilistically.

8) Trees over Infinite Structures and Path Logics with Synchronization (LINK)

A generalization of the proof method of Büchi (to prove complementation of Büchi automata) allows the manipulation of automata running on certain kinds of infinite alphabets.

9) Probabilistic Automata on Finite words: Decidable and Undecidable Problems (LINK)

Problems related to finite-automata with probabilistic acceptance (as first studied by Rabin).