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.

Publication
University of Grenoble Alpes
Nicolas Amat
Nicolas Amat
Postdoctoral researcher

Postdoctal researcher at the IMDEA Software Institute on Presburger arithmetic.

Related