Concurrent Kleene Algebra and its Foundations

12 years 7 months ago

Download www.dcs.shef.ac.uk

A Concurrent Kleene Algebra oﬀers 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 ﬁnally reconstruct the original trace model, using the notion of atoms from lattice theory.

Tony Hoare, Bernhard Möller, Georg Struth, Ia

Real-time Traffic