An Equational Axiomatization for Multi-Exit Iteration

Luca Aceto, Willem Jan Fokkink


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

X1 = P1 X2 + Q1
Xn = Pn X1 + Qn

where n is a positive integer, and the Pi and the Qi 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). 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. An expressiveness hierarchy for the family of k-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.


Full Text:


This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library