Deciding the Deadlock and Livelock in a Petri Net with a Target Marking Based on Its Basic Unfolding

Petri nets are widely used to model and analyse concurrent systems. It is an important study to check the deadlock and/or livelock in Petri nets. These checks are generally carried out by the reachability graph technique and thus the state explosion problem is a big obstacle to this technique. The unfolding technique can effectively avoid/alleviate the state explosion problem, especially for those Petri nets that have many concurrent actions. This paper considers the deadlock and livelock problem in a Petri net with a target state. We propose the notion of basic unfolding. Based on basic unfolding, we present a necessary and sufficient condition to decide whether a Petri net is both deadlock-free and livelock-free.