論文の概要: Model Checking Strategies from Synthesis Over Finite Traces
- arxiv url: http://arxiv.org/abs/2305.08319v3
- Date: Sun, 30 Jul 2023 19:44:20 GMT
- ステータス: 処理完了
- システム内更新日: 2023-08-01 22:45:49.623424
- Title: Model Checking Strategies from Synthesis Over Finite Traces
- Title（参考訳）: 有限トレース上の合成によるモデルチェック戦略
- Authors: Suguman Bansal and Yong Li and Lucas Martinelli Tabajara and Moshe Y.
Vardi and Andrew Wells
- Abstract要約: モデルチェックでは、2種類のトランスデューサが根本的に異なる。
本研究では,非終端トランスデューサのモデル検査は終端トランスデューサのモデル検査よりも明らかに困難であることを示す。
- 参考スコア（独自算出の注目度）: 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合成によって生成される戦略は、実行が有限だが非有界長または無限長であるような変換子または非終端変換子を用いて表すことができる。
合成において、同じ複雑さと類似したアルゴリズムを示すため、あるタイプのトランスデューサが他方よりも優れているという証拠はない。
本稿では,モデル検査において,2種類のトランスデューサが根本的に異なることを示す。
我々の中心的な結果は、非終端トランスデューサのLTLfモデル検査が終端トランスデューサのモデル検査よりも難しいことである。
これらの問題はそれぞれEXPSPACE完全かつPSPACE完全であることを示す。
したがって、検証の可能性を考えると、LTLf合成ツールは終端トランスデューサを合成すべきである。
これは、我々の知る限りでは、ltlf合成において一方のトランスデューサを他方のトランスデューサに使用するための\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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。