Kleene modules

We propose axioms for Kleene modules (KM). These structures have a Kleene algebra K and a Boolean algebra B as sorts. The scalar products are mappings K x B -> B; they 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 directed graphs. Keywords: Idempotent semirings, Kleene algebra, propositional dynamic logic, dynamic and test algebra, image and preimage operation, state transition systems, program development and analysis, graph algorithm