Using algebra for concurrency: Some approaches

Abstract

This short introduction to an algebraic approach to concurrency has necessarily omitted some intricate details, as well as paying no attention to other algebraic approaches (for example, Vaughan Pratt has suggested an approach which generalises the Kahn networks in a different manner). What we hope to have shown is that four kinds of operator — namely atomic action (α.), summation (+), product (&_β or |) and encapsulation (/β or \β) — together give great expressive power, and moreover satisfy interesting algebraic identities.

In a methodology for proof about particular systems, we almost certainly need more than "just" algebra. With algebra, we can typically prove equations between agent expressions; we often wish also to prove that an agent possesses some property which is not expressible by an equation. It is therefore important to look at the relation between such algebras and logics — Temporal or Modal logics — designed to express interesting properties of processes.

Another important relationship to study is between the algebraic approach and Net Theory. The emphases of these models are different; communication is the cornerstone of the algebra (in the present approach), while Net Theory emphasizes causal independence, provides a totally different graphical aid to intuition, and provides different tools for abstraction.

Finally, synchronous systems demand some form of treatment. The author has found one way of integrating the above asynchronous algebra with an algebra of synchronous (clocked) systems; this method has some mathematical simplicity — for example, the algebra becomes more conventional, being at least a semi-ring (with agent sum and product as the semi-ring operations) — but is by no means obviously the best integration possible.