Difference between revisions of "Lat22"
From Numerical Transition Systems
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| (13 intermediate revisions by the same user not shown) | |||
| Line 23: | Line 23: | ||
* March 2: [http://nts.imag.fr/images/5/5a/Lecture1.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1646224330352 video] | * March 2: [http://nts.imag.fr/images/5/5a/Lecture1.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1646224330352 video] | ||
* March 9: [http://nts.imag.fr/images/8/83/Lecture2.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1646830018519 video] | * March 9: [http://nts.imag.fr/images/8/83/Lecture2.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1646830018519 video] | ||
| − | * March 16: [http://nts.imag.fr/images/c/c0/Lecture3.pdf slides] [video] | + | * March 16: [http://nts.imag.fr/images/c/c0/Lecture3.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1647434515286 video] |
| − | * March 23: [slides] [video] | + | * March 23: [http://nts.imag.fr/images/e/e5/Lecture4.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1648039390780 video] |
| − | * March 30: [slides] [video] | + | * March 30: [http://nts.imag.fr/images/d/d8/Lecture5.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1648640548213 video] |
| − | * April 6: [slides] [video] | + | * April 6: [http://nts.imag.fr/images/7/7e/Lecture6.pdf slides] [https://drive.google.com/file/d/1Ma9q-yrAV2e95KLWjTouarH5SB9H4Ebv/view?usp=sharing video] |
| − | * April 13: [slides] [video] | + | * April 13: [http://nts.imag.fr/images/b/bb/Lecture7.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1649850305242 video] |
| − | * April | + | * April 27: [http://nts.imag.fr/images/c/c0/Lecture8.pdf slides] [https://bans.imag.fr/playback/presentation/2.3/335520a5341d4c867d650a71727ecd4c752fa4ca-1651059959803 video] |
'''Additional material''' | '''Additional material''' | ||
| Line 34: | Line 34: | ||
* 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 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] | * 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] | ||
| + | * Wolfgang Thomas. [https://www.youtube.com/watch?v=JqLX4LzFBn4 Finite Automata and the Infinite] 2014 Milner Lecture University of Edinburgh's Informatics Forum | ||
| + | * 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] | ||
| + | * M. Vardi. [https://www.cs.rice.edu/~vardi/papers/icla09.pdf From Philosophical to Industrial Logics] [http://www-verimag.imag.fr/~iosif/LAT/slides.pdf slides] | ||
| + | * M. Vardi and P. Wolper. [https://www.sciencedirect.com/science/article/pii/S0890540184710923 Reasoning about Infinite Computations] | ||
| + | * Talks by M. Vardi: [https://www.youtube.com/watch?v=pMAT3B13DXs&list=PLnx6_vLdgGKxLNX5m-SZfdjsmytsUKnDQ&index=2 And Logic Begat Computer Science: When Giants Roamed the Earth], [https://www.youtube.com/watch?v=QBPUQ2TZ9mc&list=PLnx6_vLdgGKxLNX5m-SZfdjsmytsUKnDQ&index=4 The Rise and Fall of Linear Temporal Logic] | ||
| + | * W. Thomas. [https://old.automata.rwth-aachen.de/download/papers/thomas/thomas88.pdf Automata on Infinite Objects] | ||
'''Bibliography''' | '''Bibliography''' | ||
| Line 39: | Line 46: | ||
* 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]. | ||
* S. Eilenberg. [https://www.elsevier.com/books/automata-languages-and-machines/eilenberg/978-0-12-234001-7 Automata, Languages, and Machines]. | * S. Eilenberg. [https://www.elsevier.com/books/automata-languages-and-machines/eilenberg/978-0-12-234001-7 Automata, Languages, and Machines]. | ||
| + | * 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] | ||
'''Software''' | '''Software''' | ||
Latest revision as of 10:36, 28 April 2022
Logic and Automata Theory
Lecturer: Radu Iosif
Objectives: Many major hardware (Intel, IBM) and software (Microsoft) companies are now using the technique of Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. Model checking and verification of computer systems are grounded in the seminal works of A. Pnueli, E. Clarke, E.A Emerson and J. Sifakis, which have been awarded the 1996 and 2007 Turing awards. The basis of these works is the relation of logic with automata theory, which was introduced by Büchi (1960) and Rabin (1969). The goal of this course is to introduce the student to these techniques, focusing on decision methods for classical non-interpreted logics and integer arithmetic theories.
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)
Level: PhD and Master 1-2
Schedule: Wednesdays between 14h00 and 17h00 (Paris time, GMT+1), from March 2nd to April 20th
Location: https://bans.imag.fr/b/rad-dmn-cap-sd6 (BigBlueButton virtual meeting). Here are some guidelines for online participation.
Course material
- March 2: slides video
- March 9: slides video
- March 16: slides video
- March 23: slides video
- March 30: slides video
- April 6: slides video
- April 13: slides video
- April 27: slides video
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
- Wolfgang Thomas. Finite Automata and the Infinite 2014 Milner Lecture University of Edinburgh's Informatics Forum
- Textbook proof of McNaughton Theorem
- Proof of Buechi Complementation Theorem using Ramseyan factorizations
- M. Vardi. From Philosophical to Industrial Logics slides
- M. Vardi and P. Wolper. Reasoning about Infinite Computations
- Talks by M. Vardi: And Logic Begat Computer Science: When Giants Roamed the Earth, The Rise and Fall of Linear Temporal Logic
- W. Thomas. Automata on Infinite Objects
Bibliography
- B. Khoussainov and A. Nerode. Automata Theory and its Applications.
- S. Eilenberg. Automata, Languages, and Machines.
- H. Comon, M. Dauchet, R. Gilleron, C. Loeding, F. Jacquemard, D. Lugiez, S. Tison and M. Tommasi. Tree Automata: Theory and Applications
Software
