uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Weak Equivalences in Psi-calculi
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)ORCID iD: 0000-0003-0174-9032
2010 (English)In: Proc. 25th Symposium on Logic in Computer Science: LICS 2010, Piscataway, NJ: IEEE , 2010, 322-331 p.Conference paper, Published paper (Refereed)
Abstract [en]

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.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-121396DOI: 10.1109/LICS.2010.30ISBN: 978-1-4244-7588-9 (print)OAI: oai:DiVA.org:uu-121396DiVA: diva2:305227
Conference
Logic in Computer Science 2010
Projects
UPMARCProFun
Available from: 2010-03-23 Created: 2010-03-23 Last updated: 2016-02-25

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Johansson, MagnusBengtson, JesperParrow, JoachimVictor, Björn

Search in DiVA

By author/editor
Johansson, MagnusBengtson, JesperParrow, JoachimVictor, Björn
By organisation
Computing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 609 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf