Difference between revisions of "Lat"
From Numerical Transition Systems
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| Line 23: | Line 23: | ||
* D. Perrin and J.E. Pin. Infinite Words. ISBN 0-12-532111-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 | * [http://tata.gforge.inria.fr/ Tree Automata Techniques and Applications] Collective Online Book | ||
| − | * M. Vardi. | + | * 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] | * 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 LTL to Buechi automata translations [http://spot.lip6.fr/wiki/LtlTranslationAlgorithms] | ||
* A genealogy of Buechi emptiness checking algorithms [http://spot.lip6.fr/wiki/EmptinessCheckAlgorithms] | * A genealogy of Buechi emptiness checking algorithms [http://spot.lip6.fr/wiki/EmptinessCheckAlgorithms] | ||
| − | * V. Bruyere, G. Hansel, C. Michaux and R. Villemairez. Logic and p-Recognizable Sets of Integers | + | * 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] | * 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. | + | * 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] | * Note about Karp's minimal mean-cycle algorithm. [http://webcourse.cs.technion.ac.il/236359/Spring2010/ho/WCFiles/MMC.ps ps] | ||
Revision as of 11:24, 13 February 2013
Contents
Logic and Automata Theory
Lecturers: Radu Iosif and Barbara Jobstmann
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 Mu-calculus, a widely used tool for specification and verification of systems.
- Logical theory of integer arithmetic. Decidability results using both quantifier elimination and automata theory. Cobham's base dependence theorem.
Similar or related lectures:
- W. Thomas. Automata and Reactive Systems
- 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.pdf
- 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
Software
- The Mona Project : http://www.brics.dk/mona/
- The Goal Project : http://goal.im.ntu.edu.tw/wiki/doku.php
- The Gastex Package for Latex : http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html
- GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/
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 W1 mon.pdf (4h, Radu Iosif)
- //Tuesday.// Automata on Finite Words. Definitions of Recognizability W1 tue.pdf (4h, Radu Iosif)
- //Wednesday.// Regular, Star Free and Aperiodic Languages W1 wed.pdf (4h, Radu Iosif)
- //Thursday.// Automata on Infinite Words W1 thu.pdf (4h, Radu Iosif)
- //Friday.// The McNaughton, Buechi and Ramsey Theorems W1 fri.pdf (4h, Radu Iosif)
- //Saturday.// Linear Temporal Logic W1 sat.pdf (4h, Radu Iosif)
Outline of the second week (24/05/2010 - 29/05/2010) :
- //Monday.// Automata on Finite Trees W2 mon.pdf (4h, Radu Iosif)
- //Tuesday.// Automata on Infinite Trees W2 tue.pdf (4h, Radu Iosif)
- //Wednesday.// Motivation W2 wed 1.pdf, Terminology W2 wed 2.pdf, Reachability and Buchi games W2 wed 3.pdf (4h, Barbara Jobstmann)
- //Thursday.// Obligation and weak-parity games W2 thu 1.pdf, Parity games W2 thu 2.pdf (4h, Barbara Jobstmann)
- //Friday.// Games and tree automata W2 fri 1.pdf, Quantitative Verification and Synthesis Quantitative-synthesis-p4.pdf, Mean-payoff games W2 fri 3.pdf (4h, Barbara Jobstmann)
- //Saturday.// Integer Arithmetic, Presburger Arithmetic and Semilinear Sets Template:Presburger-slide.pdf. Definability and Recognizability Template:Recognizable-slide.pdf (4h, Radu Iosif)
