A pure SPEC-inscribed PN model for reconfigurable systems

Petri Nets (PN) are a well established formal model for discrete event systems (DES). Classical PNs, even if Turing powerful, lack of features for specifying in an easy way structural changes that are likely to occur during systems' lifecycle. Many different attempts to face this issue have lead to several PN extensions, among which those matching the "nets within nets" paradigm are of particular relevance. In this paper we consolidate a recently introduced formal model for reconfigurable DES rigorously based on Reisig's SPEC-inscribed nets, that have a sound algebraic initial semantics. Although inspired by the same principles and goals as the "nets within nets" paradigm, our approach is uniform and consists of a single modelling layer. This permits consolidated analysis techniques to be exploited. A well known, first-order declarative language (OBJ) is used to inscribe nets