Reference:

J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994.

Abstract:

McMillan (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.

Suggested BibTeX entry:

@article{Esp94b,
    author = {J. Esparza},
    journal = {Science of Computer Programming},
    pages = {151--195},
    title = {Model checking using net unfoldings},
    volume = {23},
    year = {1994}
}