Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

lAlBlC: a program testing the equivalence of dpda's

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Géraud Sénizergues
Le mardi 29 janvier 2013 à 11:00
Salle de Conférence (Pavillon des Jardins)
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.

À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

No entries.

Les séminaires précédents