Concurrent Kleene Algebra and its Foundations

A Concurrent Kleene Algebra offers two composition operators, related by a weak version of an exchange law: when applied in a trace model of program semantics, one of them stands for sequential execution and the other for concurrent execution of program components [22]. After introducing this motivating concrete ion, we investigate its abstract background in terms of a primitive independence relation between the traces. On this basis, we develop a series of richer algebras; the richest validates a proof calculus for similar to that of a Jones style rely/guarantee calculus. On the basis of this abstract algebra, we finally reconstruct the original trace model, using the notion of atoms from lattice theory.

• Type: Journal
• Year: 2011
• Where: JLP
• Authors: Tony Hoare, Bernhard Möller, Georg Struth, Ian Wehrman
• Keywords: JLP 2011, Kleene Algebra, Lattice Theory, Program Semantics