A Complete Axiomatization for Prefix Iteration in Branching Bisimulation

This paper studies the interaction of prefix iteration ¯ x with the silent step ø in the setting of branching bisimulation. That is, we present a finite equational axiomatization for Basic Process Algebra with deadlock, empty process and the silent step, extended with prefix iteration, and prove that this axiomatization is complete with respect to rooted branching bisimulation equivalence. 1 Introduction Kleene (1956) defined a binary operator in the context of finite automata, called Kleene star or iteration. Intuitively, the expression p q yields a solution for the recursive equation X = p \Delta X + q. In other words, p q can choose to execute either p, after which it evolves into p q again, or q, after which it terminates. This paper considers the prefix counterpart ¯ x of iteration in process algebra, where the argument ¯ ranges over the set of constants. Our setting is Basic Process Algebra (BPA) from Bergstra and Klop (1984), with the deadlock ffi and the em..