論文の概要: 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を最適化した。

関連論文リスト

• 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)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。 提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
  論文  参考訳（メタデータ） (2019-12-31T17:09:49Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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