Talk title: How to Use Polyhedral Reduction for the Verification of Petri nets.
Abstract: I will describe a new concept, called polyhedral reduction, that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. This approach relies on a state space abstraction which involves sets of linear arithmetic constraints between the marking of places.
We have been using polyhedral reductions to solve several problems. I will consider three of them. First, how to use reductions to efficiently compute the number of reachable markings of a net. Then how to use polyhedral reduction in combination with a SMT-based model checker. Finally, I will define a new data-structure, called Token Flow Graph (TFG), that captures the particular structure of constraints that we generate with our approach. I will show how we can leverage TFGs to efficiently compute the concurrency relation of a net, that is all pairs of places that can be marked together in some reachable marking.
