An Equational Axiomatization for Multi-Exit Iteration

Luca Aceto
Wan J. Fokkink

June 1996


This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of recursion equations of the form


where n is a positive integer, and the tex2html_wrap_inline23 and the tex2html_wrap_inline25 are process terms. The addition of multi-exit iteration to BPA yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star (BPA tex2html_wrap_inline27 ). As a consequence, the proof of completeness of the proposed equational axiomatization for this language, although standard in its general structure, is much more involved than that for BPA tex2html_wrap_inline27 . An expressiveness hierarchy for the family of k-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.