  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.
