Lat

From Numerical Transition Systems
Revision as of 11:04, 13 February 2013 by Radu iosif (Talk | contribs)

Jump to: navigation, search

Logic and Automata Theory

Lecturer: 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:

Bibliography

    • 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

[: vérification et certification du logiciel]

    • Slides**
    - First part: Mc1.pdf
    - Second part: Mc2.pdf
    - Related software: http://www-verimag.imag.fr/~iosif/jcat
Ecole Doctorale Grenoble

[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, [[3]], [[4]], [and Buchi Games]
 - //Tuesday//, 30/11/2010, [Games], [between Games and Tree Automata]
SNSB Bucharest

[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)
EPFL

A course in the [Doctoral Program in Computer and Communication Sciences] 

 * [Course Book Page]
 * the course carries 4 credits
    • Schedule**: (lectures and exercises): Fridays 13:15-16:00

First lecture: 18.9.2009\\ Last lecture: 18.12.2009

    • Location**: [355]
    • Preliminary Outline:**
 - 18.09.2009 Introduction
 - 25.09.2009 First Order and Monadic Second Order LogicsTemplate:Slide1.pdf (Radu Iosif)
 - 02.10.2009 Automata on finite wordsTemplate:Slide2.pdf (Radu Iosif)
 - 09.10.2009 Automata on infinite wordsTemplate:Slide3.pdf (Radu Iosif)
 - 16.10.2009 Linear Temporal LogicTemplate:Ltl-slide.pdf (Radu Iosif)
 - 23.10.2009 Automata on finite treesTemplate:Slide4.pdf (Radu Iosif)
 - 30.10.2009 Automata on infinite treesTemplate:Slide5.pdf (Radu Iosif)
 - 06.11.2009 Games: Terminology, Reachability, Safety, and Buchi games Template:Slide6.pdf (Barbara Jobstmann)
 - 13.11.2009 MC and Repair Example Template:Slide7.pdf, Obligation and Weak-Parity games Template:Slide8.pdf (Barbara Jobstmann)
 - 20.11.2009 Parity games Template:Slide9.pdf (Barbara Jobstmann)
 - 27.11.2009 Muller Games, Relation between games and tree automata Template:Slide10.pdf (Barbara Jobstmann)
 - 04.12.2009 Integer Arithmetic, Presburger Arithmetic and Semilinear Sets Template:Presburger-slide.pdf (Radu Iosif)
 - 11.12.2009 Definability and Recognizability of integer sets Template:Recognizable-slide.pdf (Radu Iosif)
 - 18.12.2009 End-of-Term In-Class Quiz
    • Homework**

Please find the homework here.

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