An Analysis of \pi-calculus Bisimulations
Identifieur interne : 00CB62 ( Main/Exploration ); précédent : 00CB61; suivant : 00CB63An Analysis of \pi-calculus Bisimulations
Auteurs : R. Amadio ; O. Ait-MohamedSource :
Abstract
The \pi-calculus is a relatively simple framework in which the semantics of the dynamic creation and transmission of channels can be studied. We consider in particular the issue of defining and verifying the equivalence of \pi-terms in the context of bisimulation based semantics. We distinguish three main contributions : (1) A characterization of `early' bisimulation in terms of a notion of `contextual' bisimulation. (2) The definition of a \pi-calculus with explicit substitutions and the description of an abstract machine based on this notation which incrementally computes the synchronization tree of a \pi-process. (3) The introduction of a refinement of the `late' bisimulation which we call `uniform'. Roughly the latter corresponds to the idea of treating the formal parameter of an input prefix as a `logical' variable. It is argued that this might lead to more efficient verification tools.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 001704
- to stream Crin, to step Curation: 001704
- to stream Crin, to step Checkpoint: 003131
- to stream Main, to step Merge: 00D429
- to stream Main, to step Curation: 00CB62
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="188">An Analysis of \pi-calculus Bisimulations</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:amadio94f</idno>
<date when="1994" year="1994">1994</date>
<idno type="wicri:Area/Crin/Corpus">001704</idno>
<idno type="wicri:Area/Crin/Curation">001704</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001704</idno>
<idno type="wicri:Area/Crin/Checkpoint">003131</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">003131</idno>
<idno type="wicri:Area/Main/Merge">00D429</idno>
<idno type="wicri:Area/Main/Curation">00CB62</idno>
<idno type="wicri:Area/Main/Exploration">00CB62</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">An Analysis of \pi-calculus Bisimulations</title>
<author><name sortKey="Amadio, R" sort="Amadio, R" uniqKey="Amadio R" first="R." last="Amadio">R. Amadio</name>
</author>
<author><name sortKey="Ait Mohamed, O" sort="Ait Mohamed, O" uniqKey="Ait Mohamed O" first="O." last="Ait-Mohamed">O. Ait-Mohamed</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="4224">The \pi-calculus is a relatively simple framework in which the semantics of the dynamic creation and transmission of channels can be studied. We consider in particular the issue of defining and verifying the equivalence of \pi-terms in the context of bisimulation based semantics. We distinguish three main contributions : (1) A characterization of `early' bisimulation in terms of a notion of `contextual' bisimulation. (2) The definition of a \pi-calculus with explicit substitutions and the description of an abstract machine based on this notation which incrementally computes the synchronization tree of a \pi-process. (3) The introduction of a refinement of the `late' bisimulation which we call `uniform'. Roughly the latter corresponds to the idea of treating the formal parameter of an input prefix as a `logical' variable. It is argued that this might lead to more efficient verification tools.</div>
</front>
</TEI>
<affiliations><list></list>
<tree><noCountry><name sortKey="Ait Mohamed, O" sort="Ait Mohamed, O" uniqKey="Ait Mohamed O" first="O." last="Ait-Mohamed">O. Ait-Mohamed</name>
<name sortKey="Amadio, R" sort="Amadio, R" uniqKey="Amadio R" first="R." last="Amadio">R. Amadio</name>
</noCountry>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00CB62 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00CB62 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= CRIN:amadio94f |texte= An Analysis of \pi-calculus Bisimulations }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |