論文の概要: Forward LTLf Synthesis: DPLL At Work
- arxiv url: http://arxiv.org/abs/2302.13825v2
- Date: Mon, 19 Jun 2023 17:02:21 GMT
- ステータス: 処理完了
- システム内更新日: 2023-06-22 03:29:41.576769
- Title: Forward LTLf Synthesis: DPLL At Work
- Title（参考訳）: ltlf合成の前進:dpll at work
- Authors: Marco Favorito
- Abstract要約: 有限トレース(LTLf)上での線形時間論理の合成のための新しいAND-ORグラフ探索フレームワークを提案する。
このようなフレームワーク内では、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムにインスパイアされたプロシージャを考案し、次に利用可能なエージェント環境の動きを生成する。
また,状態公式の構文的等価性に基づく探索ノードの等価性チェックも提案する。
- 参考スコア（独自算出の注目度）: 1.370633147306388
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 本稿では,有限トレース(\LTLf)上の線形時間論理を合成するための新しいAND-ORグラフ探索フレームワークを提案する。
そのようなフレームワーク内では、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムにインスパイアされたプロシージャを考案し、真に深み第一の方法で次のエージェント環境の動きを生成する。
また,状態公式の構文的等価性に基づく探索ノードの等価性チェックも提案する。
結果の手続きは終了することが保証されていないので、実行を中止し、二分決定ダイアグラム(bdd)に基づいた状態等価チェックで検索を再開するための停止条件を特定します。
実験の結果,提案手法が他の最先端手法よりも優れていることがわかった。
我々の実装であるNikeは、2023年のSynTCOMPでLTLf Realizability Trackに出場し、優勝した。
関連論文リスト
- On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts [20.14001970300658]
トップダウン決定論的オートマトン構築に基づく有限トレース(LTLf)上での線形時間論理のオンザフライフレームワークを提案する。
論文 参考訳（メタデータ） (2024-08-14T06:52:58Z) - Double-Ended Synthesis Planning with Goal-Constrained Bidirectional Search [27.09693306892583]
材料制約を始点とする合成計画の定式化について述べる。
本稿では,双方向グラフ探索方式に基づく新しいCASPアルゴリズムであるDouble-Ended Synthesis Planning (DESP)を提案する。
DESPは既存のワンステップ逆合成モデルを利用することができ、これらのワンステップモデルの性能が向上するにつれて、その性能が拡大すると予想する。
論文 参考訳（メタデータ） (2024-07-08T18:56:00Z) - Optimizing NOTEARS Objectives via Topological Swaps [41.18829644248979]
本稿では,候補アルゴリズムの集合に有効な手法を提案する。
内部レベルでは、対象が与えられた場合、オフ・ザ・アート制約を利用する。
提案手法は,他のアルゴリズムのスコアを大幅に改善する。
論文 参考訳（メタデータ） (2023-05-26T21:49:37Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
凸最適化における総和係数法に着想を得て,広範な分岐関数を持つネットワーク上での検証クエリを解析するための新しい手法を提案する。
標準ケース分析に基づく完全探索手順の拡張は、各検索状態で実行される凸手順をDeepSoIに置き換えることによって達成できる。
論文 参考訳（メタデータ） (2022-03-19T15:05:09Z) - Recursive Causal Structure Learning in the Presence of Latent Variables
and Selection Bias [27.06618125828978]
本稿では,潜伏変数と選択バイアスの存在下での観測データからシステムの因果MAGを学習する問題を考察する。
本稿では,音と完全性を備えた計算効率のよい制約ベースの新しい手法を提案する。
提案手法と人工と実世界の両方の構造に関する技術の現状を比較した実験結果を提供する。
論文 参考訳（メタデータ） (2021-10-22T19:49:59Z) - Revisiting the Complexity Analysis of Conflict-Based Search: New
Computational Techniques and Improved Bounds [5.158632635415881]
最適解に対する最先端のアプローチは Conflict-Based Search (CBS) である
CBSの複雑性分析を再検討し、最悪の場合のアルゴリズムの実行時間に厳密な制限を与える。
論文 参考訳（メタデータ） (2021-04-18T07:46:28Z) - Improved Branch and Bound for Neural Network Verification via Lagrangian
Decomposition [161.09660864941603]
ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。
活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。
BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
論文 参考訳（メタデータ） (2021-04-14T09:22:42Z) - Lower bounds in multiple testing: A framework based on derandomized
proxies [107.69746750639584]
本稿では, 各種コンクリートモデルへの適用例を示す, デランドマイズに基づく分析戦略を提案する。
これらの下界のいくつかを数値シミュレーションし、Benjamini-Hochberg (BH) アルゴリズムの実際の性能と密接な関係を示す。
論文 参考訳（メタデータ） (2020-05-07T19:59:51Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
論文 参考訳（メタデータ） (2020-02-24T17:55:10Z) - The Simulator: Understanding Adaptive Sampling in the
Moderate-Confidence Regime [52.38455827779212]
エミュレータと呼ばれる適応サンプリングを解析するための新しい手法を提案する。
適切なログファクタを組み込んだトップk問題の最初のインスタンスベースの下位境界を証明します。
我々の新しい分析は、後者の問題に対するこの種の最初のエミュレータであるベストアームとトップkの識別に、シンプルでほぼ最適であることを示した。
論文 参考訳（メタデータ） (2017-02-16T23:42:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。