Avoiding state explosion in a class of Petri nets

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 of places p marked in superposition, and denotes that each p in ⊻ M is marked individually, yet it is uncertain if all p in ⊻ M are marked together. In other words, superposition loses which p in ⊻ M is marked by conflicting transitions, which are revealed by the transition firing history. The firing history of p ∈ ⊻ M is also defined by a set, h ( p ) , and denotes transition firings participated in p ∈ ⊻ 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 . Hence, ⊻ M is not coverable as a whole, if there are conflicting firings in 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.