Affiliations: Centro de Investigaciones en Nuevas Tecnologías Informáticas, Universidad Privada Boliviana, La Paz, Bolivia. [email protected] | Centre Universitaire d'Informatique, University of Geneva, 7 route de Drize, 1227 Carouge, Switzerland. [email protected]
Note: [] This work was partially supported by the COMEDIA project funded by the Hasler foundation, project #2107. Also works: Centre Universitaire d'Informatique, University of Geneva Address for correspondence: Centro de Investigaciones en Nuevas Tecnologías Informáticas, Universidad Privada Boliviana, La Paz, Bolivia
Abstract: Modularity is a mandatory principle to apply Petri nets to real world-sized systems. Modular extensions of Petri nets allow to create complex models by combining smaller entities. They facilitate the modeling and verification of large systems by applying a divide and conquer approach and promoting reuse. Modularity includes a wide range of notions such as encapsulation, hierarchy and instantiation. Over the years, Petri nets have been extended to include these mechanisms in many different ways. The heterogeneity of such extensions and their definitions makes it difficult to reason about their common features at a general level. We propose in this article an approach to standardize the semantics of modular Petri nets formalisms, with the objective of gathering even the most complex modular features from the literature. This is achieved with a new Petri nets formalism, called the LLAMAS Language for Advanced Modular Algebraic Nets (LLAMAS). We focus principally on the composition mechanism of LLAMAS, while introducing the rest of the language with an example. The composition mechanism is introduced both informally and with formal definitions. Our approach has two positive outcomes. First, the definition of new formalisms is facilitated, by providing common ground for the definition of their semantics. Second, it is possible to reason at a general level on the most advanced verification techniques, such as the recent advances in the domain of decision diagrams.
Keywords: System design and verification, Modularity, High-Level Petri nets, Standardization, Composition Mechanism, LLAMAS
