Nested-unit Petri nets (Q2423743)

Many concurrent systems can be thought of as consisting of subsystems, which themselves may have sub-subsystems, and so on. This study addresses the problem of exploiting this kind of hierarchies in the verification of systems. Its starting points are Petri nets that have no hierarchy, and process algebras that naturally express hierarchy. The study organizes the Petri net places into a tree-like structure of units, where a unit consists of zero or more places and zero or more sub-units. This construct is unusual in that Petri net transitions are ignored. Indeed, the hierarchy has no semantic significance. Altogether, the theoretical results of the study seem shallow. The value of the formalism is that it can be used to improve verification tools by facilitating the packing of states into a smaller number of bits. From the practical perspective the formalism has been very successful. The unusually extensive bibliography focuses on concurrency formalisms from the verification point of view, and related topics.