### 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.

### License

### Topics

- Computer science/Programming languages/Logics
- Computer science/Automata and formal languages
- Mathematics/Algebra

### Session KAD

- Domain_Semiring
- Antidomain_Semiring
- Range_Semiring
- Modal_Kleene_Algebra
- Modal_Kleene_Algebra_Models
- Modal_Kleene_Algebra_Applications