04/12/2003
Francesco Zappa Nardelli (ENS)
Méthodes de preuve basés sur la bisimulation pour les Ambients Mobiles

Travail commun avec Massimo Merro (U. Verona, Italie)

Nous étudions la théorie comportementale du calcul des Ambients Mobiles de Cardelli et Gordon. Un nouveau système de transitions étiquetées nous permet de définir une bisimulation étiquetée qui caractérise l'équivalence comportementale naturelle. Nous démontrons aussi que des techniques de preuve dites « up-to » sont correctes. Nos résultats permettent de prouver aisément un ensemble de lois algébriques, parmi lesquelles figure l'équation du firewall parfait.