In: Gianfranco Ciardo, Philippe Darondeau (Eds.): Lecture Notes in Computer Science, Vol. 3536: Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005., pages 168-187. Springer Verlag, June 2005.
Abstract: Well-formed Nets WN structural analysis techniques allow to study interesting system properties without requiring the state space generation. In order to avoid the net unfolding, which would reduce significantly the effectiveness of the analysis, a symbolic calculus allowing to directly work on the WN colour structure is needed. The algorithms for high level Petri nets structural analysis most often require a common subset of operators on symbols annotating the net elements, in particular the arc functions. These operators are the function difference, the function transpose and the function composition. This paper focuses on the first two, it introduces a language to denote structural relations in WN and proves that it is actually closed under the difference and transpose.