View article

We provide a Petri net semantics for a subset of CCSP, the union of Milner's CCS and Hoare's CSP. It assigns to each process term in the subset a labelled, one-safe place/transition net. As opposed to many other approaches to Petri net semantics, our definition is operational as it is based on Plotkin-style transition rules. These rules are inspired by work of Degano, DeNicola and Montanari, but differ in the way they model the interplay of the central concepts in CCSP: concurrency, nondeterminism and recursion. To discuss these differences, we propose criteria for a good Petri net semantics for CCSP.