Kleene algebra with domain
J. Desharnais, B. M\"oller, G. Struth

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
