Difference between revisions of "Lat"

From Numerical Transition Systems
Jump to: navigation, search
(5 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
=== Logic and Automata Theory ===
 
=== Logic and Automata Theory ===
 
'''Lecturers''': [http://www-verimag.imag.fr/~iosif/ Radu Iosif] and [http://www-verimag.imag.fr/~jobstman/ 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''':
 
'''Similar or related lectures''':
Line 30: Line 20:
 
* U. Zwick and M. Paterson. [http://www-verimag.imag.fr/~iosif/LAT/mean-payoff.pdf The Complexity of Mean Payoff Games]
 
* 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]
 +
 +
'''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'''
 
'''Software'''
 
* The Mona Project : http://www.brics.dk/mona/
 
* The Mona Project : http://www.brics.dk/mona/
 
* The Goal Project : http://goal.im.ntu.edu.tw/wiki/doku.php
 
* 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
+
* 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/
 
* 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 =====
Line 73: Line 72:
 
* //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)
 
* //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)
 
* //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]

Revision as of 17:57, 16 January 2021

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