Introduction to Kleene algebra
Kleene algebras were proposed originally as axiom systems for the equational theory of regular expressions. Yet beyond their place in theoretical computer science, they have been used widely in computational modelling, in particular program construction and verification. This lecture series introduces some of the most prominent variants, including Kleene algebras with tests, modal Kleene algebras and concurrent Kleene algebras, and discusses some typical applications.
After a brief historical overview, I introduce Kozen's axiom system for Kleene algebra, discuss some computationally interesting models and present Kozen's completeness proof with respect to the equational theory of regular expressions. Then I show shown how Kleene algebras with tests allow one to model simple while programs and to verify them in algebraic approaches to Hoare logic and Morgan's refinement calculus. Next I present modal Kleene algebras, point out connections to dynamic logics and predicate transformer semantics, and discuss additional applications in program analysis and verification. Finally, I introduce concurrent Kleene algebra together with its most important models, and outline some directions for future research.
Program verification components based on variants of Kleene algebra and formalised with the Isabelle/HOL proof assistant will be presented during the lectures and explored in the exercise sessions.
- G. Struth. Introduction to Kleene algebra. Slides from the EWSCS 2018 course.
March 3, 2018 23:55 Europe/Helsinki (GMT +02:00)
local organizers, ewscs18(at)cs.ioc.ee
EWSCS'18 page: http://cs.ioc.ee/ewscs/2018/