Abstract:
We study equational axiomatizations of bisimulation equivalence
for the language obtained by extending Milner's basic CCS with string
iteration. String iteration is a variation on the original binary version of
the Kleene star operation 
obtained by restricting the first argument
to be a non-empty sequence of atomic actions. We show that, for every
positive integer k, bisimulation equivalence over the set of processes in
this language with loops of length at most k is finitely axiomatizable. We
also offer a countably infinite equational theory that completely axiomatizes
bisimulation equivalence over the whole language. We prove that this result
cannot be improved upon by showing that no finite equational axiomatization
of bisimulation equivalence over basic CCS with string iteration can exist,
unless the set of actions is empty.
Available as PostScript, PDF, DVI.