Difference between revisions of "Lat"

Revision as of 17:57, 16 January 2021

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