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 and COSMOS, then a toolset has become available for structural analysis of SN: SNexpression. 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.
SNexpression: A New Component for SN Matrix-Based Structural Analysis / L. Capra, M. De Pierro, G. Franceschinis (LECTURE NOTES IN COMPUTER SCIENCE). - In: Formal Techniques for Distributed Objects, Components, and Systems / [a cura di] C. Ferreira, C.A. Mezzina. - [s.l] : Springer Cham, 2025 Jun. - ISBN 9783031954962. - pp. 193-201 (( Intervento presentato al 45. convegno 45th IFIP WG 6.1 International Conference, FORTE 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025 tenutosi a Lille nel 2025 [10.1007/978-3-031-95497-9_12].
SNexpression: A New Component for SN Matrix-Based Structural Analysis
L. Capra
Primo
Membro del Collaboration Group
;
2025
Abstract
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 and COSMOS, then a toolset has become available for structural analysis of SN: SNexpression. 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.| File | Dimensione | Formato | |
|---|---|---|---|
|
Forte25_CR (1).pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Licenza:
Nessuna licenza
Dimensione
848.54 kB
Formato
Adobe PDF
|
848.54 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.




