A complete equational axiomatization for MPA with string iteration

We study equational axiomatizations of bisimulation equivalence for the lan guage obtained by extending Milner's basic CCS with string iteration. Strin g iteration is a variation on the original binary version of the Kleene sta r operation p*q obtained by restricting the first argument to be a non-empt y sequence of atomic actions. We show that, for every positive integer k, b isimulation equivalence over the set of processes in this language with loo ps of length at most k is finitely axiomatizable, provided that the set of actions is finite. We also offer an infinite equational theory that complet ely axiomatizes bisimulation equivalence over the whole language. We prove that this result cannot be improved upon by showing that no finite equation al axiomatization of bisimulation equivalence over basic CCS with string it eration can exist, unless the set of actions is empty. (C) 1999-Elsevier Sc ience B.V. All rights reserved.