Concurrency Models with Causality and Events as Psi-calculi

• Main Authors: Håkon Normann, Cristian Prisacariu, Thomas Hildebrandt
• Format: Article
• Language: English
• Published: Open Publishing Association 2014-10-01
• Series: Electronic Proceedings in Theoretical Computer Science
• Online Access: http://arxiv.org/pdf/1410.7466v1

Psi-calculi are a parametric framework for nominal calculi, where standard calculi are found as instances, like the pi-calculus, or the cryptographic spi-calculus and applied-pi. Psi-calculi have an interleaving operational semantics, with a strong foundation on the theory of nominal sets and process algebras. Much of the expressive power of psi-calculi comes from their logical part, i.e., assertions, conditions, and entailment, which are left quite open thus accommodating a wide range of logics. We are interested in how this expressiveness can deal with event-based models of concurrency. We thus take the popular prime event structures model and give an encoding into an instance of psi-calculi. We also take the recent and expressive model of Dynamic Condition Response Graphs (in which event structures are strictly included) and give an encoding into another corresponding instance of psi-calculi. The encodings that we achieve look rather natural and intuitive. Additional results about these encodings give us more confidence in their correctness.