Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modular Stochastic Rewritable Petri Nets

Lorenzo Capra

TL;DR

The paper addresses the challenge of modeling adaptive distributed systems with dynamic changes by proposing modular Rewritable Petri nets (RwPT) implemented in Maude. It introduces modular algebraic operators and composite labeling to reveal hierarchical symmetries and to derive a lumped CTMC from the quotient graph once stochastic parameters are incorporated. A semi-automatic workflow aggregates quotient transitions into a lumped generator, and experimental results on a fault-tolerant production-line model demonstrate substantial state-space reductions and reliability improvements as the replication level grows. This work enables scalable, verifiable analysis of large, symmetry-rich adaptive systems and points toward integration with graphical editors and generalization to arbitrary Maude specifications.

Abstract

Petri Nets (PN) are widely used for modeling concurrent and distributed systems, but face challenges in modeling adaptive systems. To address this, we have formalized "rewritable" PT nets (RwPT) using Maude, a declarative language with sound rewriting logic semantics. Recently, we introduced a modular approach that utilizes algebraic operators to construct large RwPT models. This technique employs composite node labeling to outline symmetries in hierarchical organization, preserved through net rewrites. Once stochastic parameters are added to the formalism, we present an automated process to derive a lumped CTMC from the quotient graph generated by an RwPT.

Modular Stochastic Rewritable Petri Nets

TL;DR

The paper addresses the challenge of modeling adaptive distributed systems with dynamic changes by proposing modular Rewritable Petri nets (RwPT) implemented in Maude. It introduces modular algebraic operators and composite labeling to reveal hierarchical symmetries and to derive a lumped CTMC from the quotient graph once stochastic parameters are incorporated. A semi-automatic workflow aggregates quotient transitions into a lumped generator, and experimental results on a fault-tolerant production-line model demonstrate substantial state-space reductions and reliability improvements as the replication level grows. This work enables scalable, verifiable analysis of large, symmetry-rich adaptive systems and points toward integration with graphical editors and generalization to arbitrary Maude specifications.

Abstract

Petri Nets (PN) are widely used for modeling concurrent and distributed systems, but face challenges in modeling adaptive systems. To address this, we have formalized "rewritable" PT nets (RwPT) using Maude, a declarative language with sound rewriting logic semantics. Recently, we introduced a modular approach that utilizes algebraic operators to construct large RwPT models. This technique employs composite node labeling to outline symmetries in hierarchical organization, preserved through net rewrites. Once stochastic parameters are added to the formalism, we present an automated process to derive a lumped CTMC from the quotient graph generated by an RwPT.

Paper Structure

This paper contains 9 sections, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. (Stochastic) PT nets, Maude, and demonstrative example
  3. Maude
  4. Running example: fault-tolerant production line
  5. Modular Rewritable Stochastic PN: Symmetries and Lumpability
  6. Modularity, symmetries, and lumpability
  7. Getting the Lumped CTMC generator from RwSPT
  8. Experimental Evidence
  9. Conclusion and Future Work

Figures (2)

  • Figure 1: One of the possible paths of the Gracefully Degrading Production System.
  • Figure 2: System Reliability.

Theorems & Definitions (1)

  • Definition 3.1: Symmetric Labeling