Formal methods course, M2

• Lesson 1, Büchi automata
• Lesson 2, Monadic second order logic
• Lesson 3, Regular languages and logic
• Lesson 4, The Linear Temporal Logic (LTL)
• Lesson 5, The First-Order Logic of Linear Order and Kamp’s Theorem
• Lesson 6, Star-free sets, aperiodic monoids and first-order logic : here and here
• Lesson 7, Introduction to B specification language

Topics for projects (contact Catalin or Julien if you cannot get a copy of one of the references)

1. Memoryless determinacy of two-player games (chapters 2 and 6 of this book).
2. Closure under complementation of tree automata (chapters 2 and 8 of the same book) (to be presented by Mikhail Dubov).
3. Safra trees and closure under complementation of Büchi automata (chapter 1 and 3 of the same book) (to be presented by Cordero Christophe).
4. Schützenberger’s Theorem on the equivalence between star-free languages and languages accepted by finite aperiodic monoids (here) (to be presented by MALALANIRAINY Rakotoson Tina).
5. A theorem by Imre Simon that a language is piecewise testable if and only if it is recognized by a finite F-trivial monoid (here) (to be presented by Mónika Csikós).
6. A direct proof of the expressive equivalence between the Linear Temporal Logic and the \omega-regular languages which are accepted by aperiodic monoids (section 8 of this paper).
7. A “faster” procedure for constructing Büchi automata from LTL formulas (here) (to be presented by Daniel Antunes).
8. Separability of LTL formulas (Theorem 2.4 in this paper or also in this version).
9. The Krohn-Rhodes decomposition of deterministic automata – three variants here, here and here

Bibliography

• Kamp’s Theorem
• Connections between LTL, first-order logic, automata, star-free sets and aperiodicity
• A book on automata, logics and games

Topics for internships

• Logical modeling of strategic interactions in multi-agent systems
• Decidability problems for linear recurrent sequences: the Skolem problem and related problems (two articles with introductory material here and here, description to be added soon)
• The model-checking problem for various fragments of a probabilistic temporal logic with (probabilistic) knowledge (starting material: first chapters of this book and this article)
• Theory of Electric Boolean Games