Computing structural properties of symmetric nets

Structural properties of Petri Nets (PN) have an important role in the process of model validation and analysis. When considering Stochastic PNs, comprising stochastic timed and immediate transitions, structural analysis becomes a fundamental step in net-level definition of probabilistic parameters. High Level PN (HLPN) structural analysis still poses many problems and is often based on the unfolding of the HLPN model: this approach prevents the exploitation of model behavioural symmetries. A more effective alternative approach consists in providing a language, along with an associated calculus, making it possible to derive expressions defining structural relations among node instances of a HLPN model in a symbolic and parametric form: this has been proposed in the literature for Symmetric Nets (SN). The goal of the present paper is to summarize the language defined to express SNs’ structural relations and to formalize the derivation of a basic set of such relations; in particular the algorithms to compute the Structural Mutual Exclusion relation and the symmetric and transitive closure of Structural Conflict are an original contribution of this paper. Examples of applications are also included. The algorithms required to support the calculus for symbolic structural relations computation have been recently completed and implemented in a tool called SNexpression.