On the Completeness of the Equations for the Kleene Star in Bisimulation

Abstract

A classical result from Redko says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema showed that there does exist a complete finite equational axiom atization for the Kleene star up to strong bisimulation equivalence. Their proof is based on a sophisticated term rewriting analysis. In this paper we present a much simpler and shorter completeness proof. Furthermore, we show that the three equations for the Kleene star are all essential for this completeness result.