Automated Proof of Polyhedral Abstraction for Petri Nets

Abstract

In this talk, I propose an automated procedure for proving polyhedral abstractions for Petri nets. Polyhedral abstraction is a new type of state-space equivalence based on the use of linear integer constraints.

The approach relies on an encoding into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets that have Presburger-definable reachability sets.

This talk will also be an opportunity to present new results on the use of polyhedral abstraction for verifying reachability properties. In particular, I will introduce a new variable elimination procedure that can project a property, about an initial Petri net, into an equivalent formula that only refers to the reduced version of this net.