Counter systems and temporal logics
This site contains slides
and reference materials for the
course 'Counter systems and temporal logics',
taught by
S. Demri
in October/November 2010, Buenos Aires and Córdoba.
Course Description
Counter automata are a fundamental computational model and many decision problems are
known to be undecidable, which is not so surprising since they are equivalent to Turing machines.
Many subclasses have been considered in the literature (reversal-bounded counter machines,
one-counter automata, vector addition systems, counter automata with errors, etc. ) in order to
regain decidability at the cost of reducing their computational power. For instance,
counter machines have many applications in formal verification. Their
ubiquity stems from their use as operational models of numerous infinite-state systems,
including for instance broadcast protocols and programs with pointer variables.
This course is dedicated to present decidable problems for counter machines.
We develop techniques for various classes of counter machines
(vector addition systems, reversal-bounded counter machines, counter automata
with errors, one-counter machines, etc.) and for various problems including
reachability problems, boundedness, and model-checking with temporal logics, which is a
well-known approach to verifying behavioral
properties of computing systems.
Prerequisites
This is the material that we assume you have already seen and will simply be mentioned in the lectures.
- Basics of finite-state automata and Buchi automata.
- Basics of logic including first-order logic and temporal logic.
- Basics of complexity theory, decidability.
Course material
The course comprises six 120-min lectures.
- PART I (Counter systems) -- U. of Buenos Aires
- Lecture 1 (26/10/10): Introduction to counter systems (Minsky machines, Presburger arithmetic, counter
systems).
Slides
- Lecture 2 (28/10/10): Classes with semilinear reachability sets (difference bounds constraints, reversal-bounded counter automata,
affine counter systems with finite monoids).
Slides
- Lecture 3 (29/10/10): Vector addition systems (relationships with Petri nets, coverability graphs,
covering
problem in EXSPACE)
Slides
- PART II (Temporal logics) -- U. Nacional de Córdoba
- Lecture 4 (01/11/10): Linear-time temporal logics for counter systems (plain LTL, automata-based approach, Presburger
LTL, LTL with registers).
Slides
- Lecture 5 (02/11/10): Model-checking counter systems
(decidability results, imperfect counter automata and LTL)
Slides
- Lecture 6 (03/11/10): Data logics and counter systems (temporal logics, first-order logics, register automata, etc.)
Slides
You may like to visit the web page of the course
2.9 of the Master MPRI and to download documents from it.
See also the related
web page for ESSLLI'10 course
on "Decidable problems for counter systems".
Suggestions for readings
-
On Yen's Path Logic for Petri Nets
by M.F. Atig and P. Habermehl.
In RP'09, LNCS 5797, pp. 51--63, 2009. (related to lecture 3)
-
On the freeze quantifier in constraint LTL: decidability and complexity
by S. Demri, R. Lazic, D. Nowak.
IC 205(1):2--24, 2007. (related to lecture 4)
-
Linear-Time Temporal logics with Presburger Constraints: An Overview
by S. Demri.
In JANCL 16(3--4):311--347, 2006. (related to lecture 4)
-
Decidability and Complexity of Petri Net Problems --- An
Introduction by J. Esparza.
In Advances in Petri Nets 1998, LNCS 1491, pp. 374--428, 1998. (related to lecture 3)
-
Reversal-Bounded Counter Machines Revisited by A. Finkel and A. Sangnier.
MFCS'08, LNCS 5162, pp.323--334, 2008. (related to lecture 2)
-
Reversal-bounded multicounter machines and their
decision problems
by O. Ibarra.
JACM 25(1): 116--133, 1978. (related to lecture 2)
-
Automata and Logics for Words and Trees over an Infinite Alphabet
by L. Segoufin.
In CSL'06, LNCS 4207, pp. 41--57, 2006. (related to lecture 6)