Computing Strong and Weak Bisimulations for Psi-Calculi
2012 (English)In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 81, no 3, 162-180 p.Article in journal (Refereed) Published
We present a symbolic transition system and strong and weak bisimulation equivalences for psi-calculi, and show that they are fully abstract with respect to bisimulation congruences in the non-symbolic semantics. A procedure which computes the most general constraint under which two agents are bisimilar is developed and proved correct.
A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations. Psi-calculi can be more general than other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, or the concurrent constraint pi-calculus.
Symbolic semantics are necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means the symbolic semantics makes exactly the same distinctions as the original.
Place, publisher, year, edition, pages
Elsevier, 2012. Vol. 81, no 3, 162-180 p.
Symbolic semantics, Bisimulation, Psi-calculi, Full abstraction
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-162421DOI: 10.1016/j.jlap.2012.01.001ISI: 000302500700002OAI: oai:DiVA.org:uu-162421DiVA: diva2:460442
The 22nd Nordic Workshop on Programming Theory — NWPT 2010, 10-12 November 2010, Turku Finland