Petri Nets (PN) are extensively used as a robust formalism to model concurrent and distributed systems; however, they encounter difficulties in accurately modeling adaptive systems. To address this issue, we defined rewritable PT nets (RwPT) using Maude, a declarative language that ensures consistent rewriting logic semantics. Recently, we proposed a modular approach that employs algebraic operators to build extensive RwPT models. This methodology uses composite node labeling to maintain hierarchical organization through net rewrites and has been shown to be effective. Once stochastic parameters are integrated into the formalism, we introduce an automated procedure to derive a lumped CTMC from the quotient graph generated by a modular RwPT model. To demonstrate the effectiveness of our method, we present a fault-tolerant manufacturing system as a case study.

翻译：Petri网（PN）作为一种强大的形式化方法被广泛用于建模并发与分布式系统；然而，其在精确建模自适应系统方面存在困难。为解决这一问题，我们使用声明式语言Maude定义了可重写PT网（RwPT），该语言确保了重写逻辑语义的一致性。最近，我们提出了一种模块化方法，该方法采用代数运算符来构建大规模RwPT模型。此方法通过复合节点标记在网络重写过程中保持层次化组织，并已被证明是有效的。一旦将随机参数整合到该形式化方法中，我们引入了一种自动化流程，可从模块化RwPT模型生成的商图中推导出集总连续时间马尔可夫链。为展示我们方法的有效性，我们以一个容错制造系统作为案例研究进行说明。