Difference between revisions of "Lat21"

From Numerical Transition Systems
Jump to: navigation, search
 
(65 intermediate revisions by the same user not shown)
Line 1: Line 1:
== Logic and Automata Theory ===
+
=== Logic and Automata Theory ===
  
'''Lecturer''': [http://nts.imag.fr/index.php/Radu_Iosif Radu_Iosif]
+
'''Lecturer''': [http://nts.imag.fr/index.php/Radu_Iosif 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.
 
'''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.
Line 8: Line 8:
 
* Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
 
* 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.  
 
* Relationship between Weak Monadic Second-Order Logic and finite automata.  
* Infinite automata on words (Buechi, Mueller) and on trees (Rabin) automata, and their relationship with Monadic Second-Order Logic.  
+
* 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.
 
* Game theory. Proof of Rabin's Complementation Theorem. Application of game theory to logic.
  
Line 17: Line 17:
 
'''Schedule''': Wednesdays between 14h00 and 17h00, from March 3rd to April 21st
 
'''Schedule''': Wednesdays between 14h00 and 17h00, from March 3rd to April 21st
  
'''Location''': virtual meeting (Zoom)
+
'''Location''': https://veri-bbb.imag.fr/b/rad-jbd-yvz-lwk (BigBlueButton virtual meeting). Here are some [[guidelines for online participation]].
  
'''Register''':  
+
'''Course material'''
* send email to [mailto:Radu.Iosif@univ-grenoble-alpes.fr Radu.Iosif@univ-grenoble-alpes.fr] indicating your name and year of Phd/Master program
+
 
* for PhD students, indicate also your host laboratory and name of your PhD advisor
+
* March 3: [http://nts.imag.fr/images/5/5a/Lecture1.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1614775141595 video]
 +
 
 +
* March 10: [http://nts.imag.fr/images/8/83/Lecture2.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1615380421661 video]
 +
 
 +
* March 17: [http://nts.imag.fr/images/c/c0/Lecture3.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1615984701021 video]
 +
 
 +
* March 24: [http://nts.imag.fr/images/e/e5/Lecture4.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1616589047417 video]
 +
 
 +
* March 31: [http://nts.imag.fr/images/d/d8/Lecture5.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1617190616756 video]
 +
 
 +
* April 7: [http://nts.imag.fr/images/7/7e/Lecture6.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1617796097159 video]
 +
 
 +
* April 14: [http://nts.imag.fr/images/b/bb/Lecture7.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1618400923673 video]
 +
 
 +
* May 5: [http://nts.imag.fr/images/c/c0/Lecture8.pdf slides] [https://veri-bbb.imag.fr/playback/presentation/2.0/playback.html?meetingId=5f07ea99b4367d97904b14147bb9178d7fd90fd8-1620213733308 video]
 +
 
 +
'''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]
 +
* 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]
 +
* A. Doxiadis and C. Papadimitriou. Logicomix. ISBN 9780747597209
 +
* Integer arithmetic: [http://www-verimag.imag.fr/~iosif/LAT/recognizable-slide.pdf definability and recognizability]
 +
 
 +
'''Software'''
 +
 
 +
* [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL] [http://nts.imag.fr/images/f/f6/Goal.zip example]
 +
* [https://www.brics.dk/mona/ MONA] [http://nts.imag.fr/images/b/b8/Mona.zip example]
 +
 
 +
'''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
 +
* 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]
 +
* F. Gécseg and M. Steinby. [https://www.researchgate.net/publication/220688732_Tree_Automata Tree Automata]
  
 
[[Lat|Past LAT courses]]
 
[[Lat|Past LAT courses]]

Latest revision as of 10:18, 31 March 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, 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

Software

Bibliography

Past LAT courses