Difference between revisions of "Lat21"
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| Line 32: | Line 32: | ||
* 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] | ||
* Textbook proof of [http://nts.imag.fr/images/2/24/Mcnaughton.pdf McNaughton Theorem] | * Textbook proof of [http://nts.imag.fr/images/2/24/Mcnaughton.pdf McNaughton Theorem] | ||
| − | * Proof of Buechi Complementation Theorem using [Ramseyan factorizations] | + | * Proof of Buechi Complementation Theorem using [http://nts.imag.fr/images/b/b0/Ramseyan.pdf Ramseyan factorizations] |
'''Software''' | '''Software''' | ||
Revision as of 16:04, 20 March 2021
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, from March 3rd to April 21st
Location: https://veri-bbb.imag.fr/b/rad-jbd-yvz-lwk (BigBlueButton virtual meeting). Here are some guidelines for online participation.
Course material
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
Software
Bibliography
- B. Khoussainov and A. Nerode. Automata Theory and its Applications. ISBN 0-8176-4207-2
- D. Perrin and J.E. Pin. Infinite Words. ISBN 0-12-532111-2
