Difference between revisions of "Lat18"
From Numerical Transition Systems
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| (27 intermediate revisions by the same user not shown) | |||
| Line 15: | Line 15: | ||
'''Level''': PhD and Master 2 | '''Level''': PhD and Master 2 | ||
| − | '''Schedule''': | + | '''Schedule''': Mondays between 10h00 and 13h00 |
| − | * Oct | + | * Oct 08: [http://www-verimag.imag.fr/~iosif/LAT/w1_mon.pdf Introduction, First and Second Order Logics] |
| − | * Oct | + | * Oct 15: [http://www-verimag.imag.fr/~iosif/LAT/w1_tue.pdf Automata on Finite Words] |
| − | * Oct | + | * Oct 22: [http://www-verimag.imag.fr/~iosif/LAT/w1_thu.pdf Automata on Infinite Words] |
| − | * Oct | + | * Oct 29: [http://www-verimag.imag.fr/~iosif/LAT/w1_fri.pdf McNaughton's Theorem], [http://www-verimag.imag.fr/~iosif/LAT/mc1.pdf Model Checking 1], [http://www-verimag.imag.fr/~iosif/LAT/mc2.pdf Model Checking 2] |
| − | * Nov | + | * Nov 05: [http://www-verimag.imag.fr/~iosif/LAT/w2_mon.pdf Automata on Finite Trees] |
| − | * Nov | + | * Nov 12: [http://www-verimag.imag.fr/~iosif/LAT/w2_tue.pdf Automata on Infinite Trees] |
| − | * | + | * Dec 3: [http://nts.imag.fr/images/c/c3/GameTheoryMotivation.pdf Game Theory Motivation], [http://nts.imag.fr/images/5/55/GameTheoryTerminology.pdf Terminology], [http://nts.imag.fr/images/3/3b/ReachabilityBuchiGames.pdf Reachability and Buchi games] |
| − | * Dec | + | * Dec 10: [http://nts.imag.fr/images/3/36/StaigerWagnerWeakParityGames.pdf Staiger-Wagner and Weak Parity Games] [http://nts.imag.fr/images/1/1d/ParityGames.pdf Parity games] [http://nts.imag.fr/images/8/89/GamesTreeAutomata.pdf Games and Tree Automata] |
| − | '''Location''': [https://batiment.imag.fr/ IMAG building], Room: | + | '''Resources''': |
| + | |||
| + | * [http://wcms.inf.ed.ac.uk/lfcs/Automata_On_Infinite_Trees_Slide.pdf Automata on Infinite Trees] lecture by Wolfgang Thomas | ||
| + | * [http://nts.imag.fr/images/2/24/Mcnaughton.pdf Textbook proof of McNaughton's Theorem] | ||
| + | * [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL] - Graphical Tool for Omega-Automata and Logics | ||
| + | * [http://nts.imag.fr/images/6/67/Games.zip Game Examples for GOAL] | ||
| + | * M. Vardi and P. Wolper. [https://www.sciencedirect.com/science/article/pii/S0890540184710923 Reasoning about Infinite Computations] | ||
| + | * M. Vardi. [http://www.cs.rice.edu/~vardi/papers/icla09.pdf/ From Philosophical to Industrial Logics] [http://www-verimag.imag.fr/~iosif/LAT/slides.pdf slides] | ||
| + | * [http://www-verimag.imag.fr/~iosif/jcat Java Concurrency Analysis Tool] | ||
| + | |||
| + | '''Location''': [https://batiment.imag.fr/ IMAG building], Room: 206 | ||
'''Register''': | '''Register''': | ||
Latest revision as of 12:42, 9 December 2018
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. The works of A. Pnueli, E. Clarke, E.A Emerson and J. Sifakis on algorithmic verification of systems using the Model Checking has been awarded the 1996 and 2007 Turing awards. The basis of this work is the relation of logic with automata theory, which was introduced by the seminal works of Buechi (1960) and Rabin (1969). This course is intended 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, Mueller) 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
Level: PhD and Master 2
Schedule: Mondays between 10h00 and 13h00
- Oct 08: Introduction, First and Second Order Logics
- Oct 15: Automata on Finite Words
- Oct 22: Automata on Infinite Words
- Oct 29: McNaughton's Theorem, Model Checking 1, Model Checking 2
- Nov 05: Automata on Finite Trees
- Nov 12: Automata on Infinite Trees
- Dec 3: Game Theory Motivation, Terminology, Reachability and Buchi games
- Dec 10: Staiger-Wagner and Weak Parity Games Parity games Games and Tree Automata
Resources:
- Automata on Infinite Trees lecture by Wolfgang Thomas
- Textbook proof of McNaughton's Theorem
- GOAL - Graphical Tool for Omega-Automata and Logics
- Game Examples for GOAL
- M. Vardi and P. Wolper. Reasoning about Infinite Computations
- M. Vardi. From Philosophical to Industrial Logics slides
- Java Concurrency Analysis Tool
Location: IMAG building, Room: 206
Register:
- send email to 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
