TY - JOUR AU - Aceto, Luca AU - Fokkink, Willem Jan PY - 1996/01/22 Y2 - 2024/03/28 TI - An Equational Axiomatization for Multi-Exit Iteration JF - BRICS Report Series JA - BRICS VL - 3 IS - 22 SE - Articles DO - 10.7146/brics.v3i22.19985 UR - https://tidsskrift.dk/brics/article/view/19985 SP - AB - <p>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<br />of systems of recursion equations of the form</p><p>X1 = P1 X2 + Q1<br />...<br />Xn = Pn X1 + Qn</p><p>where n is a positive integer, and the Pi and the Qi are process terms. The addition<br />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<br />consequence, the proof of completeness of the proposed equational axiomatization<br />for this language, although standard in its general structure, is much more involved<br />than that for BPA. An expressiveness hierarchy for the family of k-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.</p><p> </p> ER -