LSV Seminar

Date

Tuesday, October 09 2012 at 11:00AM

Place

Salle Condorcet (Bât. d'Alembert)

Speaker

Christoph Haase (LSV, ENS Cachan)

Counter automata are a fundamental model of computation that were introduced by Minsky sixty years ago. They comprise a finite-state automaton with a finite number of counters ranging over the naturals. Along a transition, a counter can be incremented, decremented, or tested for zero. Minsky showed that the restriction to two counters suffices to render reachability undecidable. Due to this negative result, various restrictions on the the set of operations, the underlying graph structure, the operation mode or the number of counters have been considered in the literature and have shown to entail decidable reachability problems. Besides pure theoretical interest, those models have also found applications, for example in the verification of multi-threaded and concurrent programs, programs with linked lists, and modelling of resource-bounded processes.

Throughout the last ten years, there has been a strong interest in model checking infinite graphs generated by subclasses of counter automata against specifications written in temporal logics. In this talk, I am going to give a high-level introduction to some of the main concepts and ideas underlying the lower and upper bounds for various model checking problems with an emphasis on the restriction to one counter. It turns out that many problems have beautiful connections to topics in number theory, such as non-linear Diophantine equations or Frobenius numbers. I will also discuss some open problems and how they relate to open problems in other areas.

This talk is based on joint work with Stefan Göller (Bremen), Stefan Kreutzer (Berlin), and Joel Ouaknine and James Worrell (Oxford).