有限迹上线性时序逻辑的即时合成：一种高效的计数方法

我们提出了一种基于自顶向下确定自动机构造的线性时序逻辑有限迹（LTLf）即时合成框架。现有方法依赖于构造与 LTLf 规范相对应的完整确定有限自动机（DFA），该过程在最坏情况下具有相对于公式规模的 doubly exponential 复杂度。在此情况下，合成过程必须等待整个 DFA 构造完成后才能进行。这种低效性是现有方法的主要瓶颈。为应对这一挑战，我们首先提出了一种利用 LTLf 语义直接将 LTLf 转换为基于转移的确定有限自动机（TDFA）的方法，将中间结果作为最终自动机的直接组件，从而实现并行化合成与自动机构造。随后我们探讨了 LTLf 合成与 TDFA 游戏之间的关系，并开发了一种通过即时 TDFA 游戏求解来执行 LTLf 合成的算法。该算法以全局前向方式结合局部后向方式遍历状态空间，并检测强连通分量。此外，我们引入了两种优化技术——模型引导合成与状态蕴含——以提升我们方法的实际效率。实验结果表明，我们的即时合成方法在测试基准上取得了最优性能，并有效补充了现有工具与方法。