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 @p-calculus, which generalizes Sangiorgi's work. To achieve this aim, we introduce indexed higher order @p-calculus, which is similar to higher order @p-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.

• Publication year

  2012

• Venue

  Theoretical Computer Science

• Publication date

  2012-08-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1016/j.tcs.2012.04.014
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• On the Expressiveness and Decidability of Higher-Order Process Calculi

  2008cited by this paper
• The π-Calculus: A theory of mobile processes

  2008cited by this paper
• Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA

  2008cited by this paper
• Call-by-Value Termination in the Untyped lambda-Calculus

  2008cited by this paper
• Environmental Bisimulations for Higher-Order Languages

  2007cited by this paper
• A Spatial Logical Characterisation of Context Bisimulation

  2006cited by this paper
• More on Bisimulations for Higher Order pi-Calculus

  2006cited by this paper
• A bisimulation-based semantic theory of Safe Ambients

  2006cited by this paper
• Plain CHOCS A second generation calculus for higher order processes

  2005cited by this paper
• Contextual equivalence for higher-order pi-calculus revisited

  2005cited by this paper
• The Kell Calculus: A Family of Higher-Order Distributed Process Calculi

  2004cited by this paper
• A Uniform Reduction Equivalence for Process Calculi

  2004cited by this paper
• Towards a theory of bisimulation for the higher-order process calculi

  2004cited by this paper
• Bisimulation Congruences for Homer a calculus of Higher-order mobile embedded resources

  2004cited by this paper
• Contextual equivalence for higher-order π-calculus revisited

  2003cited by this paper
• Edinburgh Research Explorer A Calculus of Mobile Processes, I

  2003cited by this paper
• A Calculus of Mobile Resources

  2002cited by this paper
• The Pi-Calculus - a theory of mobile processes

  2001cited by this paper
• A theory of bisimulation for a fragment of Concurrent ML with local names

  2000cited by this paper
• Bisimulations in the join-calculus

  1998cited by this paper
• A hierarchy of equivalences for asynchronous calculi

  1998cited by this paper
• A theory of weak bisimulation for core CML

  1996cited by this paper
• Bisimulation for Higher-Order Process Calculi

  1994cited by this paper
• Expressing mobility in process algebras : first-order and higher-order paradigms

  1993influential reference
• A Calculus of Mobile Processes, II

  1992cited by this paper
• Calculus of Communicating Systems

  1991cited by this paper
• A Calculus of Mobile Processes, Part I

  1989cited by this paper
• Introduction to the Calculus

  year unknowncited by this paper

• Theoretical Computer Science: 39th National Conference of Theoretical Computer Science, NCTCS 2021, Yinchuan, China, July 23–25, 2021, Revised Selected Papers

  2021cites this paper
• Bisimulation for Parameterized Higher-order Processes

  2018cites this paper
• On parameterization of higher-order processes

  2017cites this paper
• HOCore in Coq

  2015cites this paper
• Higher-Order π-Calculus with the Mismatch Operator

  2014cites this paper
• Normal Bisimulation for Higher Order Pi-Calculus with Unguarded Choice

  2013influential citation
• On Context Bisimulation for Parameterized Higher-order Processes

  2013cites this paper
• Characterizing contextual equivalence in calculi with passivation

  2011cites this paper
• Bisimulations for Open Processes in Higher Order p-Calculus

  2010cites this paper
• Reducing Higher Order Pi-Calculus to Spatial Logics

  2010cites this paper
• Higher-Order Concurrency: Expressiveness and Decidability Results

  2010cites this paper