Master thesis: A New Approach for the Symbolic Model Checking of Petri nets

Abstract

The Vertics team at LAAS-CNRS has been developing a new approach for the symbolic model checking for years, i.e., a method to represent exactly the state-space of a system without enumerating it exhaustively. This study’s originality consists in the verification of properties on a Petri net $N$ from a reduced net $N’$, as well as a system of linear equations $E$ linking these two nets. This study focuses on the adaptation of SAT methods such as BMC and PDR into SMT methods to verify efficiently different properties on non-safe Petri nets by taking advantage of these nets reductions. After defining the reductions used, this study defines a new notion of equivalence to prove the soundness of these reduction rules. This study is also interested in the decomposition of Petri nets into sub-net called NUPNs, introduced by the Convecs team from INRIA. This decomposition requires the computation of concurrency relations between the places composing the net. This work proposes a promising method to answer this question on large nets by treating the reduction equations.