Nested-unit Petri nets

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

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.

Recommendations

Cites work

Cited in

(11)

Describes a project that uses

Uses Software

This page was built for publication: Nested-unit Petri nets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2423743)