Difference between revisions of "Lat"
From Numerical Transition Systems
Radu iosif (Talk | contribs) (→Logic and Automata Theory) |
Radu iosif (Talk | contribs) (→Logic and Automata Theory) |
||
| Line 24: | Line 24: | ||
* [http://wcms.inf.ed.ac.uk/lfcs/Automata_On_Infinite_Trees_Slide.pdf Automata on Infinite Trees] lecture by Wolfgang Thomas | * [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://nts.imag.fr/images/2/24/Mcnaughton.pdf Textbook proof of McNaughton's Theorem] | ||
| − | |||
| − | |||
* M. Vardi and P. Wolper. [https://www.sciencedirect.com/science/article/pii/S0890540184710923 Reasoning about Infinite Computations] | * 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] | * 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] | ||
| Line 36: | Line 34: | ||
* GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/ | * GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/ | ||
* [http://www-verimag.imag.fr/~iosif/jcat Java Concurrency Analysis Tool] | * [http://www-verimag.imag.fr/~iosif/jcat Java Concurrency Analysis Tool] | ||
| + | * [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] | ||
===== ENS Lyon Course on Automata-Theoretic Model Checking ===== | ===== ENS Lyon Course on Automata-Theoretic Model Checking ===== | ||
Revision as of 17:56, 16 January 2021
Contents
Logic and Automata Theory
Similar or related lectures:
- A. Pnueli and M. Vardi. Automata-Theoretic Approach to Automated Verification
- V. Kuncak. Software Analysis and Verification
- D. Nickovic. Aperiodic Languages
Bibliography
- M. Vardi. From Philosophical to Industrial Logics slides
- W. Thomas. Handbook of Theoretical Computer Science, Volume B, Chapter 4. Automata on Infinite Objects
- 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
- Tree Automata Techniques and Applications Collective Online Book
- M. Vardi. The Buchi Complementation Saga
- S. Schewe. Büchi complementation made tight. STACS 2009
- A genealogy of LTL to Buechi automata translations [1]
- A genealogy of Buechi emptiness checking algorithms [2]
- V. Bruyere, G. Hansel, C. Michaux and R. Villemairez. Logic and p-Recognizable Sets of Integers
- M. Jurdzinski, J. Voege. A Discrete Stratety Improvement Algorithm for Solving Parity Games. pdf
- U. Zwick and M. Paterson. The Complexity of Mean Payoff Games
- Note about Karp's minimal mean-cycle algorithm. ps
Other Resources
- Automata on Infinite Trees lecture by Wolfgang Thomas
- Textbook proof of McNaughton's Theorem
- M. Vardi and P. Wolper. Reasoning about Infinite Computations
- M. Vardi. From Philosophical to Industrial Logics slides
Software
- The Mona Project : http://www.brics.dk/mona/
- The Goal Project : http://goal.im.ntu.edu.tw/wiki/doku.php
- LTL2BA: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
- GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/
- Java Concurrency Analysis Tool
- GOAL - Graphical Tool for Omega-Automata and Logics
- Game Examples for GOAL
ENS Lyon Course on Automata-Theoretic Model Checking
ER01 : vérification et certification du logiciel
- First part: mc1.pdf
- Second part: mc2.pdf
- Related software: http://www-verimag.imag.fr/~iosif/jcat
Ecole Doctorale Grenoble
Ecole Doctorale Mathématiques, Sciences et Technologies de l'Information, Informatique
Slides for lectures on game theory (23/11/2010 and 30/11/2010)
- //Tuesday//, 23/11/2010, Motivation, Terminology, Safety and Buchi Games
- //Tuesday//, 30/11/2010, Parity Games, Relationship between Games and Tree Automata
SNSB Bucharest
Scoala Normala Superioara Bucharest (SNSB)
Outline of the first week (19/04/2010 - 24/04/2010) :
- //Monday.// Introduction, First and Second Order Logics (4h, Radu Iosif)
- //Tuesday.// Automata on Finite Words. Definitions of Recognizability (4h, Radu Iosif)
- //Wednesday.// Regular, Star Free and Aperiodic Languages (4h, Radu Iosif)
- //Thursday.// Automata on Infinite Words (4h, Radu Iosif)
- //Friday.// The McNaughton, Buechi and Ramsey Theorems (4h, Radu Iosif)
- //Saturday.// Linear Temporal Logic (4h, Radu Iosif)
Outline of the second week (24/05/2010 - 29/05/2010) :
- //Monday.// Automata on Finite Trees (4h, Radu Iosif)
- //Tuesday.// Automata on Infinite Trees (4h, Radu Iosif)
- //Wednesday.// Motivation, Terminology, Reachability and Buchi games (4h, Barbara Jobstmann)
- //Thursday.// Obligation and weak-parity games, Parity games (4h, Barbara Jobstmann)
- //Friday.// Games and tree automata, Quantitative Verification and Synthesis, Mean-payoff games (4h, Barbara Jobstmann)
- //Saturday.// Integer Arithmetic, Presburger Arithmetic and Semilinear Sets. Definability and Recognizability (4h, Radu Iosif)
ED MSTII Grenoble 2018
- 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
