What is Polyhedral Reduction? ... and how we use it to accelerate the verification of reachability problems

Abstract

We define a method that takes advantage of structural reductions to accelerate the verification of reachability problems. We prove the correctness of this method using a new notion of equivalence between nets that we call polyhedral abstraction. Our approach has been implemented in a tool, named SMPT, that provides SMT-based methods. We present an adaptation of the Property Directed Reachability (PDR) decision procedure that permits to generate some certificate of invariance for generalised nets. We also propose a new method for accelerating the computation of the concurrency relation, that is all pairs of places in a Petri net that can be marked together. Our approach relies on the same state-space abstraction, that involves a mix between structural reductions and linear algebra, but this time using a new data-structure that is specifically designed for our task.