2003/10/28 by J. Desharnais, Josée Desharnais, B. Möller +6
Computer Science · #D.2.4 #F.3.1 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #I.1.3 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0310054
40 pages
arxiv created 2003/10/28 · openalex publication_date 2003/10/28 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.