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:
An Easy Algorithm For The General Vector Addition System Rea
chability Problem
STATUS:CONFIRMED
ATTENDEE;CN="JérÃ´me Leroux
":
MAILTO:no@spam.com
DESCRIPTION:
The reachability problem for Vector Addition Systems (VAS)
or equivalently for Petri Nets is a central problem of net t
heory. The general problem is known decidable by algorithms
exclusively based on the classical Kosaraju-Lambert-Mayr-Sac
erdote-Tenney (KLMST) decomposition. This decomposition is d
ifficult and it just has a non-primitive recursive upper-bou
nd complexity. In this paper\, we prove that if a final conf
iguration is not reachable from an initial one\, there exist
s a pair of Presburger formulas denoting an inductive separa
tor proving this property. Since we can decide with any deci
sion procedure for the Presburger arithmetic if pairs of Pre
sburger formulas denote inductive separators\, we deduce tha
t there exist checkable certificates of non-reachability. In
particular\, there exists an easy algorithm for deciding th
e general VAS reachability problem based on two semi-algorit
hms. A first one that tries to prove the reachability by fai
rly enumerating finite sequence of actions and a second one
that tries to prove the non-reachability by fairly enumerati
ng pairs of Presburger formulas. Even if the KLMST decomposi
tion is used for proving the termination\, this algorithm is
the very first one that can be implemented without using it
.
DTSTART;TZID=Europe/Paris:20081209T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200812091
100
UID:LSVsemLSV.200812091100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR