Lat24
Logic and Automata Theory
Lecturer: Radu Iosif
Contents: Formal language theory is the study of representations of infinite sets of (finite or infinite) objects (words, trees, graphs, etc.). These representations can be descriptive (logical) or constructive (based on algebras). The aim of the course is to introduce the student to the basic notions of logics and automata used to describe infinite sets. We shall emphasize the various connections that exist between logics and automata theory, thus providing robust definitions of the classes of objects (words, trees) that can be equivalently represented in both logical and automata-theoretic ways. These representations are the basis of formal methods, such as verification and synthesis, that aim to help engineers design correct hardware and software systems.
Syllabus:
- Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
- Relationship between Weak Monadic Second-Order Logic and finite automata.
- Infinite automata on words (Buechi, Muller) and on trees (Rabin) automata, and their relationship with Monadic Second-Order Logic.
- Game theory. Proof of Rabin's Complementation Theorem. Application of game theory to logic.
Prerequisites: basic notions of boolean logic and discrete mathematics (sets, relations, orders, functions); see preliminaries for an introduction to the basic notions required by this course
Level: PhD and Master 1-2
Schedule: Wednesdays between 14h00 and 17h00 (Paris time, GMT+1), from March 6nd to May 15th
- Mar 6, 2024 02:00 PM slides
- Mar 13, 2024 02:00 PM (no class due to out-of-office leave)
- Mar 20, 2024 02:00 PM slides
- Mar 27, 2024 02:00 PM slides
- Apr 3, 2024 02:00 PM slides
- Apr 10, 2024 02:00 PM slides
- Apr 17, 2024 02:00 PM slides
- Apr 24, 2024 02:00 PM (no class due to easter holiday)
- May 1, 2024 02:00 PM (no class due to national holiday)
- May 8, 2024 02:00 PM (no class due to national holiday)
- May 15, 2024 02:00 PM slides
- May 22, 2024 02:00 PM slides
Additional material
- Equivalence of first-order and star-free languages: First-order definable languages by Volker Diekert and Paul Gastin, pp 1--10
- Equivalence of star-free and aperiodic languages aka Schutzenberger's theorem: slides
- Textbook proof of McNaughton Theorem
- Proof of Buechi Complementation Theorem using Ramseyan factorizations
- W. Thomas. Automata on Infinite Objects
- W. Thomas. Finite Automata and the Infinite 2014 Milner Lecture University of Edinburgh's Informatics Forum
- R. Mazala. Infinite Games
- R. Kuesters. Memoryless Determinacy of Parity Games
- F. Niessner. [Nondeterministic Tree Automata]
Bibliography
- B. Khoussainov and A. Nerode. Automata Theory and its Applications.
- H. Comon, M. Dauchet, R. Gilleron, C. Loeding, F. Jacquemard, D. Lugiez, S. Tison and M. Tommasi. Tree Automata: Theory and Applications
- E. Graedel and W. Thomas. Automata Logics, and Infinite Games
Software
