A Lightweight Formalization of the Metatheory of Bisimulation-Up-To

Kaustuv Chaudhuri 1 Matteo Cimini 2 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the under-lying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the π-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of co-inductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. Since the logic behind Abella also supports λ-tree syntax and generic reasoning using the ∇-quantifier, our treatment of the π-calculus is both direct and natural.
Type de document :
Communication dans un congrès
Xavier Leroy and Alwen Tiu. 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2015, Mumbai, India. ACM Proceedings, 2014, 〈http://cpp2015.inria.fr〉. 〈10.1145/2676724.2693170〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01091524
Contributeur : Kaustuv Chaudhuri <>
Soumis le : vendredi 5 décembre 2014 - 15:31:01
Dernière modification le : jeudi 11 janvier 2018 - 01:49:36
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:03:58

Fichiers

cpp-hal.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Citation

Kaustuv Chaudhuri, Matteo Cimini, Dale Miller. A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. Xavier Leroy and Alwen Tiu. 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2015, Mumbai, India. ACM Proceedings, 2014, 〈http://cpp2015.inria.fr〉. 〈10.1145/2676724.2693170〉. 〈hal-01091524〉

Partager

Métriques

Consultations de la notice

350

Téléchargements de fichiers

120