A complete equational axiomatization for BPA-δε with prefix iteration

Abstract

Prex iteration x is added to Basic Process Algebra with deadlock and empty process. We present a nite equational axiomatization for this process algebra, and we prove that this axiomatization is complete with respect to strong bisimulation equivalence. This result is a mild generalization of a similar result in the setting of basic CCS in Fokkink (1994b). To obtain this completeness result, we set up a rewrite system, based on the axioms. In order to prove that this rewrite system is terminating modulo AC of the +, we generalize a termination theorem from Zantema and Geser (1994) to the setting of rewriting modulo equations. Finally, we show that bisimilar normal forms are syntactically equal modulo AC of the +.