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
Psi-calculi: a framework for mobile process calculi: Cook your own correct process calculus - just add data and logic
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Mobility)
2010 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

A psi-calculus is an extension of the pi-calculus with nominal data types for data structures, logical assertions, and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Expressiveness and therefore modelling convenience significantly exceed those of other formalisms: psi-calculi can capture the same phenomena as other extensions of the pi-calculus, and can be more general, e.g. by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions.

Ample comparisons to related calculi are provided and a few significant applications are discussed. The labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. Minimal requirements on the nominal data and logic are established in order to prove general algebraic properties of psi-calculi. The purity of the semantics is on par with the pi-calculus.

The theory of weak bisimulation is established, where the tau actions are unobservable. The notion of barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of weak barbs in all static contexts. It is proved that weak barbed equivalence coincides with weak bisimulation equivalence.

A symbolic transition system and bisimulation equivalence is presented, and shown fully abstract with respect to bisimulation congruence in the non-symbolic semantics. The symbolic semantics is necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means processes are bisimilar in the symbolic setting if they are bisimilar in the original semantics.

Psi-calculi remove the necessity of proving general properties every time a new mobile process calculus is defined. By properly instantiating the framework the properties are guaranteed to hold, thus removing the need to do tedious and error-prone proofs.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2010. , p. 184
Series
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 94
Keywords [en]
process calculi, pi-calculus, bisimulation, operational semantics, nominal logic
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-123139ISBN: 978-91-554-7818-6 (print)OAI: oai:DiVA.org:uu-123139DiVA, id: diva2:312489
Public defence
2010-05-31, Room 2446, Polacksbacken, Lägerhyddsvägen 2D, Uppsala, 13:15 (English)
Opponent
Supervisors
Projects
UPMARCAvailable from: 2010-05-10 Created: 2010-04-25 Last updated: 2019-02-25Bibliographically approved

Open Access in DiVA

fulltext(1624 kB)544 downloads
File information
File name FULLTEXT01.pdfFile size 1624 kBChecksum SHA-512
82629f272e4e7e42221be4a5ed42bd1460c10c739eccc2907e4aedf72e4ba6a02439abfa2c417ab02c1b97bddc1c74e7221303fa35061327fb3481ac8a6147b3
Type fulltextMimetype application/pdf
Buy this publication >>

Authority records BETA

Johansson, Magnus

Search in DiVA

By author/editor
Johansson, Magnus
By organisation
Division of Computer SystemsComputer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 544 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 2443 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