Bisimulations up-to: beyond first-order transition systems

Jean-Marie Madiot 1, 2, * Damien Pous 1, * Davide Sangiorgi 2, 3, *
* Auteur correspondant
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : The bisimulation proof method can be enhanced by employing 'bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on the notion of compatible function for fixed-point theory. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpus of up-to techniques that are available on first-order LTSs. The only ingredient that has to be manually supplied is the compatibility of basic up-to techniques that are specific to the new languages. We investigate the method on the pi-calculus, the lambda-calculus, and a (call-by-value) lambda-calculus with references.
Type de document :
Communication dans un congrès
CONCUR, Sep 2014, Rome, Italy. 2014, 〈10.1007/978-3-662-44584-6_8〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger
Contributeur : Damien Pous <>
Soumis le : mercredi 14 mai 2014 - 12:01:42
Dernière modification le : vendredi 20 avril 2018 - 15:44:25
Document(s) archivé(s) le : jeudi 14 août 2014 - 11:30:48


Fichiers produits par l'(les) auteur(s)




Jean-Marie Madiot, Damien Pous, Davide Sangiorgi. Bisimulations up-to: beyond first-order transition systems. CONCUR, Sep 2014, Rome, Italy. 2014, 〈10.1007/978-3-662-44584-6_8〉. 〈hal-00990859〉



Consultations de la notice


Téléchargements de fichiers