An Equational Axiomatization for Multi-exit Iteration

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 formX1 = def P1X2+Q1 ⋮Xn = def PnX1+Qn, wherenis a positive integer and thePi and theQi 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 ofk-exit iteration operators proposed by Bergstra, Bethke, and Ponse is also offered.

Authors

• Luca Aceto
• Wan Fokkink

Keywords

No keywords are indexed for this paper.