TY - JOUR
T1 - An Equational Axiomatization for Multi-exit Iteration
AU - Aceto, Luca
AU - Fokkink, Wan
PY - 1997/9/15
Y1 - 1997/9/15
N2 - 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 =def P1X2 + Q1 ⋮ Xn =def PnX1 + 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.
AB - 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 =def P1X2 + Q1 ⋮ Xn =def PnX1 + 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.
UR - http://www.scopus.com/inward/record.url?scp=0000128341&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0000128341&partnerID=8YFLogxK
U2 - 10.1006/inco.1997.2645
DO - 10.1006/inco.1997.2645
M3 - Article
AN - SCOPUS:0000128341
VL - 137
SP - 121
EP - 158
JO - Information and Computation
JF - Information and Computation
SN - 0890-5401
IS - 2
ER -