AXIOMATIZING PREFIX ITERATION WITH SILENT STEPS

Prefix iteration is a variation on the original binary version of the Kleene star operation PQ, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silen t steps is studied in the setting of Milner's basic CCS. Complete equa tional axiomatizations are given for four notions of behavioural congr uence over basic CCS with prefix iteration, viz., branching congruence , eta-congruence, delay congruence, and weak congruence. The completen ess proofs for eta-, delay, and weak congruence are obtained by reduct ion to the completeness theorem for branching congruence. It is also a rgued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a c onsiderable simplification with respect to the only direct proof prese nted in the literature. The preliminaries and the completeness proofs focus on open terms, i.e., terms that may contain process variables. A s a by-product, the omega-completeness of the axiomatizations is obtai ned, as well as their completeness for closed terms. (C) 1996 Academic Press, Inc.