Coloured Petri nets (CPN) [1] are one of the major steps towards practical usage. In some sense, coloured nets are abstract in the sense that an external mechanism is assumed to generate bindings. A concrete formalism is obtained by importing a concrete annotation language and type system for arc expressions, like ML. Resig's Algebraic Petri nets [2] may represent one of the most robust and sophisticated high-level Petri net formalisms proposed to date, integrating clear mathematical semantics grounded in pure equational logic [3, 4] with intuitive operational semantics, high expressiveness, and analytical capabilities. However, it appears that there are few rigorous implementations derived from this model based on an algebraic framework: notable among these is the OBJSA formalism [5] and the associated tool (based on OBJ [6]), both unfortunately no longer supported. Other implementations of pseudo-algebraic nets have utilised various established programming languages such as Java or Python, partially compromising the original model's soundness. Translation of Algebraic Petri Nets into Conditional Rewrite Rules We present an efective implementation of algebraic Petri nets utilizing Maude [7], a purely declarative algebraic language characterized by sound rewriting logic semantics. Our definition follows the idea originally proposed in [8]. Despite Maude being proposed as a unifying framework for Petri Nets two decades ago and some recent works employing it to specify diferent classes of Petri Nets [ 9, 10, 11, 12, 13], we contend that our approach is the first systematic utilization of Maude as an efective rewriting engine for algebraic Petri Net models. Additonally, we explore the formalisation of algebraic net inscriptions as terms designed to conform to Maude's pattern-matching (modulo axioms) strategy, which ensures eficiency through the ground coherence property. Representation of Multisets In this contribution, we explore two potential approaches to cope with these modelling challenges arising from Maude's pattern-matching methodology employed in its operational semantics. The first approach is based on a classical representation of multisets as a free monoid on a set and the second one is based on a more compact representation as weighted sums. A small set of base functional modules delineate the signature of algebraic Petri nets (accessible at https://github.com/lgcapra/rewpt/blob/main/algPT/ALG-PN.maude). The resulting module hierarchy is succinct, modular, and easily extendable For both methods we define a translation procedure that generates conditional rewrite rules from the inscriptions of arcs and transitions.
Active Tokens We further demonstrate the advantage of using rewritable terms as active tokens [14, 15, 16, 17, 18], a feature naturally supported by Maude. When places are linked to system modules, tokens act as “dynamic entities” that can be rewritten. To demonstrate the advantages of this capability – natural within the context of Maude and aligning perfectly with our definition of algebraic nets – we will present an example of meta-modelling. Instead of utilizing the meta-model modules available in the Maude system, which are cumbersome and reserved for expert users (and also impact rewrite eficiency), we will showcase an application directly at the object-level. This approach is akin to the nets-within-nets concept, but more generalized: We define an algebraic net where places contain nested algebraic nets, using the same methodology described in the previous sections.
We presented an efective methodology for the comprehensive implementation of the algebraic nets schema in Maude, a purely declarative algebraic language characterized by sound rewriting logic semantics. The fundamental Maude tools for model-checking and formal verification are readily accessible; more sophisticated options (such as symbolic reachability and SMT) may be integrated at a later stage.
Our approach has the advantage that it allows rewritable terms for coloured tokens, i.e., we allow for active tokens. A special case of active case are nets-within-nets, where the tokens are Petri nets again. Our framework allows modifications to the structure and dynamic aspects can be straightforwardly integrated, such as the removal or addition of net places, changes in types linked to places, arcs that depend on parameters or markings, rewrite rules or transitions parametric in pre- and post-sets.
The author(s) have not employed any Generative AI tools. [11] M.-O. Stehr, J. Meseguer, P. C. Ölveczky, Rewriting logic as a unifying framework for Petri nets, in: H. Ehrig, G. Juhas, J. Padberg, G. Rozenberg (Eds.), Unifying Petri Nets, Lecture Notes in Computer Science (Advances in Petri Nets), Springer-Verlag, 2001. [12] K. Hofmann, H. Ehrig, T. Mossakowski, High-level nets with nets and rules as tokens, in: Application and Theory of Petri Nets and Other Models of Concurrency, volume 3536 of Lecture Notes in Computer Science, Springer-Verlag, 2005, pp. 268 – 288. [13] J. Padberg, L. Kahloul, Overview of reconfigurable Petri nets, in: R. Heckel, G. Taentzer (Eds.),
Graph Transformation, Specifications, and Nets, volume 10800, Springer-Verlag, 2018, pp. 201–222. [14] R. Valk, Object Petri nets: Using the nets-within-nets paradigm, in: J. Desel, W. Reisig, G. Rozenberg (Eds.), Advanced Course on Petri Nets 2003, volume 3098 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 819–848. [15] K. Hofmann, T. Mossakowski, Algebraic higher-order nets: Graphs and petri nets as tokens, in: Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002, volume 2755 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 253–267. [16] M. Köhler-Bußmeier, A survey on decidability results for elementary object systems, Fundamenta
Informaticae 130 (2014) 99–123. doi:10.5555/2608435.2608440. [17] M. Köhler-Bußmeier, Hornets: Nets within nets combined with net algebra, in: K. Wolf, G. Franceschinis (Eds.), Application and Theory of Petri Nets (ICATPN’2009), volume 5606 of Lecture Notes in Computer Science, Springer-Verlag, 2009, pp. 243–262. doi:10.1007/978-3-642-02424-5_15. [18] L. Capra, M. Köhler-Bußmeier, Modular rewritable Petri nets: an eficient model for dynamic distributed systems, Theoretical Computer Science 990 (2024) 114397. doi:10.1016/j.tcs.2024. 114397.