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:
lAlBlC: a program testing the equivalence of dpda's
STATUS:CONFIRMED
ATTENDEE;CN="Géraud Sénizergues
":
MAILTO:no@spam.com
DESCRIPTION:
We present a preliminary version of the program "lAlBlC" (i.
e. lA=lB? let us Compute). The equivalence problem for dpda
consists in deciding\, for two given deterministic pushdown
automata A\,B\, whether they recognize the same language. It
was proved in [TCS 2001\, G.S.] that this problem is decida
ble by means of some complete proof systems. The program lAl
BlC gives\, in some sense\, life to the above completeness p
roof: on an input A\,B\, the program computes either a proof
of their equivalence (w.r.t. to the system D5 of the above
reference) or it computes a witness of their non-equivalence
(i.e. a word that belongs to the symmetric difference of th
e two languages). We shall outline the main mathematical obj
ects that are manipulated as well as the main functions perf
ormed over these objects. We shall emphasize the functionnal
style of the most abstract part of the program (synthesis o
f strategies from a sequence of tactics\, computation of a t
actics from a sequence of functions) as well as the algebrai
c structure that the basic objects are implementing: the gro
upoid of deterministic rational matrices over some structure
d alphabet. We shall also explain the experimental results o
btained so far (size of dpda's or grammars treated up to now
\, time and space of the computations\, size of the proofs).
The talk is based on an ongoing\, joint\, work with P. Henr
y.
DTSTART;TZID=Europe/Paris:20130129T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201301291
100
UID:LSVsemLSV.201301291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR