Kleene Modules

摘要

We propose axioms for Kleene modules (KM). These structures have a Kleene algebra and a Boolean algebra as sorts. The scalar products are mappings from the Kleene algebra and the Boolean algebra into the Boolean algebra that arise as algebraic abstractions of relational image and preimage operations. KM is the basis of algebraic variants of dynamic logics. We develop a calculus for KM and discuss its relation to Kleene algebra with domain and to dynamic and test algebras. As an example, we apply KM to the reachability analysis in digraphs.