A Complete Equational Axiomatization for Prefix Iteration with Silent Steps

Fokkink ((1994) Inf. Process. Lett. 52: 333{337) has recently proposed a completeequational axiomatization of strong bisimulation equivalence for MPA_delta^*(A_tau),i.e., the language obtained by extending Milner's basic CCS with prefix iteration.Prefix iteration is a variation on the original binary version of the Kleene star operationp*q obtained by restricting the first argument to be an atomic action. In thispaper, we extend Fokkink's results to a setting with the unobservable action bygiving a complete equational axiomatization of Milner's observation congruence overMPA_delta^*(A_tau ). The axiomatization is obtained by extending Fokkink's axiom systemwith two of Milner's standard tau-laws and the following three equations that describethe interplay between the silent nature of tau and prefix iteration:tau . x = tau*xa*(x+tau.y) = a*(x+tau.y + a.y)tau.(a*x) = a*(tau.a*x) .Using a technique due to Groote, we also show that the resulting axiomatization isomega-complete, i.e., complete for equality of open terms.AMS Subject Classification (1991): 68Q40, 68Q42.CR Subject Classification (1991): D.3.1, F.3.2, F.4.2.Keywords and Phrases: Minimal Process Algebra, prefix iteration, equationallogic, omega-completeness, observation congruence