Difference between revisions of "Lat"
From Numerical Transition Systems
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
(20 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
=== Logic and Automata Theory === | === Logic and Automata Theory === | ||
− | ''' | + | '''Similar or related lectures''': |
+ | * A. Pnueli and M. Vardi. [http://www.cs.rice.edu/~vardi/av.html Automata-Theoretic Approach to Automated Verification] | ||
+ | * V. Kuncak. [http://lara.epfl.ch/web2010/sav11:top Software Analysis and Verification] | ||
+ | * D. Nickovic. [http://www-verimag.imag.fr/~iosif/LAT/star-free-pres.pdf Aperiodic Languages] | ||
− | ''' | + | '''Bibliography''' |
+ | * 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] | ||
+ | * 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 | ||
+ | * [http://tata.gforge.inria.fr/ Tree Automata Techniques and Applications] Collective Online Book | ||
+ | * M. Vardi. [http://www-verimag.imag.fr/~iosif/LAT/stacs07.pdf The Buchi Complementation Saga] | ||
+ | * S. Schewe. Büchi complementation made tight. [http://arxiv.org/PS_cache/arxiv/pdf/0902/0902.2152v1.pdf STACS 2009] | ||
+ | * A genealogy of LTL to Buechi automata translations [http://spot.lip6.fr/wiki/LtlTranslationAlgorithms] | ||
+ | * A genealogy of Buechi emptiness checking algorithms [http://spot.lip6.fr/wiki/EmptinessCheckAlgorithms] | ||
+ | * V. Bruyere, G. Hansel, C. Michaux and R. Villemairez. [http://www-verimag.imag.fr/~iosif/LAT/bru.pdf Logic and p-Recognizable Sets of Integers] | ||
+ | * M. Jurdzinski, J. Voege. A Discrete Stratety Improvement Algorithm for Solving Parity Games. [http://www.brics.dk/RS/00/48/BRICS-RS-00-48.pdf pdf] | ||
+ | * U. Zwick and M. Paterson. [http://www-verimag.imag.fr/~iosif/LAT/mean-payoff.pdf The Complexity of Mean Payoff Games] | ||
+ | * Note about Karp's minimal mean-cycle algorithm. [http://webcourse.cs.technion.ac.il/236359/Spring2010/ho/WCFiles/MMC.ps ps] | ||
− | ''' | + | '''Other 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] | |
− | * | + | * 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] |
− | ''' | + | '''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/ | |
− | + | * [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 ===== | ||
− | + | [http://www.ens-lyon.fr/DI/?p=2320 ER01 : vérification et certification du logiciel] | |
− | * | + | * First part: [http://www-verimag.imag.fr/~iosif/LAT/mc1.pdf mc1.pdf] |
− | + | * Second part: [http://www-verimag.imag.fr/~iosif/LAT/mc2.pdf mc2.pdf] | |
− | + | * Related software: http://www-verimag.imag.fr/~iosif/jcat | |
− | + | ||
===== Ecole Doctorale Grenoble ===== | ===== Ecole Doctorale Grenoble ===== | ||
− | + | [http://edmstii.ujf-grenoble.fr/ 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, [http://www-verimag.imag.fr/~jobstman/teaching/LAT2011/1_motivation.pdf Motivation], [http://www-verimag.imag.fr/~jobstman/teaching/LAT2011/2_terminology.pdf Terminology], [http://www-verimag.imag.fr/~jobstman/teaching/LAT2011/3_safety_buchi.pdf Safety and Buchi Games] | |
− | + | * //Tuesday//, 30/11/2010, [http://www-verimag.imag.fr/~jobstman/teaching/LAT2011/4_parity.pdf Parity Games], [http://www-verimag.imag.fr/~jobstman/teaching/LAT2011/5_games_and_trees.pdf Relationship between Games and Tree Automata] | |
===== SNSB Bucharest ===== | ===== SNSB Bucharest ===== | ||
− | + | [http://www.imar.ro/~purice/SNS/homepage/index_eng.php3 Scoala Normala Superioara Bucharest (SNSB)] | |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | |||
− | First | + | '''Outline of the first week''' (19/04/2010 - 24/04/2010) : |
− | + | * //Monday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_mon.pdf Introduction, First and Second Order Logics] (4h, Radu Iosif) | |
+ | * //Tuesday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_tue.pdf Automata on Finite Words. Definitions of Recognizability] (4h, Radu Iosif) | ||
+ | * //Wednesday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_wed.pdf Regular, Star Free and Aperiodic Languages] (4h, Radu Iosif) | ||
+ | * //Thursday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_thu.pdf Automata on Infinite Words] (4h, Radu Iosif) | ||
+ | * //Friday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_fri.pdf The McNaughton, Buechi and Ramsey Theorems] (4h, Radu Iosif) | ||
+ | * //Saturday.// [http://www-verimag.imag.fr/~iosif/LAT/w1_sat.pdf Linear Temporal Logic] (4h, Radu Iosif) | ||
− | ** | + | '''Outline of the second week''' (24/05/2010 - 29/05/2010) : |
+ | * //Monday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_mon.pdf Automata on Finite Trees] (4h, Radu Iosif) | ||
+ | * //Tuesday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_tue.pdf Automata on Infinite Trees] (4h, Radu Iosif) | ||
+ | * //Wednesday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_wed_1.pdf Motivation], [http://www-verimag.imag.fr/~iosif/LAT/w2_wed_2.pdf Terminology], [http://www-verimag.imag.fr/~iosif/LAT/w2_wed_3.pdf Reachability and Buchi games] (4h, Barbara Jobstmann) | ||
+ | * //Thursday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_thu_1.pdf Obligation and weak-parity games], [http://www-verimag.imag.fr/~iosif/LAT/w2_thu_2.pdf Parity games] (4h, Barbara Jobstmann) | ||
+ | * //Friday.// [http://www-verimag.imag.fr/~iosif/LAT/w2_fri_1.pdf Games and tree automata], [http://www-verimag.imag.fr/~iosif/LAT/quantitative-synthesis-p4.pdf Quantitative Verification and Synthesis], [http://www-verimag.imag.fr/~iosif/LAT/w2_fri_3.pdf Mean-payoff games] (4h, Barbara Jobstmann) | ||
+ | * //Saturday.// [http://www-verimag.imag.fr/~iosif/LAT/presburger-slide.pdf Integer Arithmetic, Presburger Arithmetic and Semilinear Sets]. [http://www-verimag.imag.fr/~iosif/LAT/recognizable-slide.pdf Definability and Recognizability] (4h, Radu Iosif) | ||
− | + | ===== ED MSTII Grenoble 2018 ===== | |
− | + | * Oct 08: [http://www-verimag.imag.fr/~iosif/LAT/w1_mon.pdf Introduction, First and Second Order Logics] | |
− | + | * Oct 15: [http://www-verimag.imag.fr/~iosif/LAT/w1_tue.pdf Automata on Finite Words] | |
− | + | * Oct 22: [http://www-verimag.imag.fr/~iosif/LAT/w1_thu.pdf Automata on Infinite Words] | |
− | + | * 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 05: [http://www-verimag.imag.fr/~iosif/LAT/w2_mon.pdf Automata on Finite Trees] | |
− | + | * 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 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] | |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ===== ED MSTII Grenoble 2021 ===== | |
− | + | http://nts.imag.fr/index.php/Lat21 |
Latest revision as of 17:40, 25 February 2022
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