論文の概要: What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints

• arxiv url: http://arxiv.org/abs/2008.01926v1
• Date: Wed, 5 Aug 2020 04:18:59 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-02 18:47:29.859519
• Title: What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints
• Title（参考訳）: 全てできないとき何をすべきか:ソフトな時間的論理制約による時間的論理計画
• Authors: Hazhar Rahmani, Jason M. O'Kane
• Abstract要約: ソフト仕様の集合から最適な選択を満足する無限軌跡を見つけることを目的とした時間論理計画問題を考える。 提案アルゴリズムはまず,計画問題を最小限のコストで計算できる製品を構築する。 このような短いラッソを計算することは難しいが、短いラッソを合成するための効率的なグリージーなアプローチも導入する。
• 参考スコア（独自算出の注目度）: 28.072597424460472
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this paper, we consider a temporal logic planning problem in which the objective is to find an infinite trajectory that satisfies an optimal selection from a set of soft specifications expressed in linear temporal logic (LTL) while nevertheless satisfying a hard specification expressed in LTL. Our previous work considered a similar problem in which linear dynamic logic for finite traces (LDLf), rather than LTL, was used to express the soft constraints. In that work, LDLf was used to impose constraints on finite prefixes of the infinite trajectory. By using LTL, one is able not only to impose constraints on the finite prefixes of the trajectory, but also to set `soft' goals across the entirety of the infinite trajectory. Our algorithm first constructs a product automaton, on which the planning problem is reduced to computing a lasso with minimum cost. Among all such lassos, it is desirable to compute a shortest one. Though we prove that computing such a shortest lasso is computationally hard, we also introduce an efficient greedy approach to synthesize short lassos nonetheless. We present two case studies describing an implementation of this approach, and report results of our experiment comparing our greedy algorithm with an optimal baseline.
• Abstract（参考訳）: 本稿では、線形時間論理(LTL)で表されるソフト仕様の集合から最適な選択を満足する無限軌跡を見つけることを目的として、LTLで表されるハード仕様を満足しながら、時間論理計画問題を考える。 従来の研究では, LTL ではなく, 有限トレースに対する線形動的論理式 (LDLf) をソフト制約を表現するために用いた。 この研究において LDLf は無限軌跡の有限接頭辞に制約を与えるために使われた。 ltlを使用することで、軌道の有限接頭辞に制約を課すだけでなく、無限の軌道全体にわたって「ソフト」目標を設定することができる。 提案アルゴリズムはまず,計画問題を最小限のコストで計算する製品オートマトンを構築する。 これらすべてのラッソのうち、最も短いものを計算することが望ましい。 このような最短ラッソの計算が困難であることは証明するが、同時に短いラッソを合成するための効率的なグリージーアプローチも導入する。 本手法の実装を記述した2つのケーススタディと,本アルゴリズムと最適ベースラインを比較した実験結果について報告する。

関連論文リスト

• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications [59.01527054553122]
  リニア時間論理(LTL)は、強化学習(RL)における複雑で時間的に拡張されたタスクを特定する強力なフォーマリズムとして最近採用されている。 既存のアプローチはいくつかの欠点に悩まされており、それらは有限水平フラグメントにのみ適用でき、最適以下の解に制限され、安全制約を適切に扱えない。 本研究では,これらの問題に対処するための新しい学習手法を提案する。 提案手法は, 自動仕様のセマンティクスを明示的に表現したB"uchiaの構造を利用して, 所望の式を満たすための真理代入の順序を条件としたポリシーを学習する。
  論文  参考訳（メタデータ） (2024-10-06T21:30:38Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。 合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。 我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
  論文  参考訳（メタデータ） (2024-08-18T14:25:44Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。 有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
  論文  参考訳（メタデータ） (2023-07-31T17:02:23Z)
• Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
  我々は、制約付き最適化のための一階アルゴリズムと非滑らかなシステムの間で、新しい一階アルゴリズムのクラスを設計する。 これらのアルゴリズムの重要な性質は、制約がスパース変数の代わりに速度で表されることである。
  論文  参考訳（メタデータ） (2023-02-01T08:50:48Z)
• Policy Optimization with Linear Temporal Logic Constraints [37.27882290236194]
  本稿では,線形時間論理制約を用いた政策最適化の問題点について考察する。 我々は,タスク満足度とコスト最適性の両方を保証するために,サンプル複雑性分析を楽しむモデルベースアプローチを開発した。
  論文  参考訳（メタデータ） (2022-06-20T02:58:02Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic [2.631744051718347]
  トレースを分類する公式を学習する際の問題点を考察する。 既存の解には2つの制限がある: それらは小さな公式を超えてスケールせず、結果を返すことなく計算資源を消費する。 我々は,両問題に対処する新しいアルゴリズムを導入する。我々のアルゴリズムは,従来よりも桁違いに大きい式を構築でき,いつでも可能である。
  論文  参考訳（メタデータ） (2021-10-13T13:57:31Z)
• Efficient Temporal Piecewise-Linear Numeric Planning with Lazy Consistency Checking [4.834203844100679]
  本稿では,プランナがLP整合性チェックを可能な限り遅延的に計算できる手法を提案する。 また,時間依存ゴールチェックをより選択的に行うアルゴリズムを提案する。 結果として得られるプランナーは、より効率的であるだけでなく、最先端の時間数値とハイブリッドプランナーよりも優れています。
  論文  参考訳（メタデータ） (2021-05-21T07:36:54Z)
• Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach [22.46055650237819]
  雑音の存在下でも簡潔な公式を推測するための2つのアルゴリズムを考案する。 我々の第一のアルゴリズムは、推論問題を満足できる問題に還元することで最小の式を推論する。 第2の学習アルゴリズムは、決定木学習アルゴリズムに基づく公式上の決定木を導出する第1のアルゴリズムに依存している。
  論文  参考訳（メタデータ） (2021-04-30T16:06:03Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。 有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。 本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
  論文  参考訳（メタデータ） (2020-09-23T01:26:47Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。 ラグランジアン分解に基づく新しい手法を提案する。 ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
  論文  参考訳（メタデータ） (2020-02-24T17:55:10Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。