Kleene Algebra (KA) is a paradigm for reasoning about equivalence between programs. Its (sound and complete) axioms allow us to answer verification questions such as "does program A refine specification B?" or "is this transformation semantics-preserving?". As a matter of fact, queries such as these can be answered mechanically.
In recent years, extensions and refinements of KA have been proposed, each of which can be applied to reason about different kinds of programs in more detail. The question then arises: can we find sound and complete axioms for these variants? And can equivalence queries be similarly mechanised? While each flavour of KA has its own idiosyncrasies, it turns out that there are some common techniques that pop up when considering these questions.
We start out with a brief introduction to KA, and then consider the features of three variants (synchronous, concurrent and guarded). For each variant, we discuss results and ongoing efforts towards axiomatisation and decidability, and the techniques that have proven successful so far.
This talk includes joint work with Paul Brunet, Nate Foster, Justin Hsu, Dexter Kozen, Bas Luttik, Jurriaan Rot, Alexandra Silva, Steffen Smolka, Jana Wagemaker and Fabio Zanasi. |