A theory of communicating transactions

We propose a novel language construct called communicating transactions, obtained by dropping the isolation requirement from classical transactions, which can be used to model automatic error recovery in distributed systems. We extend CCS with this construct and give a simple semantics for the extended calculus, called TransCCS. We develop a sound and complete theory for both may and fair-testing, which we believe are the appropriate notions to capture safety and liveness in TransCCS. We exhibit the usefulness of our theory by proving illuminating laws and simple but non-trivial examples.