This paper describes general theory underpinning the operational semantics
and the denotational Petri net semantics of the box algebra including recur
sion. For the operational semantics, inductive rules for process expression
s are given. For the net semantics, a general mechanism of refinement and r
elabelling is introduced, using which the connectives of the algebra are de
fined. The paper also describes a denotational approach to the Petri net se
mantics of recursive expressions. A domain of nets is identified such that
the solution of a given recursive equation can be found by fixpoint approxi
mation from some suitable starting point. The consistency of the two semant
ics is demonstrated. The theory is generic for a wide class of algebraic op
erators and synchronisation schemes. (C) 1999-Elsevier Science B.V. All rig
hts reserved.