Concurrency Models with Causality and Events as Psi-calculi

TL;DR

This paper encodes event-based concurrency models, specifically prime event structures and Dynamic Condition Response Graphs, into psi-calculi, demonstrating the framework's expressive power for representing complex concurrent behaviors.

Contribution

It provides natural and intuitive encodings of event-based models into psi-calculi, expanding the framework's applicability to concurrency with causality and events.

Findings

Successful encoding of prime event structures into psi-calculi

Encoding of Dynamic Condition Response Graphs into psi-calculi

Encodings are natural, intuitive, and supported by correctness evidence

Abstract

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.