Difference between revisions of "Lat24"

From Numerical Transition Systems
Jump to: navigation, search
Line 21: Line 21:
 
* Mar 20, 2024 02:00 PM [https://nts.imag.fr/images/8/83/Lecture2.pdf slides]
 
* Mar 20, 2024 02:00 PM [https://nts.imag.fr/images/8/83/Lecture2.pdf slides]
 
* Mar 27, 2024 02:00 PM [https://nts.imag.fr/images/c/c0/Lecture3.pdf slides]
 
* 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
 
* Apr 17, 2024 02:00 PM (no class due to easter holiday)
 
* Apr 17, 2024 02:00 PM (no class due to easter holiday)
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]
 
+
* 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]
  
 
'''Bibliography'''
 
'''Bibliography'''

Revision as of 10:54, 4 April 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
  • Apr 17, 2024 02:00 PM (no class due to easter holiday)
  • Apr 24, 2024 02:00 PM
  • 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
  • May 22, 2024 02:00 PM

Additional material

Bibliography

Software