Property-preserving transformations of elementary net systems based on morphisms (Q2163769)

The main purpose of this paper is to define a set of local abstraction/refinement transformations for elementary net (EN) systems. A local transformation acts only on a specific subnet, while the rest of the EN system remains unchanged. The authors consider EN systems with labelled transitions, where labels specify interactions with the environment. Transformation rules are presented preserving labelled transitions, while unlabelled transitions are reduced. As a result of applying these transformations, an initial EN system and a transformed EN system are related by an alpha-morphism, and their reachable markings and, especially, deadlocks are preserved. Interestingly enough, it is also shown that simple Petri net transformations, introduced earlier in the literature, also yield corresponding alpha-morphisms. In addition, the authors provide two cases of applying transformations defined in the study. For the entire collection see [Zbl 1492.68020].