Yann Thierry-Mieg - Symbolic and Structural Model-Checking

fi:7334 - Fundamenta Informaticae, December 23, 2021, Volume 183, Issues 3-4: Petri Nets 2020
Symbolic and Structural Model-CheckingArticle

Authors: Yann Thierry-Mieg

    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.


    Volume: Volume 183, Issues 3-4: Petri Nets 2020
    Published on: December 23, 2021
    Accepted on: October 28, 2021
    Submitted on: April 8, 2021
    Keywords: Computer Science - Distributed, Parallel, and Cluster Computing,Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 148 times.
    This article's PDF has been downloaded 174 times.