一句话：提出融合语法与语义的LTL图表示OSUG，用图学习判定可满足性并生成可验证的可满足迹。
LTL可满足性检查是PSPACE完全的经典问题，凭借神经网络强大的学习能力，有望在多项式时间内得到高置信度的判定结果。然而现有神经方法归纳能力有限、难以支持任意数量的原子命题，且缺少对可满足性结果的验证机制。本文提出一种LTL可满足性检查方法：不仅判定公式是否可满足，还在公式可满足时生成一条可满足迹，用该迹来验证可满足性结论。其核心贡献是一种新的LTL公式图表示——一步展开图（one-step unfolded graph, OSUG），它同时刻画LTL的语法与语义特征，从而提升模型的归纳能力与命题数量上的泛化性。在合成数据集上的初步结果表明，该方法优于当前最先进的神经方法，并验证了OSUG的有效性。
With the superior learning ability of neural networks, it is promising to obtain highly confident results for linear temporal logic (LTL) satisfiability checking in polynomial time. However, existing neural approaches are limited in inductive ability and in supporting with an arbitrary number of atomic propositions. Besides, there is no mechanism to verify the results for satisfiability checking. In this paper, we propose an approach to checking the satisfiability of an LTL formula and meanwhile generating a satisfiable trace if the LTL formula is satisfiable, where the satisfiable trace verifies the satisfiability result. The core contribution is a new graph representation for LTL formulae - one-step unfolded graph (OSUG) to incorporate the syntax and semantic features of LTL. Preliminary results show that our approach is superior to the state-of-the-art neural approaches on synthetic datasets and confirms the effectiveness of OSUG.
@inproceedings{LuoZYWDLC23,
title = {SAT-Verifiable LTL Satisfiability Checking via Graph Representation Learning},
author = {Weilin Luo and Yuhang Zheng and Rongzhen Ye and Hai Wan and Jianfeng Du and Pingjia Liang and Polong Chen},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00173}
}