A class of composable high level Petri nets

In this paper a high-level Petri net model called hi-nets (for multilabeled nets) is developed. A distinctive feature of this model is that it allows not only vertical unfolding, as do most other high-level net models, but also horizontal composition - in particular, synchronisation - in a manner similar to process algebras such as CCS. This turns the set of hi-nets into a domain whose composition operations satisfy various algebraic properties. The operations are shown to be consistent with unfolding in the sense that the unfolding of a composite high-level net is the composition of the unfoldings of its components. A companion paper shows how this algebra can be used to define the semantics of a concurrent programming language compositionally.