Kleene Algebras with Domain

Title:	Kleene Algebras with Domain
Authors:	Victor B. F. Gomes (vb358 /at/ cl /dot/ cam /dot/ ac /dot/ uk), Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber (tjark /dot/ weber /at/ it /dot/ uu /dot/ se)
Submission date:	2016-04-12
Abstract:	Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.
BibTeX:	@article{KAD-AFP, author = {Victor B. F. Gomes and Walter Guttmann and Peter Höfner and Georg Struth and Tjark Weber}, title = {Kleene Algebras with Domain}, journal = {Archive of Formal Proofs}, month = apr, year = 2016, note = {\url{http://isa-afp.org/entries/KAD.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Kleene_Algebra
Used by:	Algebraic_VCs, Hybrid_Systems_VCs
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.