Difference between revisions of "Lat"

From Numerical Transition Systems
Jump to: navigation, search
Line 56: Line 56:
 
===== 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) :
+
'''Outline of the first week''' (19/04/2010 - 24/04/2010) :
  - //Monday.// Introduction, First and Second Order Logics {{:w1_mon.pdf|}} (4h, Radu Iosif)
+
* //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)
+
* //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)
+
* //Wednesday.// Regular, Star Free and Aperiodic Languages {{:w1_wed.pdf}} (4h, Radu Iosif)
  - //Thursday.// Automata on Infinite Words {{:w1_thu.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)
+
* //Friday.// The McNaughton, Buechi and Ramsey Theorems {{:w1_fri.pdf}} (4h, Radu Iosif)
  - //Saturday.// Linear Temporal Logic {{:w1_sat.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) :
+
'''Outline of the second week''' (24/05/2010 - 29/05/2010) :
  - //Monday.// Automata on Finite Trees {{:w2_mon.pdf|}} (4h, Radu Iosif)
+
* //Monday.// Automata on Finite Trees {{:w2_mon.pdf}} (4h, Radu Iosif)
  - //Tuesday.// Automata on Infinite Trees {{:w2_tue.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)
+
* //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)
+
* //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)
+
* //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)
+
* //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\\
+
Last lecture:  18.12.2009
+
 
+
**Location**: [[http://map.epfl.ch/?room=BC355|BC 355]]
+
 
+
**Preliminary Outline:**
+
 
+
  - 18.09.2009 Introduction
+
  - 25.09.2009 First Order and Monadic Second Order Logics{{slide1.pdf}} (Radu Iosif)
+
  - 02.10.2009 Automata on finite words{{slide2.pdf}} (Radu Iosif)
+
  - 09.10.2009 Automata on infinite words{{slide3.pdf}} (Radu Iosif)
+
  - 16.10.2009 Linear Temporal Logic{{ltl-slide.pdf}} (Radu Iosif)
+
  - 23.10.2009 Automata on finite trees{{slide4.pdf}} (Radu Iosif)
+
  - 30.10.2009 Automata on infinite trees{{slide5.pdf}} (Radu Iosif)
+
  - 06.11.2009 Games: Terminology, Reachability, Safety, and Buchi games {{slide6.pdf}} (Barbara Jobstmann)
+
  - 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**
+
 
+
Please find the homework [[LAT:homework|here.]]
+

Revision as of 11:11, 13 February 2013

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

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

  • //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) :