論文の概要: On Strategies in Synthesis Over Finite Traces
- arxiv url: http://arxiv.org/abs/2305.08319v1
- Date: Mon, 15 May 2023 03:09:20 GMT
- ステータス: 処理完了
- システム内更新日: 2023-05-16 16:20:06.144632
- Title: On Strategies in Synthesis Over Finite Traces
- Title（参考訳）: 有限トレース上の合成の戦略について
- Authors: Suguman Bansal and Yong Li and Lucas Martinelli Tabajara and Moshe Y.
Vardi and Andrew Wells
- Abstract要約: モデル検査では,2種類のトランスデューサが根本的に異なることを示す。
問題はexpspace-complete と $pspace$-complete である。
- 参考スコア（独自算出の注目度）: 25.871354900295056
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The innovations in reactive synthesis from {\em Linear Temporal Logics over
finite traces} ($\ltlf$) will be amplified by the ability to verify the
correctness of the strategies generated by $\ltlf$ synthesis tools. This
motivates our work on {\em $\ltlf$ model checking}. $\ltlf$ model checking,
however, is not straightforward. The strategies generated by $\ltlf$ synthesis
may be represented using {\em terminating} transducers or {\em non-terminating}
transducers where executions are of finite-but-unbounded length or infinite
length, respectively. For synthesis, there is no evidence that one type of
transducer is better than the other since they both demonstrate the same
complexity and similar algorithms.
In this work, we show that for model checking, the two types of transducers
are fundamentally different. Our central result is that $\ltlf$ model checking
of non-terminating transducers is \emph{exponentially harder} than that of
terminating transducers. We show that the problems are \expspace-complete and
$\pspace$-complete, respectively. Hence, considering the feasibility of
verification, $\ltlf$ synthesis tools should synthesize terminating
transducers. This is, to the best of our knowledge, the \emph{first} evidence
to use one transducer over the other in $\ltlf$ synthesis.
- Abstract（参考訳）: 有限トレース($\ltlf$)上の線形時相論理からの反応合成の革新は、$\ltlf$合成ツールによって生成される戦略の正確性を検証する能力によって増幅される。
これは、"em $\ltlf$ model checking}" に対する我々の取り組みを動機付けます。
しかし、$\ltlf$モデルチェックは簡単ではない。
$\ltlf$ 合成によって生成される戦略は、それぞれ有限だが無限の長さのトランスデューサまたは'em non-terminating}トランスデューサを用いて表現することができる。
合成において、同じ複雑さと類似したアルゴリズムを示すため、あるタイプのトランスデューサが他方よりも優れているという証拠はない。
本稿では,モデル検査において,2種類のトランスデューサが根本的に異なることを示す。
中心となる結果は、非終端トランスデューサの$\ltlf$モデルチェックは、終端トランスデューサよりも\emph{exponentially difficult}であるということです。
問題はそれぞれ \expspace-complete と $\pspace$-complete である。
したがって、検証の可能性を考慮すると、$\ltlf$合成ツールは終端トランスデューサを合成する必要がある。
これは、私たちの知る限りでは、$\ltlf$合成において1つのトランスデューサをもう1つ使うという \emph{first} の証拠である。
関連論文リスト
- 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) - Training Nonlinear Transformers for Chain-of-Thought Inference: A Theoretical Generalization Analysis [82.51626700527837]
チェーン・オブ・シフト(Chain-of-shift, CoT)は、複数の中間ステップを持つ例を用いてクエリを増強することにより、大規模言語モデルの推論能力を実現する効率的な手法である。
CoT の理論的成功にもかかわらず、CoT が成立しても正確な一般化が得られないことを示す。
論文 参考訳（メタデータ） (2024-10-03T03:12:51Z) - 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) - SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
トピック分類,感情分析,トーン検出,ユーモアの6つのデータセットの合成について検討した。
その結果,SynthesizRRは語彙や意味の多様性,人文との類似性,蒸留性能を大幅に向上させることがわかった。
論文 参考訳（メタデータ） (2024-05-16T12:22:41Z) - Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。
有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
論文 参考訳（メタデータ） (2023-07-31T17:02:23Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。