Symbolic and Structural Model-Checking

Yann Thierry-Mieg (1)

1 MoVe - Modélisation et Vérification

Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of techniques that stay in complexity proportional to the size of the net structure rather than to the state-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper.

Mots clés: Petri nets; Structural Reduction; Model-checking; SMT constraints

Domaines: Informatique et langage [cs.CL]; Performance et fiabilité [cs.PF]; Théorie et langage formel [cs.FL]

Yann Thierry-Mieg. Symbolic and Structural Model-Checking. Fundamenta Informaticae, 2022, 183 (3-4), pp.319-342. ⟨10.3233/FI-2021-2090⟩. ⟨hal-03147423v2⟩