符号化与结构化模型检验
Symbolic and Structural Model-Checking
AI总结：
本文提出结合SMT过近似、无记忆采样欠近似和结构化简规则，使模型检验复杂度与网结构而非状态空间成正比，并在2020年模型检验竞赛中赢得可达性查询和死锁检测。
摘要：
暴力模型检验包括对Petri网状态空间的穷举探索，并遭遇了令人畏惧的状态空间爆炸问题。相比之下，本文展示了如何通过组合多种技术来解决模型检验问题，这些技术的复杂度与网结构的大小成正比，而非与状态空间的大小成正比。我们结合了基于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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
