TY - JOUR
T1 - Axiomatizing Prefix Iteration with Silent Steps
AU - Aceto, Luca
AU - Van Glabbeek, Rob
AU - Fokkink, Wan
AU - Ingólfsdóttir, Anna
PY - 1996/5/25
Y1 - 1996/5/25
N2 - Prefix iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz., branching congruence, η-congruence, delay congruence, and weak congruence. The completeness proofs for η-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i.e., terms that may contain process variables. As a by-product, the ω-completeness of the axiomatizations is obtained, as well as their completeness for closed terms.
AB - Prefix iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz., branching congruence, η-congruence, delay congruence, and weak congruence. The completeness proofs for η-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i.e., terms that may contain process variables. As a by-product, the ω-completeness of the axiomatizations is obtained, as well as their completeness for closed terms.
UR - http://www.scopus.com/inward/record.url?scp=0002384663&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0002384663&partnerID=8YFLogxK
U2 - 10.1006/inco.1996.0047
DO - 10.1006/inco.1996.0047
M3 - Article
AN - SCOPUS:0002384663
VL - 127
SP - 26
EP - 40
JO - Information and Computation
JF - Information and Computation
SN - 0890-5401
IS - 1
ER -