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.

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

De Pierro M.
;
2025-01-01

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 [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.
2025
FORTE 2025 - 45th International Conference on Formal Techniques for Distributed Objects, Components, and Systems
Lille, France
June 16–20, 2025
Formal Techniques for Distributed Objects, Components, and Systems
SPRINGER INTERNATIONAL PUBLISHING AG
15732
193
201
9783031954962
9783031954979
Symmetric Nets; Structural analysis; Matrix calculus
Capra L.; De Pierro M.; Franceschinis G.
File in questo prodotto:
File Dimensione Formato  
Forte25_CR.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 851.05 kB
Formato Adobe PDF
851.05 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/2120853
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact