The Box Algebra —; A Model of Nets and Process Expressions

The paper outlines a Petri net as well as a structural operational semantics for an algebra of process expressions. It specifically addresses this problem for the box algebra, a model of concurrent computation which combines Petri nets and standard process algebras. The paper proceeds in arguably the most general setting. For it allows infinite operators, and recursive definitions which can be unguarded and involve infinitely many recursion variables. The main result is that it is possible to obtain a framework where process expressions can be given two, entirely consistent, kinds of semantics, one based on Petri nets, the other on SOS rules.