© 1994 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Basic Process Algebra with Iteration: Completeness of its Equational Axioms

1 CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands, 2 Utrecht University, Padualaan 14, 3508 TB Utrecht, The Netherlands
Bergstra, Bethke and Ponse proposed an axiomatization for Basic Process Algebra extended with (binary) iteration. In this paper, we prove that this axiomatization is complete with respect to strong bisimulation equivalence. To obtain this result, we will set up a term rewriting system, based on the axioms, and prove that this term rewriting system is terminating, and that bisimilar normal forms are syntactically equal modulo commutativity and associativity of the +.
* CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands
Utrecht University, Padualaan 14, 3508 TB Utrecht, The Netherlands