論文の概要: LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

• arxiv url: http://arxiv.org/abs/2411.09366v1
• Date: Thu, 14 Nov 2024 11:17:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-15 15:23:38.618488
• Title: LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
• Title（参考訳）: LTLf+とPLTL+:LTLfとPLTLを無限微量に拡張する
• Authors: Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi,
• Abstract要約: オートマチックf+/PPLTL+のためのDFAベースの合成技術について述べる。 PPLTL+の表現力は2EXPTIME完全ではなくEXPTIME完全であることを示す。
• 参考スコア（独自算出の注目度）: 44.35335751462176
• License:
• Abstract: We introduce LTLf+ and PPLTL+, two logics to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli's LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of the reactive synthesis problem for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL reactive synthesis. We present DFA-based synthesis techniques for LTLf+/PPLTL+, and show that synthesis is 2EXPTIME-complete for LTLf+ (matching LTLf) and EXPTIME-complete for PPLTL+ (matching PPLTL). Notably, while PPLTL+ retains the full expressive power of LTL, reactive synthesis is EXPTIME-complete instead of 2EXPTIME-complete. The techniques are also adapted to optimally solve satisfiability, validity, and model-checking, to get EXPSPACE-complete for LTLf+ (extending a recent result for the guarantee level using LTLf), and PSPACE-complete for PPLTL+.
• Abstract（参考訳）: 有限トレース上の線形時間時間時間論理 LTLf と PPLTL に基づく無限トレースの性質を表現する2つの論理 LTLf+ と PPLTL+ を導入する。 LTLf+/PPLTL+ は Manna と Pnueli の LTL セーフティプログレス階層のレベルを使用し、LTL と同じ表現力を持つ。 戦略抽出のゲームアリーナは決定論的有限オートマトン(DFA)から導出されることができる。 その結果、これらの論理はLTL反応合成の典型的な無限トレースオートマトンの決定に関わる悪名高い困難を回避している。 本稿では, LTLf+/PPLTL+の合成技術について述べるとともに, LTLf+(マッチングLTLf)に対して2EXPTIME完全であり, PPLTL+(マッチングPPLTL)に対してEXPTIME完全であることを示す。 特に、PLTL+はLTLの完全な表現力を保持するが、反応性合成は2EXPTIME完全ではなくEXPTIME完全である。 また, LTLf+ではEXPSPACEを, PPLTL+ではPSSPACEを, PPLTL+ではPSPSPACEを最適化した。

関連論文リスト

• LTLf Synthesis Under Unreliable Input [36.04060143603635]
  我々は、信頼できない入力変数の場合、少なくとも anf のバックアップ仕様が満たされることを保証しながら、 anf 目標仕様の戦略を実現する問題について検討する。 1つは2EXPTIME、もう1つは信頼できない入力変数を無視する3EXPTIME、もう1つは2次量子化f(QLTLf)を利用する3つの異なる解法を考案した。 興味深いことに、理論上の最悪のケース境界は観測性能に変換されず、MSO技術は最もよく機能し、次いで信念構築と直接オートマチック操作が続く。
  論文  参考訳（メタデータ） (2024-12-19T10:54:17Z)
• On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts [20.14001970300658]
  トップダウン決定論的オートマトン構築に基づく有限トレース(LTLf)上での線形時間論理のオンザフライフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-08-14T06:52:58Z)
• Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
  本稿では,古典的リアクティブハンドル(命題)を仕様言語として,時間論理仕様から正しいコントローラを生成する方法を示す。 また,制御器が常に最小の安全値を提供するために出力を最適化できるという意味で応答が可能であることを示す。
  論文  参考訳（メタデータ） (2024-07-12T15:23:27Z)
• 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)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。 有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。 本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
  論文  参考訳（メタデータ） (2020-09-23T01:26:47Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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