Operational and denotational semantics for the box algebra

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.