SNexpression: A New Component for SN Matrix-Based Structural Analysis

Symmetric nets (SN), including their stochastic extension (SSN), are a type of high-level Petri net (HLPN) known for their structured syntax, which aids in efficient analysis. Their dynamics is described by a quotient state-transition system (SRG) linked to a lumped Markov chain. State-space analysis and stochastic model checking are supported by tools like GreatSPN [4, 7] and COSMOS [3, 9], then a toolset has become available for structural analysis of SN: SNexpression [2, 10]. This framework is based on algebraic calculi to derive properties in a symbolic manner. The paper presents a novel component for operating at the net level by manipulating matrices of structural expressions directly. This approach enables a coherent definition of stochastic parameters in SSNs with several transition priority levels and extends the analysis capabilities by identifying independent classes of transition instances. The paper illustrates the new SNexpression functionalities of matrix structural calculi on two examples.