论文标题
八分之一：LTL模型检查的图表学习
OCTAL: Graph Representation Learning for LTL Model Checking
论文作者
论文摘要
模型检查广泛应用于验证与规范相对于规范的复杂系统和并发系统的正确性。纯象征性方法虽然受欢迎，但仍遭受了状态空间爆炸问题，这使得它们对于大型系统和/或规格不切实际。在本文中，我们建议使用图表表示学习（GRL）来求解线性时间逻辑（LTL）模型检查，其中系统和规范分别由BüchiAutomaton和LTL公式表示。一种新型的基于GRL的框架八元旨在学习图形结构化系统和规范的表示，这将模型检查问题减少到潜在空间中的二进制分类。经验实验表明，与三个不同数据集上的规范SOTA模型检查器相当的精度可比性，最高$ 5 \ times $ $总体加速，超过$ 63 \ times $ $ $ $ $ $ $ $ $用于单独检查。
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that makes them impractical 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üchi automaton and an LTL formula respectively. A novel GRL-based framework OCTAL, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification in the latent space. The empirical experiments show that OCTAL achieves comparable accuracy against canonical SOTA model checkers on three different datasets, with up to $5\times$ overall speedup and above $63\times$ for satisfiability checking alone.
