Avoiding state explosion in a class of Petri nets

• A novel tool, superposition chain, is proposed to avoid state explosion.
• This can be used in some classes of Petri nets.
• The future research direction is to incorporate the idea into the acyclic safe PNs.
• As the reachability problem of an acyclic safe PN is NP-complete, the effect would be immense.
• A long way has been passed in this direction.

This paper introduces leveled Petri nets (PNs), and proposes a novel PN analysis tool, the superposition chain (SC), to avoid state explosion. It also introduces underlying tools—superposition and the leveled token game—to tackle the P vs NP   problem, a well known problem in CS/AI community. The leveled token game, defined over a leveled PN, generates the SC of the PN. The leveling is based on the transitions such that a transition and all its input places are in the same level, and that there is no causality among transitions in a level, while transitions across levels indicate causality. The enabling rule is extended by superposition and firing history. Superposition of markings is defined by a set ⊻M⊻M of places p marked in superposition, and denotes that each p   in ⊻M⊻M is marked individually, yet it is uncertain if all p   in ⊻M⊻M are marked together. In other words, superposition loses which p   in ⊻M⊻M is marked by conflicting transitions, which are revealed by the transition firing history. The firing history of p∈⊻Mp∈⊻M is also defined by a set, h(p)h(p), and denotes transition firings participated in p∈⊻Mp∈⊻M, yet does not enumerate their firing sequences to avoid the state explosion. Then, the compound firing history defined over ⊻M,h(⊻M), is used to reveal all conflicting transitions participated in ⊻M⊻M. Hence, ⊻M⊻M is not coverable as a whole, if there are conflicting firings in h(⊻M)h(⊻M), which is used for the transition enabling. Consequently, the SC, generated by the leveled token game, specifies the PN behavior, as a reachability tree, generated by the (conventional) token game, also specifies a PN behavior.