Abstract

This talk is on the foundational side. In 2009, Concurrent Kleene Algebra (briefly CKA ) was defined as an extension of Kleene Algebra, adding to sequential composition several variants of concurrent composition while preserving the standard laws. The aim was to allow, in parallel to operational or assertion-logical deduction, also algebraic, (in)equational proofs about concurrent systems. This is particularly interesting, since (in)equational reasoning is very suitable for semi-automatic or even automatic proofs. CKA has met considerable interest. We discuss some new twists about it. - We present a new definition technique for partial operators, namely an assume/claim style akin to the rely/guarantee format of program specification. This admits a general way of defining a refinement relation as well as Top and Bottom elements of the refinement order. - We experiment with the graph model of the algebra, in particular how state-like entities could be defined, along with image and inverse image operators. This allows a form of Hoare triples and relates to O’Hearn’s resource view of these. It remains to be seen whether a purely algebraic abstraction of the approach can be found. The talk is based on unpublished joint work with Tony Hoare.