Abstraction-Based Incremental Inductive Coverability for Petri Nets

摘要

We present a novel approach to check the coverability problem of Petri nets which is based on a tight integration of IC3 with place-merge abstraction. Place-merge abstraction can reduce the dimensionality of state spaces by trying to merge some places that may be not critical for proving the property. In this scenario, IC3 runs only on abstract Petri nets with lower dimensionality. When the current abstraction allows for a spurious counterexample, it is refined by splitting candidate abstract places. Furthermore, this can be done in a completely incremental way without discarding results found in previous abstractions. The experimental evaluation on the standard Petri net benchmarks shows the effectiveness and competitiveness of our approach.