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

A classical result from Redko [14] says that there does not exist a complete finite equational axiomatization for the Kleene star modulo trace equivalence. Fokkink and Zantema [9] showed that there does exist a complete finite equational axiomatization 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. 1 Introduction Kleene [10] defined a binary operator x y in the context of finite automata, which denotes the iterate of x and y. Intuitively, the expression x y can choose to execute either x, after which it evolves into x y again, or y, after which it terminates. An advantage of the Kleene star is that on the one hand it can express recursion, but that on the other hand one can capture this operator in equational laws. H..