Automatic abstraction refinement for Petri nets verification

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