A SUBCLASS OF PETRI NETS WHERE LIVENESS IS PRESERVED UNDER THE EARLIEST FIRING RULE

The Petri net is a powerful tool for modeling, analysis, verification, and evaluation of discrete event systems, and liveness is one of the most important analytical properties of the Petri net. On the other hand, introduction of the earliest firing rule gives an extended class of the net that is useful from both theoretical and applicative viewpoints. This paper clarifies a relation between 'normal' liveness of Petri nets and liveness of the net under 'the earliest firing rule.' POC nets, a subclass of Petri nets where normal liveness is a sufficient condition for liveness under the earliest firing rule are proposed. Then conditions for necessity are investigated, considering the two rules for multiple firing of a single transition, i.e., single servers and infinite servers. This provides a subclass where the two forementioned livenesses are equivalent to each other. Finally, computational complexity for liveness problem is considered.