Matteo Mio
PhD, CNRS Researcher
Course M2 CR05, ENSLyon
 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 FOlogic.
 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,+,(mod_{i})_{i in I}) is decidable ?
Lesson 3: 26 September, Matteo Mio
 Proving decidability of FOtheories using finiteautomata. 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 finitecofinite 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 FOtheory 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 omegawords 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 FOtheories:
 Regular Languages can be seen as omegaregular 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: omegaregular expressions are equivalent to Büchi automata.
Exercises given during class:
 Construct Büchi automata accepting several examples of omegalanguages.
 Prove decidability of MSO(N,<)
Suggested paper: it covers finiteautomata and how to prove decidability of FOtheories using them.
 Sasha Rubin:
Automata Presenting Structures: A Survey of the Finite String Case. Bulletin of Symbolic Logic 14(2): 169209 (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 settheoretical definitions in arithmetic, Proc. Amer. Math. Soc., 9 (1958) 238242. ( LINK )
 Correction of some exercises and Q/A session.
 Discussion of some of the type of questions which will appear in the midterm 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/omegawords/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, starfree expressions.
 Languages recognized by finite monoids, equivalence with regularity.
 Syntactic monoid, syntactic congruence, minimization of monoids.
 Idempotent power, aperiodic monoids.
 Schützenberger Theorem: FOdefinable <=> Starfree <=> Aperiodic monoid
Exercises:
 Show that a monoid is aperiodic if and only if it contains no nontrivial group.
 Which of the two languages (aa+ab)* and (aba)* is FOdefinable ? Give a FO formula and a starfree 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 Starfree => FOdefinable
 Green's relations in monoids: R,L,J,H.
 Cayley Graphs of monoids with generators.
 Green's Lemma, Eggbox Diagrams
 StarHeight and Generalized StarHeight 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: LettertoLetter, DFT, NFT.
 Undecidability of DFT intersection emptyness via Post Correspondence Problem.
 Some closure and decidability properties of DFT/NFT.
 Modelchecking 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 2player games of infinite duration with perfect information
 Winning strategies, finitememory, memoryless
 Determinacy, Martin Theorem
 Regular conditions: Reachability, Safety, Büchi, CoBüchi, Parity, Rabin, Streett, Muller
 Positional determinacy of Parity and Rabin, Finitememory (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).
 EhrenfeuchtFraïssé games for FO
 Applications: undefinability of finiteness or (aa)* in FO.
Additional material:
 Automata on infinite words with various conditions: link
 Exercises for Logic and Automata, by Anca Muscholl: link 1 and link 2
 Course and exercises on Games and Synthesis, by Anca Muscholl: link
 A chapter on Automata, Logic and Games, covering MSO, parity condition (called here "Rabin chain condition"), determinacy and attractors in games, by Wolfgang Thomas: link
 A chapter on EhrenfeuchtFraïssé Games, by Neil Immerman: link