基于图表示学习的可验证 LTL 可满足性检查

基于摘要分析。本文研究线性时序逻辑（LTL）公式的可满足性检查，提出一种在判断公式可满足时同时生成满足轨迹的方法，以轨迹为可满足结论提供验证依据。核心贡献是 one-step unfolded graph（OSUG，单步展开图），用于联合表示 LTL 公式的语法与语义特征。 作者将现有神经方法的局限概括为归纳能力受限、难以支持任意数量的原子命题，以及缺乏可满足性结果的验证机制。OSUG 的设计旨在为学习式检查提供更合适的公式表示，但摘要未说明具体图构造、网络结构、训练目标及轨迹生成与验证流程。满足轨迹支持的是可满足结论，不能据此推断该方法也为不可满足结论提供了证明。 作者报告，在合成数据集上的初步实验中，该方法优于所比较的先进神经方法，并支持 OSUG 的有效性。摘要未提供数据集名称、规模、划分、基线名称或具体指标；实验协议、消融及统计信息尚未验证。开篇关于多项式时间获得高置信结果的表述属于研究动机，不能解读为已获得通用、精确的多项式时间 LTL 判定算法。 本文主要对象是形式逻辑与可满足性检查，所给材料未建立其与 EEG 或 BCI 任务的具体机制对应，因此不据此推断 BCI 有效性或提出迁移实验。