Modal Kleene Algebras: Foundations, Models, Automation
by
Georg Struth
Department of Computer Science, University of Sheffield, UK

Modal Kleene Algebras:
Foundations, Models, Automation

Georg Struth

Over the last decade, Kleene algebras emerged as fundamental structures in computing. Originally conceived as algebras of regular events, theory and applications are currently rapidly evolving. Particular strengths are syntactic simplicity, universal applicability, concise equational proofs, easy mechanisability and strong decidability. This lead to simplifications and unifications in many areas of computing, including program semantics, analysis and verification, term rewriting, concurrency control and game theory. Formally, Kleene algebras are (additively) idempotent semirings extended by Park-style fixedpoint operators. In the context of programming, they model actions of an agent or system under choice, sequential composition and finite iteration. To model program tests or propositions, e.g., in if-then-else statements or while-loops, Boolean algebras-so-called test algebras-can be embedded into the subalgebra bounded by 0 and 1; the destructive and the ineffective action .

This talk surveys the author's recent extension of Kleene algebras by modal operators that bridges the gap between relation-algebraic and modal approaches, and opens the door to novel applications. These modalities are action-indexed endofunctions on test algebras axiomatised by three simple equations. The talk sketches the calculus of modal Kleene algebras, their connection with Boolean algebras with operators and their relationship to computational logics such as PDL, LTL and Hoare logic. It also discusses their capacity to treat some important models in a uniform way, e.g., relations, predicate transformers, languages and traces. As a particular benefit of the algebraic approach, some complex program semantics and analysis tasks that previously presumed set theory or higher-order logics can, for the first time, be fully automated through equational reasoning with off the shelf theorem provers. This is illustrated by three examples: Bachmair and Dershowitz's well-founded union theorem, Hoare logic and Goldblatt's calculational correspondence proof of Löb's formula.

The results presented are based on joint work with Jules Desharnais, Peter Höfner and Bernhard Möller.

PDF

Date received: May 14, 2007