Material for the course
'Decidable problems for counter systems'
ESSLLI 2010, Copenhagen
ESSLLI 2010
This site contains
course notes and reference materials for the
ESSLLI course 'Decidable problems for counter systems',
taught by
S. Demri
in August 2010, Copenhagen.
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
Here is the final version of the
lecture notes.
Slides will be available on a daily basis.
The course comprise ten 40-min lectures, delivered 2 per day,
with a 5 min break in between.
- Day 1: Introduction to counter systems (Minsky machines, Presburger arithmetic, counter
systems).
Slides
- Day 2: Linear-time temporal logics for counter systems (plain LTL, automata-based approach, Presburger
LTL, LTL with registers).
Slides
- Day 3: Vector addition systems (VASS vs. FO2 on data words, relationships with Petri nets, coverability graphs, covering
problem in EXSPACE)
Slides
- Day 4: Reversal-bounded counter automata (semilinearity of reachability sets, variants, linear-time properties)
Slides
- Day 5: Model-checking counter systems (decidability results, imperfect counter automata, admissible counter automata and LTL)
Slides
You may like to visit the web page of the course
2.9 of the Master MPRI and to download documents from it.
Useful readings