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:
The Computational Complexity of Verifying One-Counter Proces
ses
STATUS:CONFIRMED
ATTENDEE;CN="Stefan Göller
":
MAILTO:no@spam.com
DESCRIPTION:
A one-counter automaton is a pushdown automaton over a singl
eton stack alphabet plus a bottom-of-stack symbol. I will ta
lk about equivalence checking and model checking of processe
s generated by one-counter automata\, so-called one-counter
processes (OCPs). The goal of the talk is to present some id
eas and techniques that are used for obtaining complexity bo
unds for these problems. In the first part of the talk I pla
n to show that it is PSPACE-complete to decide strong bisimu
lation equivalence for OCPs. The previously best known upper
bound for this problem was 3-EXPSPACE. The same problem tur
ns out to be NL-complete when the processes are described by
deterministic one-counter automata. In the second part of t
he talk\, I plan to discuss a technique for proving lower bo
unds by employing two known results from complexity theory:
(i) Converting a natural number in Chinese remainder present
ation into binary presentation is in logspace-uniform NC^1 a
nd (ii) PSPACE is AC^0-serializable. With the latter one can
prove that there exists a fixed CTL formula for which model
checking of OCPs is PSPACE-hard. With the same technique on
e can show some further lower bounds\, as for example the fo
llowing one: The emptiness problem for timed automata with t
wo clocks but with modulo tests is PSPACE-complete even if a
ll numbers are encoded in unary. The results were obtained i
n joint works with Stanislav Böhm\, Petr Jancar and Markus L
ohrey.
DTSTART;TZID=Europe/Paris:20111122T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111221
100
UID:LSVsemLSV.201111221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR