LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work

LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work

Giuseppe De Giacomo, Marco Favorito, Jianwen Li, Moshe Y. Vardi, Shengping Xiao, Shufang Zhu

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 2591-2598. https://doi.org/10.24963/ijcai.2022/359

Synthesis techniques for temporal logic specifications are typically based on exploiting symbolic techniques, as done in model checking. These symbolic techniques typically use backward fixpoint computation. Planning, which can be seen as a specific form of synthesis, is a witness of the success of forward search approaches. In this paper, we develop a forward-search approach to full-fledged Linear Temporal Logic on finite traces (LTLf) synthesis. We show how to compute the Deterministic Finite Automaton (DFA) of an LTLf formula on-the-fly, while performing an adversarial forward search towards the final states, by considering the DFA as a sort of AND-OR graph. Our approach is characterized by branching on suitable propositional formulas, instead of individual evaluations, hence radically reducing the branching factor of the search space. Specifically, we take advantage of techniques developed for knowledge compilation, such as Sentential Decision Diagrams (SDDs), to implement the approach efficiently.
Keywords:
Knowledge Representation and Reasoning: Reasoning about actions
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis
Planning and Scheduling: Theoretical Foundations of Planning