37.
Equational axiomatizations for prefix iteration with silent steps
L. Aceto (U. Aalborg), W.J. Fokkink (U. Utrecht), R.J. van
Glabbeek (Stanford) & A. Ingólfsdóttir (U. Aalborg)
November 1995
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, eta-congruence, delay
congruence and weak congruence. The completeness proofs for eta-,
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 omega-completeness of the
axiomatizations is obtained as well as their completeness for closed
terms.
KEYWORDS: Concurrency, process algebra, basic CCS,
prefix iteration, branching bisimulation,
eta-bisimulation, delay bisimulation, weak bisimulation,
equational logic, complete axiomatizations.