This paper proposes a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (\LTLf), that overcomes some limitations of previous approaches. Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves in a truly depth-first fashion, possibly avoiding exhaustive enumeration or costly compilations. We also propose a novel equivalence check for search nodes based on syntactic equivalence of state formulas. Since the resulting procedure is not guaranteed to terminate, we identify a stopping condition to abort execution and restart the search with state-equivalence checking based on Binary Decision Diagrams (BDD), which we show to be correct. The experimental results show that in many cases the proposed techniques outperform other state-of-the-art approaches. Our implementation Nike competed in the LTLf Realizability Track in the 2023 edition of SYNTCOMP, and won the competition.

翻译：本文提出了一种新的AND-OR图搜索框架，用于有限迹上的线性时态逻辑（LTLf）的合成，克服了先前方法的一些局限性。在该框架内，我们设计了一种受Davis-Putnam-Logemann-Loveland（DPLL）算法启发的过程，以真正的深度优先方式生成下一个可用的智能体-环境移动，从而可能避免穷举枚举或昂贵的编译。我们还提出了一种基于状态公式语法等价性的搜索节点新型等价性检查。由于所得到的过程不能保证终止，我们识别了一个停止条件，以中止执行并重新启动带有基于二叉决策图（BDD）的状态等价检查的搜索，我们证明了该方法的正确性。实验结果表明，在许多情况下，所提出的技术优于其他最先进的方法。我们的实现Nike参加了2023年SYNTCOMP的LTLf可实现性赛道，并赢得了比赛。