Since 2018, we have been developing a novel approach to symbolic model checking for Petri nets, which we call polyhedral reduction. By “symbolic”, we mean a method that allows the exact representation of a system’s entire state space without having to enumerate each state individually in an exhaustive way.
The core idea behind polyhedral reductions is to combine structural reductions, a technique that simplify a net by merging or removing places, with an abstraction of sets of states using system of linear equations (called reduction equations). These equations capture the relationship between the original net and its reduced version, allowing us to reconstruct the reachable markings of the original net from the reduced one.
You can look at the following poster for a quick, gentle introduction:
Or you can refer to the slides from a recent invited talk for a more general presentation of our technique and how it is applied in our verification tools.
Reference#
