Petri Net Semantics
Petri nets have long been provided with different kinds of coherent semantics (e.g., [90, 83, 15]); in particular, concurrency semantics, such as trace , step , process [48, 5], and partial word semantics [49, 94, 100]. Therefore, a natural idea to get a fully fledged concurrency semantics for a process expression is to associate with it a Petri net. This technique has already been exploited for various process algebras [13, 19, 47, 44, 84, 95], but in many cases only a fragment of a model has been successfully translated. Here we shall show how to accomplish this task not only in full generality, but also entirely compositionally, thanks to a careful choice of the operators and very general mechanisms introduced to combine nets. In order to obtain a compositional translation of PBC expressions into Petri nets, we shall define for the latter operators corresponding to those introduced for the process algebra; the translation itself will then be a homomorphism. This chapter shows how to do this for the finite PBC and for iteration; in Chap. 5, we will turn to the translation of recursion variables. To avoid (or at least minimise) the risk of having to redesign a large part of the theory whenever a small change needs to be made to the algebra (for example, due to the introduction of a new operator), we shall develop a general mechanism to define net operators based on an auxiliary notion of net refinement.
KeywordsProcess Algebra Linkage Graph Reachable Marking Entry Place Exit Place
Unable to display preview. Download preview PDF.