Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, suffer from the state space explosion problem due to cross product operations required that make them prohibitively expensive for large-scale systems and/or specifications. In this paper, we propose to use graph representation learning (GRL) for solving linear temporal logic (LTL) model checking, where the system and the specification are expressed by a B{\"u}chi automaton and an LTL formula, respectively. A novel GRL-based framework \model, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification. Empirical experiments on two model checking scenarios show that \model achieves promising accuracy, with up to $11\times$ overall speedup against canonical SOTA model checkers and $31\times$ for satisfiability checking alone.

翻译：模型检验被广泛应用于验证复杂并发系统是否满足规约的正确性。纯符号化方法虽被广泛采用，但因需要执行笛卡尔积运算而导致状态空间爆炸问题，这使得其在大规模系统和/或规约上的计算成本高昂。本文提出利用图表示学习（GRL）解决线性时态逻辑（LTL）模型检验问题，其中系统与规约分别由Büchi自动机和LTL公式表示。我们设计了一种新型基于GRL的框架\model，用于学习图结构系统与规约的表示，从而将模型检验问题转化为二分类任务。在两个模型检验场景上的实证实验表明，\model在取得显著精度的同时，相比经典最优模型检验器可实现最高$11$倍的整体加速，其中可满足性检验任务单独加速达$31$倍。