論文の概要: 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} の証拠である。
関連論文リスト
- 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) - Exposing Attention Glitches with Flip-Flop Language Modeling [55.0688535574859]
この研究は、大きな言語モデルにおける注意点の現象を特定し、分析する。
ニューラルネットワークモデルの外挿挙動を探索するために設計された,合成ベンチマークのファミリであるフリップフロップ言語モデリング(FFLM)を導入する。
その結果,Transformer FFLM は散発的推論誤差の長い尾に悩まされていることがわかった。
論文 参考訳（メタデータ） (2023-06-01T17:44:35Z) - 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) - Towards Neural-Guided Program Synthesis for Linear Temporal Logic
Specifications [26.547133495699093]
ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。
提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
論文 参考訳（メタデータ） (2019-12-31T17:09:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。