Modal Kleene Algebras: Foundations, Models, Automation

Georg Struth

(The University of Sheffield)

Kleene algebras are fundamental structures in computing.
Applications range from formal language theory to program
analysis and verification, concurrency control and the design of
algorithms. This talk surveys recent extensions of Kleene algebras by
modal operators. It sketches the axiomatisation and calculus of modal
Kleene algebras, some interesting models, such as traces, graphs,
relations and predicate transformers, and their connection with
Boolean algebras with operators, propositional dynamic logics and
temporal logics. A particular benefit of the algebraic approach is
that some complex analysis tasks that previously required higher-order
reasoning can, for the first time, be fully automated through
equational reasoning with off-the-shelf theorem provers. This is
illustrated through several examples: program analysis in Hoare logic,
Bachmair and Dershowitz's termination theorem for rewrite systems,
Back's atomicity refinement theorem and a correspondence proof
of Loeb's formula in modal/provability logic.

Tuesday 30th October 2007, 14:00
Robert Recorde Room
Department of Computer Science