Material for the course
'Decidable problems for counter systems'
ESSLLI 2010, Copenhagen

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.

This is the material that we assume you have already seen and will simply be mentioned in the lectures. 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.

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