Difference between revisions of "Lat"

From Numerical Transition Systems
Jump to: navigation, search
 
(26 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
=== Logic and Automata Theory ===
 
=== Logic and Automata Theory ===
  
−
**Lecturer**: [[http://www-verimag.imag.fr/~iosif/|Radu Iosif]] and [[http://www-verimag.imag.fr/~jobstman/|Barbara Jobstmann]]
+
'''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]
  
−
**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.
+
'''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]
  
−
**Syllabus**:
+
'''Other Resources'''
−
  - Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
+
* [http://wcms.inf.ed.ac.uk/lfcs/Automata_On_Infinite_Trees_Slide.pdf Automata on Infinite Trees] lecture by Wolfgang Thomas
−
  - 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.  
+
* [http://nts.imag.fr/images/2/24/Mcnaughton.pdf Textbook proof of McNaughton's Theorem]
−
  - 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.
+
* M. Vardi and P. Wolper. [https://www.sciencedirect.com/science/article/pii/S0890540184710923 Reasoning about Infinite Computations]
−
  - Logical theory of integer arithmetic. Decidability results using both quantifier elimination and automata theory. Cobham's base dependence theorem.
+
* 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]
  
−
**Similar or related lectures**:
+
'''Software'''
−
      - W. Thomas. [[http://sit.iitkgp.ernet.in/archive/teaching/autometa|Automata and Reactive Systems]]
+
* The Mona Project : http://www.brics.dk/mona/
−
      - A. Pnueli and M. Vardi. [[http://www.cs.rice.edu/~vardi/av.html|Automata-Theoretic Approach to Automated Verification]]
+
* The Goal Project : http://goal.im.ntu.edu.tw/wiki/doku.php
−
      - V. Kuncak. [[http://lara.epfl.ch/web2010/sav11:top| Software Analysis and Verification]]
+
* LTL2BA: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
−
      - D. Nickovic. Aperiodic Languages {{star-free-pres.pdf}}
+
* GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/
−
      - R. Iosif. [[http://www-verimag.imag.fr/~iosif/LogicAutomata07/|Logic and Automata (2007)]].
+
* [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
−
**Bibliography**
+
* [http://nts.imag.fr/images/6/67/Games.zip Game Examples for GOAL]
−
      - M. Vardi. [[http://www.cs.rice.edu/~vardi/papers/icla09.pdf/|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
+
−
      - [[http://tata.gforge.inria.fr/|Tree Automata Techniques and Applications]] Collective Online Book
+
−
      - M. Vardi. The Buchi Complementation Saga. {{:stacs07.pdf|}}
+
−
      - 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. Logic and p-Recognizable Sets of Integers. {{BRU.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. The Complexity of Mean Payoff Games. {{:mean-payoff.pdf|}}
+
−
      - Note about Karp's minimal mean-cycle algorithm. [[http://webcourse.cs.technion.ac.il/236359/Spring2010/ho/WCFiles/MMC.ps|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 =====
 
===== ENS Lyon Course on Automata-Theoretic Model Checking =====
  
−
[[http://www.ens-lyon.fr/DI/?p=2320|ER01 : vérification et certification du logiciel]]
+
[http://www.ens-lyon.fr/DI/?p=2320 ER01 : vérification et certification du logiciel]
  
−
**Slides**
+
* First part: [http://www-verimag.imag.fr/~iosif/LAT/mc1.pdf mc1.pdf]
−
    - First part: {{:mc1.pdf|mc1.pdf}}
+
* Second part: [http://www-verimag.imag.fr/~iosif/LAT/mc2.pdf mc2.pdf]
−
    - Second part: {{:mc2.pdf|mc2.pdf}}
+
* Related software: http://www-verimag.imag.fr/~iosif/jcat
−
    - 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]]
+
[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)
+
'''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//, 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]]
+
* //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)]]
+
[http://www.imar.ro/~purice/SNS/homepage/index_eng.php3 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 {{presburger-slide.pdf}}. Definability and Recognizability {{recognizable-slide.pdf}} (4h, Radu Iosif)
+
−
 
+
−
===== EPFL =====
+
−
 
+
−
A course in the [[http://phd.epfl.ch/edic|EPFL Doctoral Program in Computer and Communication Sciences]]
+
−
  * [[http://infowww.epfl.ch/imoniteur_ISAP/!itffichecours.htm?ww_i_matiere=280335500&ww_x_anneeAcad=2009-2010&ww_i_section=2139068&ww_c_langue=en|Official Course Book Page]]
+
−
  * the course carries 4 credits
+
−
 
+
−
**Organized by:** [[http://lara.epfl.ch/~kuncak|Viktor Kuncak]]
+
  
−
**Schedule**: (lectures and exercises): Fridays 13:15-16:00
 
  
−
First lecture: 18.9.2009\\
+
'''Outline of the first week''' (19/04/2010 - 24/04/2010) :
−
Last lecture: 18.12.2009
+
* //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)
  
−
**Location**: [[http://map.epfl.ch/?room=BC355|BC 355]]
+
'''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)
  
−
**Preliminary Outline:**
+
===== ED MSTII Grenoble 2018 =====
  
−
  - 18.09.2009 Introduction
+
* Oct 08: [http://www-verimag.imag.fr/~iosif/LAT/w1_mon.pdf Introduction, First and Second Order Logics]
−
  - 25.09.2009 First Order and Monadic Second Order Logics{{slide1.pdf}} (Radu Iosif)
+
* Oct 15: [http://www-verimag.imag.fr/~iosif/LAT/w1_tue.pdf Automata on Finite Words]
−
  - 02.10.2009 Automata on finite words{{slide2.pdf}} (Radu Iosif)
+
* Oct 22: [http://www-verimag.imag.fr/~iosif/LAT/w1_thu.pdf Automata on Infinite Words]
−
  - 09.10.2009 Automata on infinite words{{slide3.pdf}} (Radu Iosif)
+
* 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]
−
  - 16.10.2009 Linear Temporal Logic{{ltl-slide.pdf}} (Radu Iosif)
+
* Nov 05: [http://www-verimag.imag.fr/~iosif/LAT/w2_mon.pdf Automata on Finite Trees]
−
  - 23.10.2009 Automata on finite trees{{slide4.pdf}} (Radu Iosif)
+
* Nov 12: [http://www-verimag.imag.fr/~iosif/LAT/w2_tue.pdf Automata on Infinite Trees]
−
  - 30.10.2009 Automata on infinite trees{{slide5.pdf}} (Radu Iosif)
+
* 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]
−
  - 06.11.2009 Games: Terminology, Reachability, Safety, and Buchi games {{slide6.pdf}} (Barbara Jobstmann)
+
* 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]
−
  - 13.11.2009 MC and Repair Example {{slide7.pdf}}, Obligation and Weak-Parity games {{slide8.pdf}} (Barbara Jobstmann)
+
−
  - 20.11.2009 Parity games {{slide9.pdf}} (Barbara Jobstmann)
+
−
  - 27.11.2009 Muller Games, Relation between games and tree automata {{slide10.pdf}} (Barbara Jobstmann)
+
−
  - 04.12.2009 Integer Arithmetic, Presburger Arithmetic and Semilinear Sets {{presburger-slide.pdf}} (Radu Iosif)
+
−
  - 11.12.2009 Definability and Recognizability of integer sets {{recognizable-slide.pdf}} (Radu Iosif)
+
−
  - 18.12.2009 End-of-Term In-Class Quiz
+
  
−
**Homework**
+
===== ED MSTII Grenoble 2021 =====
  
−
Please find the homework [[LAT:homework|here.]]
+
http://nts.imag.fr/index.php/Lat21

Latest revision as of 17:40, 25 February 2022

Logic and Automata Theory

Similar or related lectures:

Bibliography

Other Resources

Software

ENS Lyon Course on Automata-Theoretic Model Checking

ER01 : vérification et certification du logiciel

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)

SNSB Bucharest

Scoala Normala Superioara Bucharest (SNSB)


Outline of the first week (19/04/2010 - 24/04/2010) :

Outline of the second week (24/05/2010 - 29/05/2010) :

ED MSTII Grenoble 2018
ED MSTII Grenoble 2021

http://nts.imag.fr/index.php/Lat21

Retrieved from "http://nts.imag.fr/index.php?title=Lat&oldid=1023"