Site officiel du LSV
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.