What is polyhedral reduction? ...and how we use it to accelerate the verification of reachability problems for Petri nets.

Abstract

In this talk, we present a new framework, called polyhedral abstraction, for checking safety properties on Petri nets, that is checking if some reachable state satisfy a property of interest. This is an important and difficult problem with many practical applications: obviously for the formal verification of concurrent systems, but also for the study of diverse types of protocols (such as biological or business processes), the verification of software systems, the analysis of infinite state systems, etc. In this framework, we propose a novel approach that involves reducing the size of the model under study. The key advancement lies in the computation of a set of linear equations, which permits to trace back the reachable states of the original net based on those of the reduced net. We also introduce a new graph structure called Token Flow Graph, specifically designed to capture our reduction equations, for which we address reachability problems by playing a “token game” on the graph. To conclude the presentation, we provide a live demonstration of the tool SMPT, an SMT-based model checker that actively participates in the Model Checking Contest. An exciting feature of the tool is its ability to generate certificates of invariance.