An Analysis of \pi-calculus Bisimulations
Identifieur interne : 001704 ( Crin/Corpus ); précédent : 001703; suivant : 001705An 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 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></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><BibTex type="techreport"><ref>amadio94f</ref><crinnumber>94-R-351</crinnumber><category>15</category><equipe>EURECA</equipe><author><e>Amadio, R.</e><e>Ait-Mohamed, O.</e></author><title>An Analysis of \pi-calculus Bisimulations</title><institution>European Computer-Industry Research Center</institution><year>1994</year><type>Rapport technique</type><number>94-2</number><address>Munich</address><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.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001704 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 001704 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:amadio94f
|texte= An Analysis of \pi-calculus Bisimulations
}}
| This area was generated with Dilib version V0.6.33. |  |