A uniform approach to true-concurrency and interleaving semantics for Petri nets

摘要

This payer continues a research on universal contexts and semantics for Petri nets starred by Nielsen, Priese and Sassone (1995). We consider generalized labelled Petri nets N where some transitions and places are distinguished as public. They form the interface of N that may communicate with a Petri net context. An elementary calculus, epsilon, is introduced in which one can construct any Petri net with an interface from trivial constants (single places, single transitions) by drawing arcs, adding tokens, and hiding public places and transitions. We prove the existence of a universal contest U such that two Petri nets behave the same in any context if their behaviour is equal in the universal context. Let B(UN) be the behaviour of N embedded in its universal context, where B may be the interleaving language, step-language, or true-concurrent pomset-language. In any of these cases, B(UN) tin contrast to B(N)) turns out to be a compositional semantics of N with respect to the algebra I. In addition, the interleaving- and step-semantics are just special cases of the true-concurrency pomset-semantics. (C) 1998-Elsevier Science B.V. All rights reserved. References: 23