Preservation of liveness in hierarchical petri nets
Sadatoshi Kumagai, Shinzo Kodama, Kohkichi Tsuji, Youichi Nakamura · Electronics and Communications in Japan (Part III Fundamental Electronic Science) · 1990
Abstract For large‐scale systems for discrete events such as FA, OA and sequence control systems, it is desirable to establish a systematic design methodology. It is expected that a systematic design methodology for systems can be obtained using a Petri net model (a powerful model for discrete event systems) for system specification, analysis and verification. Generally, in the top‐down design of a large‐scale system, we begin with a rough design for the system and apply successive refinements. In the Petri net model, a hierarchical representation is considered such that in a refinement step, one of the elements in the net is replaced by a subnet which represents its behavior in more detail. This paper considers some questions regarding this hierarchical representation of Petri nets, such as whether properties such as liveness and safeness of nets are preserved by the refinement. In particular, we consider simultaneous refinement of parallel transitions to derive several sufficient conditions concerning preservation of properties of the net, and represent these as conditions on subnets which are to replace blocks in the parent net.