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

  • Lorenzo Capra,
  • Massimiliano De Pierro,
  • Giuliana Franceschinis

摘要

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.