BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
A Survey on Model-Checking Problems for Counter Automata
STATUS:CONFIRMED
ATTENDEE;CN="Christoph Haase
":
MAILTO:no@spam.com
DESCRIPTION:
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 rang
ing over the naturals. Along a transition\, a counter can be
incremented\, decremented\, or tested for zero. Minsky show
ed that the restriction to two counters suffices to render r
eachability undecidable. Due to this negative result\, vario
us restrictions on the the set of operations\, the underlyin
g graph structure\, the operation mode or the number of coun
ters have been considered in the literature and have shown t
o entail decidable reachability problems. Besides pure theor
etical interest\, those models have also found applications\
, for example in the verification of multi-threaded and conc
urrent programs\, programs with linked lists\, and modelling
of resource-bounded processes. Throughout the last ten year
s\, there has been a strong interest in model checking infin
ite graphs generated by subclasses of counter automata again
st 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 boun
ds for various model checking problems with an emphasis on t
he restriction to one counter. It turns out that many proble
ms have beautiful connections to topics in number theory\, s
uch 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 join
t work with Stefan Göller (Bremen)\, Stefan Kreutzer (Berlin
)\, and Joel Ouaknine and James Worrell (Oxford).
DTSTART;TZID=Europe/Paris:20121009T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201210091
100
UID:LSVsemLSV.201210091100@lsv.ens-cachan.fr
LOCATION:Salle Condorcet (Bât. d'Alembert)
END:VEVENT
END:VCALENDAR