A Lumped CTMC for Modular Rewritable PN

Petri Nets (PN) are extensively employed as a robust formalism for modelling concurrent and distributed systems, yet they struggle to model adaptive reconfigurable systems effectively. In response, we have developed a formalization for “rewritable” PT nets (RwPT) using Maude, a declarative language that upholds consistent rewriting logic semantics. In this work we extend a recently introduced modular approach based on composite node labelling, to incorporate stochastic parameters, and we present an automated process to obtain a lumped CTMC from the quotient graph generated by a modular RwPT model. To demonstrate the efficacy of our method, we utilize a fault-tolerant manufacturing system as a case study.