A non-interleaving process calculus for multi-party synchronisation
arXiv:0912.0555 · doi:10.4204/EPTCS.12.6
Abstract
We introduce the wire calculus. Its dynamic features are inspired by Milner's CCS: a unary prefix operation, binary choice and a standard recursion construct. Instead of an interleaving parallel composition operator there are operators for synchronisation along a common boundary and non-communicating parallel composition. The (operational) semantics is a labelled transition system obtained with SOS rules. Bisimilarity is a congruence with respect to the operators of the language. Quotienting terms by bisimilarity results in a compact closed category.