Modular Stochastic Rewritable Petri Nets

TL;DR

This paper introduces a modular, rewritable Petri Net formalism with stochastic parameters, enabling automated derivation of continuous-time Markov chains from hierarchical models for better analysis of adaptive concurrent systems.

Contribution

It formalizes rewritable Petri Nets using Maude, develops a modular approach with algebraic operators, and provides an automated method to derive CTMCs from hierarchical stochastic models.

Findings

Formalization of rewritable Petri Nets in Maude.

Development of a modular construction technique.

Automated derivation of CTMCs from hierarchical models.

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.