Weak Equivalences in Psi-calculi
2010 (English)In: Proc. 25th Symposium on Logic in Computer Science: LICS 2010, Piscataway, NJ: IEEE , 2010, 322-331 p.Conference paper (Refereed)
Psi-calculi extend the pi-calculus with nominal datatypes to represent data, communication channels, and logics for facts and conditions. This general framework admits highly expressive formalisms such as concurrent higher-order constraints and advanced cryptographic primitives. We here establish the theory of weak bisimulation, where the tau actions are unobservable. In comparison to other calculi the presence of assertions poses a significant challenge in the definition of weak bisimulation, and although there appears to be a spectrum of possibilities we show that only a few are reasonable. We demonstrate that the complications mainly stem from psi-calculi where the associated logic does not satisfy weakening.
We prove that weak bisimulation equivalence has the expected algebraic properties and that the corresponding observation congruence is preserved by all operators. These proofs have been machine checked in Isabelle. The notion of weak barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of barbs in all static contexts. We prove that weak barbed equivalence coincides with weak bisimulation equivalence.
Place, publisher, year, edition, pages
Piscataway, NJ: IEEE , 2010. 322-331 p.
IdentifiersURN: urn:nbn:se:uu:diva-121396DOI: 10.1109/LICS.2010.30ISBN: 978-1-4244-7588-9OAI: oai:DiVA.org:uu-121396DiVA: diva2:305227
Logic in Computer Science 2010