Kleene Algebra and variants thereof have been successfully used in verification of se- quential programs. The leap to concurrent programs offers many challenges, both in terms of devising the right foundations to study concurrent variants of Kleene Algebra but also in finding the right models to enable effective verification of relevant programs. In this talk, we will review existing and ongoing work on concurrent Kleene Algebra with a focus on a variant called partially observable concurrent Kleene algebra (POCKA). POCKA offers an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. We will show how a previously developed technique for com- pleteness of Kleene Algebra can be lifted to prove that POCKA is a sound and complete axiomatization of a model of partial observations. We illustrate the use of the framework in the analysis of sequential consistency, i.e., whether programs behave as if memory accesses taking place were interleaved and executed sequentially. The work described in this invited talk is based on [1, 2, 3], and it is joint with a won- derful group of people: Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi.

Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency. The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi [Tobias Kappé et al., 2017; Tobias Kappé et al., 2019; Kappé et al., 2018].

Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operational perspectives is important, for both foundations and applications. This paper takes an important step towards such a correspondence, by precisely relating bi-Kleene Algebra (BKA), a fragment of CKA, to a novel type of automata, pomset automata (PAs). We show that PAs can implement the BKA semantics of series-parallel rational expressions, and that a class of PAs can be translated back to these expressions. We also characterise the behavior of general PAs in terms of context-free pomset grammars; consequently, universality, equivalence and series-parallel rationality of general PAs are undecidable.

Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. Up until now, a description of the free model that corresponds to the CKA axioms was missing. Using a fixpoint construction, we show that the free model of the fragment of CKA with bounded parallelism consists of pomset languages that are downward-closed under the subsumption (linearisation) order.

Kleene Algebra (KA) is a successful framework for studying program flow; it sports a simple yet expressive syntax, as well as efficient algorithms for model checking. Recently, Concurrent Kleene Algebra (CKA) has been proposed by Hoare et al. as an extension of KA, aimed at incorporating concurrent composition. We shall review some hurdles recently taken in the process of extending the toolkit of KA to one for CKA, as well as some problems yet to tackle.

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years. We pave the way towards a solution, by presenting a new automaton model and a Kleene-like theorem for CKA. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours.