Counter automata are an appealing formal model of systems and programs
with an unbounded number of states that find a plethora of
applications, for instance in the verification of concurrent
shared-memory programs. A counter automaton comprises a finite-state
controller with a finite number of counters ranging over the natural
numbers that can be incremented, decremented and tested for zero when
a transition is taken. Despite having been studied since the early
days of computer science, many important problems about decidable
subclasses of counter automata have remained unsolved. This talk will
give an overview over the history and some of the progress on both
theoretical and practical aspects of counter automata that has been made
over the last two years, focusing on new results concerning reachability,
stochastic extensions, practical decision procedures, and the challenges
that lie ahead.
This talk is based on joint work with M. Blondin (Montreal), A. Finkel
(Cachan), S. Haddad (Cachan), P. Hofman (Cachan), S. Kiefer (Oxford)
and M. Lohrey (Siegen).