Bisimulation for higher-order process calculi

Davide Sangiorgi 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : A higher-order process calculus is a calculus for communicating systems which contains higher-order constructs like communication of terms. We analyse the notion of bisimulation in these calculi. We argue that %, if static binding is assumed, both the standard definition of bisimulation (i.e., the one for CCS and related calculi), as well as higher-order bisimulation \cite{AsGi88,Bou89,Tho90} are in general unsatisfactory, because over-discriminating. We propose and study a new form of bisimulation for such calculi, called context bisimulation, which yields a more satisfactory discriminanting power. A drawback of context bisimulation is the heavy use of universal quantification in its definition. A major goal of the paper is to find characterisations which make bisimilarities easier to verify. An important role in our theory is played by the factorisation theorem: When comparing the behaviour of two processes, it allows us to «isolate» subcomponents which might cause differences, so that the analysis can be concentrated on them.
Type de document :
RR-2508, INRIA. 1995
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:39:55
Dernière modification le : jeudi 11 janvier 2018 - 16:41:41
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:06:20



  • HAL Id : inria-00074170, version 1



Davide Sangiorgi. Bisimulation for higher-order process calculi. RR-2508, INRIA. 1995. 〈inria-00074170〉



Consultations de la notice


Téléchargements de fichiers