Operational semantics for the Petri Box Calculus

The Petri Box Calculus (PBC), based on Milner's CCS, has been developed to provide a compositional semantics of high level programming constructs in terms of a class of Petri nets with interfaces, called Petri Boxes. In this paper we present a structural operational semantics for Box expressions which provide the syntax for the PBC. We show that the use of equations in addition to action rules leads to a uniform theory consisting essentially of …