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:

  1. Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
  2. 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.
  3. 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.
  4. Logical theory of integer arithmetic. Decidability results using both quantifier elimination and automata theory. Cobham's base dependence theorem.

Similar or related lectures:

  1. D. Nickovic. Aperiodic Languages star-free-pres.pdf

Bibliography

  1. W. Thomas. Handbook of Theoretical Computer Science, Volume B, Chapter 4. Automata on Infinite Objects
  2. B. Khoussainov and A. Nerode. Automata Theory and its Applications. ISBN 0-8176-4207-2
  3. D. Perrin and J.E. Pin. Infinite Words. ISBN 0-12-532111-2
  4. M. Vardi. The Buchi Complementation Saga. stacs07.pdf
  5. S. Schewe. Büchi complementation made tight. STACS 2009
  6. A genealogy of LTL to Buechi automata translations http://spot.lip6.fr/wiki/LtlTranslationAlgorithms
  7. A genealogy of Buechi emptiness checking algorithms http://spot.lip6.fr/wiki/EmptinessCheckAlgorithms
  8. V. Bruyere, G. Hansel, C. Michaux and R. Villemairez. Logic and p-Recognizable Sets of Integers. bru.pdf
  9. M. Jurdzinski, J. Voege. A Discrete Stratety Improvement Algorithm for Solving Parity Games. pdf
  10. U. Zwick and M. Paterson. The Complexity of Mean Payoff Games. mean-payoff.pdf
  11. Note about Karp's minimal mean-cycle algorithm. ps

Software

  1. The Mona Project : http://www.brics.dk/mona/
  2. GAVS+: An Open Platform for the Research of Algorithmic Game Solving: http://www6.in.tum.de/~chengch/gavs/

Scoala Normala Superioara Bucharest (SNSB)

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

  1. Monday. Introduction, First and Second Order Logics w1_mon.pdf (4h, Radu Iosif)
  2. Tuesday. Automata on Finite Words. Definitions of Recognizability w1_tue.pdf (4h, Radu Iosif)
  3. Wednesday. Regular, Star Free and Aperiodic Languages w1_wed.pdf (4h, Radu Iosif)
  4. Thursday. Automata on Infinite Words w1_thu.pdf (4h, Radu Iosif)
  5. Friday. The McNaughton, Buechi and Ramsey Theorems w1_fri.pdf (4h, Radu Iosif)
  6. Saturday. Linear Temporal Logic w1_sat.pdf (4h, Radu Iosif)

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

  1. Monday. Automata on Finite Trees w2_mon.pdf (4h, Radu Iosif)
  2. Tuesday. Automata on Infinite Trees w2_tue.pdf (4h, Radu Iosif)
  3. Wednesday. Motivation w2_wed_1.pdf, Terminology w2_wed_2.pdf, Reachability and Buchi games w2_wed_3.pdf (4h, Barbara Jobstmann)
  4. Thursday. Obligation and weak-parity games w2_thu_1.pdf, Parity games w2_thu_2.pdf (4h, Barbara Jobstmann)
  5. 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)
  6. Saturday. Integer Arithmetic, Presburger Arithmetic and Semilinear Sets presburger-slide.pdf. Definability and Recognizability recognizable-slide.pdf (4h, Radu Iosif)

A course in the EPFL Doctoral Program in Computer and Communication Sciences

Organized by: Viktor Kuncak

Schedule: (lectures and exercises): Fridays 13:15-16:00

First lecture: 18.9.2009
Last lecture: 18.12.2009

Location: BC 355

Preliminary Outline:

  1. 18.09.2009 Introduction
  2. 25.09.2009 First Order and Monadic Second Order Logicsslide1.pdf (Radu Iosif)
  3. 02.10.2009 Automata on finite wordsslide2.pdf (Radu Iosif)
  4. 09.10.2009 Automata on infinite wordsslide3.pdf (Radu Iosif)
  5. 16.10.2009 Linear Temporal Logicltl-slide.pdf (Radu Iosif)
  6. 23.10.2009 Automata on finite treesslide4.pdf (Radu Iosif)
  7. 30.10.2009 Automata on infinite treesslide5.pdf (Radu Iosif)
  8. 06.11.2009 Games: Terminology, Reachability, Safety, and Buchi games slide6.pdf (Barbara Jobstmann)
  9. 13.11.2009 MC and Repair Example slide7.pdf, Obligation and Weak-Parity games slide8.pdf (Barbara Jobstmann)
  10. 20.11.2009 Parity games slide9.pdf (Barbara Jobstmann)
  11. 27.11.2009 Muller Games, Relation between games and tree automata slide10.pdf (Barbara Jobstmann)
  12. 04.12.2009 Integer Arithmetic, Presburger Arithmetic and Semilinear Sets presburger-slide.pdf (Radu Iosif)
  13. 11.12.2009 Definability and Recognizability of integer sets recognizable-slide.pdf (Radu Iosif)
  14. 18.12.2009 End-of-Term In-Class Quiz

Homework

Please find the homework here.