Forward LTLf Synthesis: DPLL At Work

要約

この論文では、以前のアプローチのいくつかの制限を克服する、有限トレース (LTLf) 上の線形時相論理の合成のための新しい AND-OR グラフ検索フレームワークを提案します。
このようなフレームワーク内で、Davis-Putnam-Logemann-Loveland (DPLL) アルゴリズムに触発された手順を考案して、真の深さ優先の方法で次に利用可能なエージェント環境の動きを生成し、おそらく徹底的な列挙やコストのかかるコンパイルを回避します。
また、状態式の構文上の等価性に基づく検索ノードの新しい等価性チェックも提案します。
結果のプロシージャが終了するとは限らないため、実行を中止する停止条件を特定し、二分決定図 (BDD) に基づく状態等価性チェックを使用して検索を再開します。これが正しいことを示しています。
実験結果は、多くの場合、提案された技術が他の最先端のアプローチよりも優れていることを示しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google