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.
KeywordsAlla Suffix Elementary Action
Unable to display preview. Download preview PDF.