Automatically Proving Up-to Bisimulation

Nous développons diverses méthodes permettant d'automatiser des preuves de bisimulation up-to pour le -calcul. Nous traitons les techniques à congruence structurelle près (par l'intermédiaire de la dénition d'un algorithme calculant une forme normale unique pour la congruence structurelle), à substitutions injectives sur les noms li-bres près, à restriction près, et à composition parallèle près. Ces techniques permettent de réduire la taille des relations que l'on doit ex-hiber an de prouver un résultat de bisimilarité. Dans le cadre d'une implémentation, cela présente des avantages immédiats en termes de gestion de la mémoire; en outre, sur le plan de l'expressivité de notre système, la technique de preuve à composition parallèle près permet de prendre en compte certains termes comportant l'opérateur de répli-cation, et dont l'espace d'états est inni (chose que ne peuvent faire les outils existants pour le -calcul). Nous illustrons les divers avantages de ces méthodes sur une implémentation. We present a methodology for checking bisimilarities between -calculus processes with the up-to techniques for bisimulation. These techniques are used to reduce the size of the relation one has to exhibit to prove a bisimulation. Not only is this interesting in terms of space management, but it also increases dramatically the expressive power of our system, by making in some cases the verication of innite states space processes possible. Based on an algorithm to compute a unique normal form for structural congruence, we develop sound and complete methods to check bisimulation up to injective substitutions on free names, up to restriction and up to parallel composition. We show the expressiveness of our techniques on a prototype implementation