论文标题
符号和结构模型检查
Symbolic and Structural Model-Checking
论文作者
论文摘要
蛮力模型检查包括对培养皿网的状态空间的详尽探索，并遇到了可怕的状态空间爆炸问题。 相比之下，本文展示了如何使用与净结构大小成正比的技术组合解决模型检查问题，而不是状态空间的大小。 我们结合了基于SMT的过度评价，以证明某些行为是不可行的，使用无记忆的跑步采样以查找证人痕迹或反调查，以及一组可以简化系统和属性的结构还原规则。 这种方法能够从2020年的模型检查竞赛中明确获胜，以获取可及性查询以及僵局检测，从而证明了本文介绍的规则制度的实际有效性和一般性适用性。
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.
