A Maude Implementation of Rewritable Petri Nets: a Feasible Model for Dynamically Reconfigurable Systems

TL;DR

This paper presents a Maude-based formalization of reconfigurable Petri Nets with inhibitor arcs, enabling modeling of dynamic system reconfiguration, demonstrated through a fault-tolerant manufacturing system example.

Contribution

It introduces a novel, efficient Maude implementation of reconfigurable Petri Nets incorporating rewriting logic, enhancing expressiveness for dynamic system modeling.

Findings

Efficient Maude formalization of reconfigurable Petri Nets.

Demonstration on a fault-tolerant manufacturing system.

Discussion of advantages and concerns of the approach.

Abstract

Petri Nets (PN) are a central, theoretically sound model for concurrent or distributed systems but, at least in their classical definition, not expressive enough to represent dynamic reconfiguration capabilities. On the other side, Rewriting Logic has proved to be a natural semantic framework for several formal models of concurrent/distributed systems. We propose a compact, efficient Maude formalization of dynamically reconfigurable PT nets (with inhibitor arcs), using as a running example the specification of a simple, fault-tolerant manufacturing system. We discuss the advantages of such a combined approach, as well as some concerns that it raises.