Model Checking is widely applied in verifying complicated and especially concurrent systems. Despite of its popularity, model checking suffers from the state space explosion problem that restricts it from being applied to certain systems, or specifications. Many works have been proposed in the past to address the state space explosion problem, and they have achieved some success, but the inherent complexity still remains an obstacle for purely symbolic approaches. In this paper, we propose a Graph Neural Network (GNN) based approach for model checking, where the model is expressed using a B{\"u}chi automaton and the property to be verified is expressed using Linear Temporal Logic (LTL). We express the model as a GNN, and propose a novel node embedding framework that encodes the LTL property and characteristics of the model. We reduce the LTL model checking problem to a graph classification problem, where there are two classes, 1 (if the model satisfies the specification) and 0 (if the model does not satisfy the specification). The experimental results show that our framework is up to 17 times faster than state-of-the-art tools. Our approach is particularly useful when dealing with very large LTL formulae and small to moderate sized models.

翻译：模型检验广泛应用于复杂系统尤其是并发系统的验证中。尽管其应用广泛，但模型检验受限于状态空间爆炸问题，这限制了其在某些系统或规范上的应用。过去虽有诸多研究致力于解决状态空间爆炸问题并取得一定成效，但纯符号方法仍难以克服其固有复杂性。本文提出一种基于图神经网络（GNN）的模型检验方法，其中模型用Büchi自动机表示，待验证性质用线性时态逻辑（LTL）描述。我们将模型表示为GNN，并提出一种新颖的节点嵌入框架，该框架可编码LTL性质与模型特征。我们将LTL模型检验问题转化为图分类问题，类别分为两类：1（模型满足规范）和0（模型不满足规范）。实验结果表明，我们的框架比最新工具快达17倍。本方法在处理大规模LTL公式及中小规模模型时尤为有效。