An Analysis of \pi-calculus Bisimulations
Identifieur interne : 00CB62 ( Main/Curation ); 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.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001704
- to stream Crin, to step Curation: Pour aller vers cette notice dans l'étape Curation :001704
- to stream Crin, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :003131
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00D429
Links to Exploration step
CRIN:amadio94fLe 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>
</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>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00CB62 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/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= Curation |type= RBID |clé= CRIN:amadio94f |texte= An Analysis of \pi-calculus Bisimulations }}
This area was generated with Dilib version V0.6.33. |