Model checking using net unfoldings

AbstractMcMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. The new algorithm is shown to be polynomial in the size of the net for 1-safe conflict-free Petri nets, while the algorithms of the literature require exponential time