LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
lAlBlC: a program testing the equivalence of dpda's
- Date
- Tuesday, January 29 2013 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Géraud Sénizergues (LaBRI, Université Bordeaux-1)
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 decidable by means of some complete proof systems.
The program lAlBlC gives, in some sense, life to the above completeness proof: 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 the two languages).
We shall outline the main mathematical objects that are manipulated as well as the main functions performed over these objects. We shall emphasize the functionnal style of the most abstract part of the program (synthesis of strategies from a sequence of tactics, computation of a tactics from a sequence of functions) as well as the algebraic structure that the basic objects are implementing: the groupoid of deterministic rational matrices over some structured alphabet.
We shall also explain the experimental results obtained 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. Henry.