Kleene algebra with domain

TL;DR

This paper introduces Kleene algebra with domain (KAD), extending Kleene algebra with domain and codomain axioms, enhancing its expressiveness for state transition systems and enabling algebraic reasoning about properties like Noethericity and Hoare logic.

Contribution

The paper presents KAD, an extension of Kleene algebra with new axioms, along with its calculus, models, and applications to formal reasoning.

Findings

KAD significantly increases the expressiveness of Kleene algebra.

Algebraic reconstruction of Noethericity and well-foundedness.

Algebraic reconstruction of propositional Hoare logic.

Abstract

We propose Kleene algebra with domain (KAD), an extension of Kleene algebra with two equational axioms for a domain and a codomain operation, respectively. KAD considerably augments the expressiveness of Kleene algebra, in particular for the specification and analysis of state transition systems. We develop the basic calculus, discuss some related theories and present the most important models of KAD. We demonstrate applicability by two examples: First, an algebraic reconstruction of Noethericity and well-foundedness; second, an algebraic reconstruction of propositional Hoare logic.