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.

In Proceedings ICLP 2024, arXiv:2502.08453