D.C.: Automatic abstraction refinement for Petri nets verification

Abstract — Model Checking has emerged as a promising and powerful approach to analyze Petri nets automatically, but a main challenge is the state explosion problem. To obtain an efficient state space, we implement a series of formalisms based on Petri nets to achieve automatically predicate abstraction and refinement via new predicate discovery. However, the complicated predicates would slow down the abstraction refinement process. A novel feature of our approach is minimizing the support of predicates, via diagnosing the failure reasons of transitions and projecting places on predicates to eliminate the dumb variables. In addition, a demonstrative example shows that our techniques could work efficiently on Petri nets. I