Matteo Mio
PhD, CNRS Researcher

Course M2 CR05, ENS-Lyon
• Title: Logic, Automata and Decidability.
• Lecturers: Matteo Mio and Denis Kuperberg.
• Period: from September 2017 to December 2017.
• Number of Lectures: 12, 2h long.
Short Description:
• Some historical background: a logic formalism (e.g., first order logic) is used to express properties of models. The decision problem of a logic formalism is: for a fixed model M, is there an algorithm that takes as input a formula F and output YES if M satisfies F, and NO otherwise? The study of this problem (varying the logic and/or the models considered) gave birth to Computer Science in the late 1930s with the seminal results of logicians like Gödel, Church and Turing, among others. They proved that for many interesting models/logics the problem is undecidable. Despite this negative general state of affairs, a lot of research (from the 40's and still going on) has focused of identifying good logic/models with decidable decision problem.
• Automata and Logic: an important development took place in the 1950's when it was realized that the emerging theory of finite automata could be use to prove the decidability of interesting logical theories. There is indeed a deep link between some operations on automata (like union of regular languages) and logical operations (like the OR connective). Most importantly for Computer Science, the algorithms for solving the decision problem of certain logics can be used to verify the correctness of software (so called, Model Checking procedure).
• The goal of this course: the main objective of this course is to introduce the student to the theory of automata (including advanced kinds of automata such as Büchi automata) and to show how this theory can be used to solve the decision problem of certain logics and, finally, how to use these methods to verify the correctness of software.
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) and with some basic results (undecidability of first order logic, decidability of propositional logic using truth tables, etc).

Lesson 1: 12 September, Matteo Mio
• First order logic: syntax and semantics.
• Relational Structures, examples: (N,+,*), (R,+,*), (N,+,<), (Z,<), ({t,f},or,and,not), ...
• Several examples of properties about these structures expressed in FO-logic.
• Statements of main decidability results: finite structures, Gödel: (N,+,*), Tarski: (R,+,*), Presburger: (N,+,<)
• Proof of decidability of Monadic FO using finite model property.
References:
• Boolos, Burgess and Jeffrey, Computability and Logic (fifth edition), Cambridge University Press
• D. Scott, M. Rabin, Finite Automata and Their Decision Problems. LINK

Lesson 2: 19 September, Denis Kuperberg
• Notion of interpretation of a logic in another.
• Definitions of DFA and NFA.
• Closure properties of DFA and NFA: union, intersection, complement, projection.
• Decidability of FO(N,<) using automata, with position encoding of integers.
• Decidability of FO(N,+) (Presburger arithmetic) using automata, with binary encoding of integers.
• General result: if a FO structure is automatic (i.e. regular encoding and regular relations), then its theory is decidable.
Exercises:
• Show that + is not regular with position encoding.
• For which sets "I" of integers can we show FO(N,+,(modi)i in I) is decidable ?

Lesson 3: 26 September, Matteo Mio
• Proving decidability of FO-theories using finite-automata. Recap of the main ideas.
• Several Examples given in detail:
• FO(N,<) and F(N,<,+)
• FO(Z,<) and FO(Z,<,+) using interpretations.
• FO(Q,<) posed as a +1 question.
• FO(Boolean algebra of finite-cofinite subsets of naturals)
• FO(Full Binary Tree)
• FO(Finite sets with inclusion, Singleton predicate and order)
• Weak MSO of (N,<), decidability by mutual interpretation wit FO-theory above.
Exercises:
• Show that FO(Q,<) is regular (+1 point)
• Is WMSO(Z,<) decidable?
• Is WMSO(Full Binary tree) decidable? (+1 point)
• Is WMSO(Q,<) decidable? (+2 points)
• Is WMSO(N,<,+) decidable? (+5 points)

Lesson 4: 3 October, Matteo Mio
• Büchi Automata and omega-words basic definitions and examples.
• Simple closure properties of Büchi automata:
• Closure under Union
• Closure under intersection.
• Deterministic Bü chi automata are strictly less expressive than Nondeterministic Büchi automata.
• Application to Decidability of FO-theories:
• Regular Languages can be seen as omega-regular languages
• Decidability of FO(R,<)
• Decidability of all other theories proved decidabile using finite automata.

Lesson 5: 10 October, Matteo Mio
• Emptiness problem for Büchi is decidable.
• Complementation of Büchi automata (Büchi's proof using Ramsey theorem) (see THIS LINK)
• Corollary of the theorem: omega-regular expressions are equivalent to Büchi automata.
Exercises given during class:
• Construct Büchi automata accepting several examples of omega-languages.
• Prove decidability of MSO(N,<)
Suggested paper: it covers finite-automata and how to prove decidability of FO-theories using them.
• Sasha Rubin: Automata Presenting Structures: A Survey of the Finite String Case. Bulletin of Symbolic Logic 14(2): 169-209 (2008) (file available here: LINK )

Lesson 6: 17 October, Matteo Mio
• Decidability of MSO(N,<) using Büchi automata
• Equivalence between MSO(N,<) and Büchi automata
• Undecidability of full second order logic SO(N,<)
• I mentioned the Robinson theorem about undecidability of MSO(N,<,+).
See: Restricted set-theoretical definitions in arithmetic, Proc. Amer. Math. Soc., 9 (1958) 238-242. ( LINK )
• Correction of some exercises and Q/A session.
• Discussion of some of the type of questions which will appear in the mid-term exam.

Midterm Exam: 23 October, Matteo Mio
• Midterm exam (2 hours): (document available HERE )

Lesson 7 : 7 November, Matteo Mio
• Parity condition, Parity automata and determinization.
• Tree automata with parity condition. Definitions and statement of Rabin's theorem.
• Several examples of definable sets of trees.
• Definition of "encoding" of a structure using words/omega-words/trees. (see also article suggested during Lecture 5)
• Examples of structures encodable using tree automata: Skolem arithmetic, MSO(full binary tree), MSO(Q,<).

Lesson 8 : 14 November, Denis Kuperberg
• MSO and generalized regular expressions as ways to define regular languages.
• Fragments: FO, star-free expressions.
• Languages recognized by finite monoids, equivalence with regularity.
• Syntactic monoid, syntactic congruence, minimization of monoids.
• Idempotent power, aperiodic monoids.
• Schützenberger Theorem: FO-definable <=> Star-free <=> Aperiodic monoid
Exercises:
• Show that a monoid is aperiodic if and only if it contains no non-trivial group.
• Which of the two languages (aa+ab)* and (aba)* is FO-definable ? Give a FO formula and a star-free expression for this language.

Lesson 9 : 21 November, Denis Kuperberg
• proof that FO+syntactic sugar (0,last, succ) is equivalent to FO on finite words.
• proof that Star-free => FO-definable
• Green's relations in monoids: R,L,J,H.
• Cayley Graphs of monoids with generators.
• Green's Lemma, Eggbox Diagrams
• Star-Height and Generalized Star-Height problems.
References:
Exercises:
• Eggbox diagrams for the following languages: (abc)*, {a,aba}, (a(ab)*b)*

Lesson 10 : 28 November, Denis Kuperberg
• Correction of exercises, tool demo.
• Transducers: Letter-to-Letter, DFT, NFT.
• Undecidability of DFT intersection emptyness via Post Correspondence Problem.
• Some closure and decidability properties of DFT/NFT.
• Model-checking of MSO: definition, example, decidability proof.
• Church synthesis problem: definition and example.
Reference:
• Semigroup Online: Online tool computing syntactic monoids and membership in various classes.
Exercises:
• Closure of NFT relations by composition
• Instance of the Church synthesis problem

Lesson 11 : 12 December, Denis Kuperberg
• Correction of exercises, example of transducers composition.
• Definition of 2-player games of infinite duration with perfect information
• Winning strategies, finite-memory, memoryless
• Determinacy, Martin Theorem
• Regular conditions: Reachability, Safety, Büchi, Co-Büchi, Parity, Rabin, Streett, Muller
• Positional determinacy of Parity and Rabin, Finite-memory (exponential) determinacy of Streett and Muller
Exercises:
• Equivalence of games with alternating games (players alternate)
• Equivalence of acceptance conditions on vertices with acceptance on edges.

Lesson 12 : 19 December, Denis Kuperberg
• Correction of exercises.
• Algorithm for Reachability/Safety games with attractor.
• Algorithm for Büchi/coBüchi games with recurrence set and strict attractor.
• Definition of games for truth of a formula (FO,MSO).
• Ehrenfeucht-Fraïssé games for FO
• Applications: undefinability of finiteness or (aa)* in FO.