論文の概要: 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} 証拠である。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。