LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
复制标题
DOI：
10.24963/ijcai.2022/359
复制
发表时间：
2022-07
期刊：
影响因子：
--
通讯作者：
G. D. Giacomo;Marco Favorito;Jianwen Li;M. Vardi;Shengping;Xiao;Shufang Zhu
中科院分区：
文献类型：
--
作者：
G. D. Giacomo;Marco Favorito;Jianwen Li;M. Vardi;Shengping;Xiao;Shufang Zhu
时序逻辑规范的合成技术通常基于利用符号技术，如在模型检查中所做的。这些符号技术通常使用后向定点计算。规划可以被看作是一种具体的综合形式，是前瞻性探索方法成功的见证。在本文中，我们开发了一个前向搜索的方法，以全面的线性时序逻辑有限迹（LTLf）的综合。我们展示了如何计算LTLf公式的确定性有限自动机（DFA），同时通过将DFA视为一种AND-OR图来对最终状态进行对抗性前向搜索。我们的方法的特点是在合适的命题公式上进行分支，而不是单独的评估，因此从根本上减少了搜索空间的分支因子。具体来说，我们利用知识编译开发的技术，如句子决策图（SDDs），有效地实现该方法。
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.