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, and yields simple iterative behaviours that
can be equationally characterized by means of finite collections of axioms.
In this paper, we present axiomatic characterizations for a significant
fragment of the notions of equivalence and preorder in van Glabbeek's
linear-time/branching-time spectrum over Milner's basic CCS extended with
prefix iteration. More precisely, we consider ready simulation, simulation,
readiness, trace and language semantics, and provide complete (in)equational
axiomatizations for each of these notions over BCCS with prefix iteration.
All of the axiom systems we present are finite, if so is the set of atomic
actions under consideration
Available as PostScript, PDF, DVI.