Material for the course
'Verification of temporal logics on infinite-state systems'
ESSLLI'07

ESSLLI 2007
This site contains course notes and reference materials for the ESSLLI course 'Verification of temporal logics on infinite-state systems', taught by S. Demri and V. Goranko in August 2007 at Trinity College, Dublin.

Course Description
Model-checking of infinite-state systems is a rapidly growing area of formal verification. It has been successfully applied to real-time and hybrid systems, concurrent systems, Petri nets, asynchronous communication devices (unbounded FIFO channels), infinite and unbounded data structures (counters, queues, lists), etc. The single most important property of practical interest in infinite-state transition systems is state reachability which is often undecidable. Therefore, intensive research has been devoted to identifying classes of finitely presentable infinite structures with decidable reachability and related safety properties. This course is decidated to infinite-state systems with decidable verification of temporal properties defined from temporal logics. We present techniques for various classes of systems (counter systems, timed automata, etc.) and logical formalisms.

Prerequisites
This is material that we assume you have already seen and will simply be mentioned in the lectures.

• Basics of finite-automata and Buchi automata.
  
• Basics of logic including first-order logic and temporal logic.
  
• Basics of complexity theory including the definition of the complexity classes NP, PSPACE and EXPTIME.
  

Course material
The slides from the course will be available soon as well as a list of exercises.
The course comprise ten 40-min lectures, delivered 2 per day, with a 5 min break in between.

• Lecture 1: Introduction to the course. Symbolic representations of infinite-state transition systems. Slides
  
• Lecture 2: Verification of basic tense logic on rational Kripke models. Slides
  
• Exercises Day 1 (lectures 1 and 2)
  
• Lecture 3: Symbolic computation of reachability. Slides
  
• Lecture 4: Temporal logics for specification and verification of infinite-state transition systems Slides
  
• Exercises Day 2 (lectures 3 and 4)
  
• Lecture 5: Model-checking temporal logics on pushdown systems Slides
  
• Lecture 6: Decidable and undecidable reachability problems for counter systems Slides
  
• Exercises Day 3 (lectures 5 and 6)
  
• Lecture 7: Temporal logics for counter systems Slides
  
• Lecture 8: Presburger counter systems and acceleration Slides
  
• Lecture 9: Reachability problems for timed automata Slides
  
• Lecture 10: Timed temporal logics Slides
  

Useful readings
The course is intended to prepare you to read the more advanced parts of these papers. Reading one or two introductions from the following papers will give an idea of the area.

• ' Decisions problems for timed automata: a survey ' by R. Alur and P. Madhusudan.
  
• ' Reachability Analysis of Pushdown Automata: Application to Model-Checking ' by A. Bouajjani, J. Esparza and O. Maler.
  
• ' Decidability of reachability problems for classes of two counters automata ' by A. Finkel and G. Sutre.
  
• ' Well-structured transition systems everywhere! ' by A. Finkel and Ph. Schnoebelen.
  
• ' Counter Machines: Decidable Properties and Applications to Verification Problems ' by O. Ibarra, J. Su, Z. Dang, T. Bultan and A. Kemmerer.
  
• ' On the decidability and complexity of metric temporal logic over finite words ' by J. Ouaknine and J. Worrell.
  
• ' Some Perspectives of Infinite-State Verification ' by W. Thomas.