Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

A Survey on Model-Checking Problems for Counter Automata

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Christoph Haase
Date
Le mardi 09 octobre 2012 à 11:00
Lieu
Salle Condorcet (Bât. d'Alembert)
Orateur
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).


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

No entries.

Les séminaires précédents