Exploiting local persistency for reduced state-space generation

This paper deals with two partial order techniques for Petri nets (PN in short): persistent sets and step graphs. These techniques aim to reduce the width and the depth of the marking graphs of PN, respectively, while preserving their deadlocks. To achieve more reductions while preserving the deadlocks of PN, this paper revisits the definition of persistent sets and establishes some weaker practical sufficient conditions. It also proposes a combination of persistent sets with steps as a sort of Cartesian product of persistent sets. This combination provides a means of better controlling the length and the number of steps, while still preserving deadlocks.