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, I 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. I 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, I identify a stopping condition to abort execution and restart the search with state-equivalence checking based on Binary Decision Diagrams (BDD), which I show to be correct. The experimental results show that in many cases the proposed techniques outperform other state-of-the-art approaches.

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