Abstract:
Prefix iteration is a variation on the original binary version
of the Kleene star operation 
, 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 overbasic 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 byproduct, the
-completeness of the axiomatizations is obtained as well as their
completeness for closed terms.
Available as PostScript, PDF, DVI.