Difference between revisions of "Lat24"
From Numerical Transition Systems
Radu iosif (Talk | contribs) (Created page with "=== Logic and Automata Theory === '''Lecturer''': [http://nts.imag.fr/index.php/Radu_Iosif Radu Iosif] '''Contents''': Formal language theory is the study of representations...") |
Radu iosif (Talk | contribs) |
||
| (27 intermediate revisions by the same user not shown) | |||
| Line 11: | Line 11: | ||
* Game theory. Proof of Rabin's Complementation Theorem. Application of game theory to 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) | + | '''Prerequisites''': basic notions of boolean logic and discrete mathematics (sets, relations, orders, functions); see [https://drive.google.com/file/d/1JnKNGHq_J8IM4U2m1FV2ci6G7OtKJzOn/view?usp=sharing preliminaries] for an introduction to the basic notions required by this course |
'''Level''': PhD and Master 1-2 | '''Level''': PhD and Master 1-2 | ||
| Line 17: | Line 17: | ||
'''Schedule''': Wednesdays between 14h00 and 17h00 (Paris time, GMT+1), from March 6nd to May 15th | '''Schedule''': Wednesdays between 14h00 and 17h00 (Paris time, GMT+1), from March 6nd to May 15th | ||
| − | * Mar 6, 2024 02:00 PM | + | * Mar 6, 2024 02:00 PM [https://nts.imag.fr/images/5/5a/Lecture1.pdf slides] |
* Mar 13, 2024 02:00 PM (no class due to out-of-office leave) | * Mar 13, 2024 02:00 PM (no class due to out-of-office leave) | ||
| − | * Mar 20, 2024 02:00 PM | + | * Mar 20, 2024 02:00 PM [https://nts.imag.fr/images/8/83/Lecture2.pdf slides] |
| − | * Mar 27, 2024 02:00 PM | + | * Mar 27, 2024 02:00 PM [https://nts.imag.fr/images/c/c0/Lecture3.pdf slides] |
| − | * Apr 3, 2024 02:00 PM | + | * Apr 3, 2024 02:00 PM [https://nts.imag.fr/images/e/e5/Lecture4.pdf slides] |
| − | * Apr 10, 2024 02:00 PM | + | * Apr 10, 2024 02:00 PM [https://nts.imag.fr/images/d/d8/Lecture5.pdf slides] |
| − | * Apr 17, 2024 02:00 PM | + | * Apr 17, 2024 02:00 PM [https://nts.imag.fr/images/7/7e/Lecture6.pdf slides] |
| − | * Apr 24, 2024 02:00 PM | + | * 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 1, 2024 02:00 PM (no class due to national holiday) | ||
| − | * May 8, 2024 02:00 PM | + | * May 8, 2024 02:00 PM (no class due to national holiday) |
| − | * May 15, 2024 02:00 PM | + | * May 15, 2024 02:00 PM [https://nts.imag.fr/images/b/bb/Lecture7.pdf slides] |
| + | * May 22, 2024 02:00 PM [https://nts.imag.fr/images/c/c0/Lecture8.pdf slides] | ||
'''Additional material''' | '''Additional material''' | ||
| + | |||
| + | * Equivalence of first-order and star-free languages: [http://www.lsv.fr/Publis/PAPERS/PDF/DG-WT08.pdf First-order definable languages] by Volker Diekert and Paul Gastin, pp 1--10 | ||
| + | * Equivalence of star-free and aperiodic languages aka [https://en.wikipedia.org/wiki/Marcel-Paul_Sch%C3%BCtzenberger Schutzenberger's] theorem: [http://nts.imag.fr/images/2/25/Schutzenberger.pdf slides] | ||
| + | * Textbook proof of [http://nts.imag.fr/images/2/24/Mcnaughton.pdf McNaughton Theorem] | ||
| + | * Proof of Buechi Complementation Theorem using [http://nts.imag.fr/images/b/b0/Ramseyan.pdf Ramseyan factorizations] | ||
| + | * W. Thomas. [https://old.automata.rwth-aachen.de/download/papers/thomas/thomas88.pdf Automata on Infinite Objects] | ||
| + | * W. Thomas. [https://www.youtube.com/watch?v=JqLX4LzFBn4 Finite Automata and the Infinite] 2014 Milner Lecture University of Edinburgh's Informatics Forum | ||
| + | * R. Mazala. [https://nts.imag.fr/images/d/d0/InfiniteGames.pdf Infinite Games] | ||
| + | * R. Kuesters. [https://nts.imag.fr/images/d/d1/MemorylessDeterminacyParityGames.pdf Memoryless Determinacy of Parity Games] | ||
| + | * F. Niessner. [https://nts.imag.fr/images/d/dc/NondeterministicTreeAutomata.pdf Nondeterministic Tree Automata] | ||
'''Bibliography''' | '''Bibliography''' | ||
* B. Khoussainov and A. Nerode. [https://link.springer.com/book/10.1007/978-1-4612-0171-7 Automata Theory and its Applications]. | * B. Khoussainov and A. Nerode. [https://link.springer.com/book/10.1007/978-1-4612-0171-7 Automata Theory and its Applications]. | ||
| + | * H. Comon, M. Dauchet, R. Gilleron, C. Loeding, F. Jacquemard, D. Lugiez, S. Tison and M. Tommasi. [http://tata.gforge.inria.fr/ Tree Automata: Theory and Applications] | ||
| + | * E. Graedel and W. Thomas. [https://link.springer.com/book/10.1007/3-540-36387-4 Automata Logics, and Infinite Games] | ||
'''Software''' | '''Software''' | ||
| + | |||
| + | * [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL] [http://nts.imag.fr/images/f/f6/Goal.zip examples] | ||
| + | * [https://www.brics.dk/mona/ MONA] [http://nts.imag.fr/images/b/b8/Mona.zip examples] | ||
Latest revision as of 10:41, 22 May 2024
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
