EnPAC: Petri Net Model Checking for Linear Temporal Logic

Zhijun Ding, Cong He, Shuo Li

State generation and exploration (counterexample search) are two cores of explicit-state Petri net model checking for linear temporal logic (LTL). Traditional state generation upda…