Kleene algebra with domain
Logic in Computer Science
2007-05-23 v1
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.
Keywords
Cite
@article{arxiv.cs/0310054,
title = {Kleene algebra with domain},
author = {J. Desharnais and B. Möller and G. Struth},
journal= {arXiv preprint arXiv:cs/0310054},
year = {2007}
}
Comments
40 pages