Complexity Results for 1-safe Nets

We study the complexity of several standard problems for 1-safe Petri nets and some of its subclasses. We prove that reachability, liveness, and deadlock are all PSPACE-complete for 1-safe nets. We also prove that deadlock is NP-complete for free-choice nets and for 1-safe free-choice nets. Finally, we prove that for arbitrary Petri nets, deadlock is equivalent to reachability and liveness. 1 

• Type: Conference
• Year: 1993
• Where: FSTTCS
• Authors: Allan Cheng, Javier Esparza, Jens Palsberg
• Keywords: 1-safe Petri Nets, Free-choice Nets, FSTTCS 1993, Petri Nets, Software Engineering