Forward LTLf Synthesis: DPLL At Work
This addresses the challenge of efficient LTLf synthesis for automated verification and planning, representing an incremental improvement over prior methods.
The paper tackles the problem of synthesizing Linear Temporal Logic on finite traces (LTLf) by proposing a new AND-OR graph search framework with a DPLL-inspired procedure and novel equivalence checks, resulting in an implementation that won the 2023 SYNTCOMP competition and outperforms other state-of-the-art approaches in many cases.
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.