A completeness theorem for nondeterministic kleene algebras

Abstract

A generalization of Kleene Algebras (structures with +·*, 0 and 1 operators) is considered to take into account possible nondeterminism expressed by the + operator. It is shown that essentially the same complete axiomatization of Salomaa is obtained except for the elimination of the distribution P·(Q + R) = P·Q + P·R and the idempotence law P + P = P. The main result is that an algebra obtained from a suitable category of labelled trees plays the same role as the algebra of regular events. The algebraic semantics and the axiomatization are then extended by adding Ω and ∥ operator, and the whole set of laws is used as a touchstone for starting a discussion over the laws for deadlock, termination and divergence proposed for models of concurrent systems.