論文の概要: LTLf Synthesis Under Unreliable Input

• arxiv url: http://arxiv.org/abs/2412.14728v1
• Date: Thu, 19 Dec 2024 10:54:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-20 13:30:18.920954
• Title: LTLf Synthesis Under Unreliable Input
• Title（参考訳）: 信頼できない入力によるLTLf合成
• Authors: Christian Hagemeier, Giuseppe de Giacomo, Moshe Y. Vardi,
• Abstract要約: 我々は、信頼できない入力変数の場合、少なくとも anf のバックアップ仕様が満たされることを保証しながら、 anf 目標仕様の戦略を実現する問題について検討する。 1つは2EXPTIME、もう1つは信頼できない入力変数を無視する3EXPTIME、もう1つは2次量子化f(QLTLf)を利用する3つの異なる解法を考案した。 興味深いことに、理論上の最悪のケース境界は観測性能に変換されず、MSO技術は最もよく機能し、次いで信念構築と直接オートマチック操作が続く。
• 参考スコア（独自算出の注目度）: 36.04060143603635
• License:
• Abstract: We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf backup specification is satisfied in case of unreliability of certain input variables. We formally define the problem and characterize its worst-case complexity as 2EXPTIME-complete, like standard LTLf synthesis. Then we devise three different solution techniques: one based on direct automata manipulation, which is 2EXPTIME, one disregarding unreliable input variables by adopting a belief construction, which is 3EXPTIME, and one leveraging second-order quantified LTLf (QLTLf), which is 2EXPTIME and allows for a direct encoding into monadic second-order logic, which in turn is worst-case nonelementary. We prove their correctness and evaluate them against each other empirically. Interestingly, theoretical worst-case bounds do not translate into observed performance; the MSO technique performs best, followed by belief construction and direct automata manipulation. As a byproduct of our study, we provide a general synthesis procedure for arbitrary QLTLf specifications.
• Abstract（参考訳）: 入力変数の信頼性が低い場合、少なくともLTLfバックアップ仕様が満たされることを保証しながら、LTLfゴール仕様の戦略を実現する問題について検討する。 我々は、この問題を正式に定義し、その最悪のケースの複雑さを標準LTLf合成のように2EXPTIME完全であると特徴づける。 次に, 2EXPTIME の直接オートマタ操作に基づく手法, 3EXPTIME の信念構成を採用することで信頼できない入力変数を無視する手法, 2EXPTIME の2次量子化 LTLf (QLTLf) を活用する手法,およびモナディックな2次論理への直接エンコードを可能にする手法を考案した。 私たちは彼らの正しさを証明し、互いに実証的に評価します。 興味深いことに、理論上の最悪のケース境界は観測性能に変換されない。 本研究の副産物として、任意のQLTLf仕様に対する一般的な合成手順を提案する。

関連論文リスト

• LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces [44.35335751462176]
  オートマチックf+/PPLTL+のためのDFAベースの合成技術について述べる。 PPLTL+の表現力は2EXPTIME完全ではなくEXPTIME完全であることを示す。
  論文  参考訳（メタデータ） (2024-11-14T11:17:06Z)
• 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)
• Model Checking Strategies from Synthesis Over Finite Traces [25.871354900295056]
  モデルチェックでは、2種類のトランスデューサが根本的に異なる。 本研究では,非終端トランスデューサのモデル検査は終端トランスデューサのモデル検査よりも明らかに困難であることを示す。
  論文  参考訳（メタデータ） (2023-05-15T03:09:20Z)
• Confident Adaptive Language Modeling [95.45272377648773]
  CALMは、入力と生成時間ごとに異なる量の計算を動的に割り当てるフレームワークである。 ハイパフォーマンスを確実に維持しつつ、計算能力、潜在的スピードアップを最大3ドルまで削減する上で、我々のフレームワークの有効性を実証する。
  論文  参考訳（メタデータ） (2022-07-14T17:00:19Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Learning Bounded Context-Free-Grammar via LSTM and the Transformer:Difference and Explanations [51.77000472945441]
  Long Short-Term Memory (LSTM) と Transformer は、自然言語処理タスクに使用される2つの一般的なニューラルネットワークアーキテクチャである。 実際には、トランスフォーマーモデルの方がLSTMよりも表現力が高いことがよく見られる。 本研究では,LSTMとTransformerの実践的差異について検討し,その潜在空間分解パターンに基づく説明を提案する。
  論文  参考訳（メタデータ） (2021-12-16T19:56:44Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。 有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。 本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
  論文  参考訳（メタデータ） (2020-09-23T01:26:47Z)
• FastLR: Non-Autoregressive Lipreading Model with Integrate-and-Fire [74.04394069262108]
  我々は,全てのターゲットトークンを同時に生成する非自己回帰(NAR)リップリーダーモデルであるFastLRを提案する。 FastLRは最先端のリップリーダーモデルと比較して10.97$times$のスピードアップを実現している。
  論文  参考訳（メタデータ） (2020-08-06T08:28:56Z)

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

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