The Coq mailing list

[Kumar Neeraj Verma <verma AT lsv.ens-cachan.fr>]

J'ai le plaisir de vous inviter à ma soutenance de thèse et au pot qui 
suivra.

La soutenance aura lieu le mardi 30 septembre à 15h à l'ENS de Cachan,
salle des conférence du Pavillon des Jardins. Le plan d'accès se trouve à
l'adresse suivante : http://www.lsv.ens-cachan.fr/info-acces.php
Le Pavillon des Jardins est indiqué sur le deuxième plan.

La thèse s'intitule:

Automates d'arbres bidirectionnels modulo théories équationnelles

et a été effectuée sous la direction de Jean Goubault-Larrecq.

La soutenance aura lieu devant un jury composé de:

Rémi Gilleron
Jean Goubault-Larrecq
Denis Lugiez
Dale Miller
Michaël Rusinowitch
Helmut Seidl

Résumé:

Les automates d'arbres bidirectionnels étendent les automates 
classiques, en ce
sens que les transitions peuvent non seulement construire mais aussi 
détruire
des termes. Récemment des variantes équationnelles des automates 
d'arbres ont
été proposés qui acceptent des termes modulo une théorie équationnelle. Dans
cette thèse on étudie des automates d'arbres bidirectionnels modulo des 
théories
équationnelles. On étudie les théories AC (associativité, commutativité 
de +),
ACU (avec unité 0), ACUI (avec idempotence x+x=x),
ACUX (avec annulation x+x=0) et ACUM (groupes abéliens). Ces automates
sont importants pour la vérification des protocoles cryptographiques qui
utilisent des primitives cryptographiques non parfaites.

On étudie la décidabilité et la clôture par opérations booléennes de ces
automates. On commence par des résultats négatifs: le vide est 
indécidable pour
les automates bidirectionnels, ou unidirectionnels alternants, modulo les
théories AC, ACU, ACUM.

On montre que les automates unidirectionnels modulo toutes ces théories sont
clos par intersection, et que le vide est décidable. La clôture par 
union est
triviale. A l'opposé, alors que les automates unidirectionnels modulo 
AC, ACU
sont clos par complémentation, ceux modulo ACUX, ACUM et ACUI ne le
sont pas. Les propriétés de clôture et de décidabilité s'étendent au cas
bidirectionnel, pour chaque théorie sauf ACUI, si on restreint le format des
clauses push. On montre cela en réduisant les automates bidirectionnels aux
automates unidirectionnels. (Le cas ACUI est ouvert.) Pour traiter 
certaines
clauses ayant le symbole + dans le corps, on développe une extension des
systèmes d'addition de vecteurs avec états (VASS), appelés VASS étendus. On
montre que la construction des arbres de Karp et Miller pour VASS peut être
étendue pour les VASS étendus.

Ces résultats diffèrent nettement du cas des automates non équationnels
qui ont toutes les propriétés de clôture et de décidabilité.


Abstract:

Two-way tree automata extend classical tree automata by allowing transitions
that can destruct terms besides constructing them. Recently equational 
variants
of tree automata have been proposed which accept terms modulo an equational
theory. In this thesis we study two-way equational tree automata. We study
the theories AC (associativity, commutativity of +), ACU (with unit 0),
ACUI (with idempotence x+x=x), ACUX (with cancellation x+x=0) and
ACUM (Abelian groups). These automata are useful in verification of
cryptographic protocols which use non-perfect cryptographic primitives.

We study the properties of decidability and closure under Boolean operations
of these automata. We start with negative results: emptiness is undecidable
for alternating one-way automata, as well as for general two-way automata
modulo the theories AC, ACU, ACUM.

We show that the one-way automata modulo all these theories are closed under
intersection, and emptiness is decidable. Closure under union is 
trivial. On the
other hand, while the one-way automata modulo AC, ACUare closed under
complementation, those modulo ACUX, ACUM and ACUI are not. These closure
and decidability properties extend to the two-way case, for each theory 
except
ACUI, if we restrict the format of push clauses. We show this by reducing
the two-way automata to one-way automata. (The ACUI case is open.) In order
to deal with certain push clauses which have the + symbol in the body, we
develop an extension of Vector Addition Systems with States (VASS), called
Extended VASSes, in which transitions can add configurations. We show 
that the
construction of  Karp and Miller trees for VASS can be extended for Extended
VASSes.

Our results on one-way and two-way equational tree automata are strikingly
different from the case of non-equational automata which have all the good
closure and decidability properties.

--
Kumar Neeraj Verma