More on bisimulations for higher order π-calculus

In this paper, we prove the coincidence between strong/weak context bisimulation and strong/weak normal bisimulation for higher order π-calculus, which generalizes Sangiorgi’s work. To achieve this aim, we introduce indexed higher order π-calculus, which is similar to higher order π-calculus except...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2012-08, Vol.446, p.1-19
Main Author: Cao, Zining
Format: Article
Language:English
Subjects:
Bisimulations
Calculus
Higher order [formula omitted]-calculus
Mathematical analysis
Process calculi
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper, we prove the coincidence between strong/weak context bisimulation and strong/weak normal bisimulation for higher order π-calculus, which generalizes Sangiorgi’s work. To achieve this aim, we introduce indexed higher order π-calculus, which is similar to higher order π-calculus except that every prefix of any process is assigned indices. Furthermore we present corresponding indexed bisimulations for this calculus, and prove the equivalence between these indexed bisimulations. Based on this result, we prove the main result of this paper, i.e., the equivalence between strong/weak context bisimulation and strong/weak normal bisimulation.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2012.04.014