Symbolic and Structural Model-Checking

TL;DR

This paper introduces a hybrid approach combining SMT-based over-approximation, under-approximation sampling, and structural reductions to efficiently perform model-checking on Petri nets, overcoming state-space explosion issues.

Contribution

It presents a novel combination of techniques that operate in complexity proportional to the net's structure, improving efficiency and effectiveness in model-checking tasks.

Findings

Outperformed competitors in the 2020 model-checking contest

Successfully verified reachability and deadlock detection

Demonstrated practical applicability and scalability

Abstract

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.