論文の概要: Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

• arxiv url: http://arxiv.org/abs/2608.02454v1
• Date: Mon, 03 Aug 2026 16:30:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-04 15:07:25.706784
• Title: Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
• Title（参考訳）: 有限トレース法による無限トレース対象:LTLをLTLf+に変換する
• Abstract要約: リニア論理(LTL)は、AIの時間拡張目的を指定するための最も広く採用されている言語の一つである。 伝統的に、これらの問題のどれでも解決するには、無限語上の非決定論的オートマトンに仕様を翻訳する必要がある。 最近の研究は、有限トレース論理fを無限トレースに引き上げるf+を導入している。
• 参考スコア（独自算出の注目度）: 27.722473386464127
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stochastic planning in Markov decision processes and reinforcement learning. Traditionally, solving any of these problems requires translating the LTL specification to a nondeterministic automata on infinite words and then determinizing it, a step that is notoriously difficult in theory and in practice. Recent work has introduced LTLf+, which lifts the finite-trace logic LTLf to infinite traces. LTLf+ has the same expressive power as LTL, yet it retains most of the crucial advantages of its base logic LTLf. Most reasoning in LTLf+ rests on finite automata on finite words, for which we have not only a canonical minimal representation but also an efficient determinization procedure. In this work we present the first translation from LTL to LTLf+. We first normalize an LTL formula into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, to create the general fragment-based shape of LTLf+. We then present linear translations for each individual component of that fragment. As a consequence of this translation, the expanding body of techniques developed for LTLf+ now becomes available to many AI problems currently formulated in LTL. We further show that this comes at no asymptotic cost, as the pipeline from LTL to automaton via LTLf+ remains doubly exponential.
• Abstract（参考訳）: 線形時間論理(LTL)は、AIにおける時間的拡張目的を指定するために最も広く採用されている言語の一つであり、マルコフ決定プロセスにおける反応性合成から確率計画まで、そして強化学習の応用がある。 伝統的に、これらの問題のどれでも解決するには、LTL仕様を無限語上の非決定論的オートマトンに翻訳し、それを決定づける必要がある。 最近の研究は LTLf+ を導入しており、これは有限トレース論理 LTLf を無限トレースに引き上げるものである。 LTLf+はLTLと同じ表現力を持つが、基本論理LTLfの重要な利点のほとんどを保っている。 LTLf+ のほとんどの推論は有限語上の有限オートマトンに依存している。 本稿では LTL から LTLf+ への最初の変換を示す。 まずLTL式をManna-Pnueli階層の構文的反応性フラグメントに正規化し、LTLf+の一般的なフラグメントベースの形状を作成する。 次に、その断片の個々の成分について線形変換を示す。 この翻訳の結果、LTLf+用に開発された技術が拡張され、現在LTLで定式化されている多くのAI問題に利用できるようになった。 さらに,LTLからLTLf+経由のオートマトンへのパイプラインは2倍指数的であり,漸近的なコストは伴わないことを示した。

関連論文リスト

• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  本研究では,大規模状態空間を持つ決定過程(MDP)における非マルコフ報酬の論理的仕様に関する新しい枠組みを提案する。 我々のアプローチは有限トレース(LTLfMT)上での線形時間論理モデュロ理論を利用する 本稿では,報酬マシンとHER(Hindsight Experience Replay)をベースとした一階述語論理仕様の翻訳手法を提案する。
  論文  参考訳（メタデータ） (2026-02-05T22:11:28Z)
• LTLf Synthesis Under Unreliable Input [36.04060143603635]
  我々は、信頼できない入力変数の場合、少なくとも anf のバックアップ仕様が満たされることを保証しながら、 anf 目標仕様の戦略を実現する問題について検討する。 1つは2EXPTIME、もう1つは信頼できない入力変数を無視する3EXPTIME、もう1つは2次量子化f(QLTLf)を利用する3つの異なる解法を考案した。 興味深いことに、理論上の最悪のケース境界は観測性能に変換されず、MSO技術は最もよく機能し、次いで信念構築と直接オートマチック操作が続く。
  論文  参考訳（メタデータ） (2024-12-19T10:54:17Z)
• LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces [44.35335751462176]
  オートマチックf+/PPLTL+のためのDFAベースの合成技術について述べる。 PPLTL+の表現力は2EXPTIME完全ではなくEXPTIME完全であることを示す。
  論文  参考訳（メタデータ） (2024-11-14T11:17:06Z)
• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL [59.01527054553122]
  線形時間論理(LTL)は、最近、複雑で時間的に拡張されたタスクを特定するための強力なフォーマリズムとして採用されている。 既存のアプローチにはいくつかの欠点がある。 これらの問題に対処するための新しい学習手法を提案する。
  論文  参考訳（メタデータ） (2024-10-06T21:30:38Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。 有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
  論文  参考訳（メタデータ） (2023-07-31T17:02:23Z)
• Model Checking Strategies from Synthesis Over Finite Traces [25.871354900295056]
  モデルチェックでは、2種類のトランスデューサが根本的に異なる。 本研究では,非終端トランスデューサのモデル検査は終端トランスデューサのモデル検査よりも明らかに困難であることを示す。
  論文  参考訳（メタデータ） (2023-05-15T03:09:20Z)
• A first-order logic characterization of safety and co-safety languages [63.29821624186913]
  有限の接頭辞が、ある単語が言語に属していないか、属していないかを確立するのに十分である安全で共同安全な言語は、モデル検査や反応合成のような問題の複雑さを下げる上で重要な役割を果たす。 本稿では,安全性とコセーフティ言語に関して,FO-TLOの断片であるSafetyFOと,その二重コセーフティについて述べる。
  論文  参考訳（メタデータ） (2022-09-06T09:00:38Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。 有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。 本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
  論文  参考訳（メタデータ） (2020-09-23T01:26:47Z)

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

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