Kleene getting lazy

摘要

We propose a relaxation of Kleene algebra by giving up strictness and right-distributivity of composition. This allows the subsumption of Dijkstra's computation calculus, Cohen's omega algebra and von Wright's demonic refinement algebra. Moreover, by adding domain and codomain operators we can also incorporate modal operators. We show that predicate transformers form lazy Kleene algebras, the disjunctive and conjunctive ones even lazy omega Kleene algebras. We also briefly sketch two further applications: a modal lazy Kleene algebra of commands modelling total correctness and another one that abstractly characterizes sets of trajectories as used in the description of reactive and hybrid systems.