論文の概要: Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

• arxiv url: http://arxiv.org/abs/2407.09348v1
• Date: Fri, 12 Jul 2024 15:23:27 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-15 23:08:25.378994
• Title: Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
• Title（参考訳）: 機能的合成による予測可能かつ高性能な反応合成モジュロ理論
• Authors: Andoni Rodríguez, Felipe Gorostiaga, César Sánchez,
• Abstract要約: 本稿では,古典的リアクティブハンドル(命題)を仕様言語として,時間論理仕様から正しいコントローラを生成する方法を示す。 また,制御器が常に最小の安全値を提供するために出力を最適化できるという意味で応答が可能であることを示す。
• 参考スコア（独自算出の注目度）: 1.1797787239802762
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory calT and outputs valuations of system variables from calT. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLt specification. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLt, which is a deterministic program (hence predictable and efficient).
• Abstract（参考訳）: リアクティブ合成は、時間論理仕様から正しいコントローラを生成するプロセスである。 古典的なLTL反応合成は、仕様言語としての(命題的な)LTLを扱う。 ブール抽象は、LTLt仕様(すなわち、alT理論のリテラルに置換された命題付きLTL)を等価化可能なLTL仕様に還元することを可能にする。 本稿では、これらの結果を完全な静的合成手順に拡張する。 合成システムは、豊かな理論である calT から変数の環境評価を受信し、 calT から変数の環境評価を出力する。 LTL仕様からリアクティブBooleanコントローラを合成するためにこの抽象化手法を用い、これを関数合成と組み合わせて元のLTLt仕様の静的コントローラを得る。 また,制御器が出力を最適化できるという意味で応答を許容し,常に最小の安全値を提供することを示す。 これはLTLtの完全な静的合成法であり、決定論的プログラムである(したがって予測可能で効率的である)。

関連論文リスト

• LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces [44.35335751462176]
  オートマチックf+/PPLTL+のためのDFAベースの合成技術について述べる。 PPLTL+の表現力は2EXPTIME完全ではなくEXPTIME完全であることを示す。
  論文  参考訳（メタデータ） (2024-11-14T11:17:06Z)
• SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
  トピック分類,感情分析,トーン検出,ユーモアの6つのデータセットの合成について検討した。 その結果,SynthesizRRは語彙や意味の多様性,人文との類似性,蒸留性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-05-16T12:22:41Z)
• Guiding Enumerative Program Synthesis with Large Language Models [15.500250058226474]
  本稿では,形式的合成ベンチマークを解くための大規模言語モデルの能力を評価する。 ワンショット合成が失敗すると,新しい列挙合成アルゴリズムを提案する。 形式的合成のためのスタンドアロンツールとしてGPT-3.5は,最先端の形式的合成アルゴリズムにより容易に性能が向上することがわかった。
  論文  参考訳（メタデータ） (2024-03-06T19:13:53Z)
• Efficient Reactive Synthesis Using Mode Decomposition [0.0]
  そこで本研究では,モードに基づく新しい分解アルゴリズムを提案する。 我々のアルゴリズムへの入力は、元の仕様とモードの記述である。 サブ仕様の自動生成方法を示し、全てのサブプロブレムが実現可能であれば、完全な仕様が実現可能であることを示す。
  論文  参考訳（メタデータ） (2023-12-14T08:01:35Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。 有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
  論文  参考訳（メタデータ） (2023-07-31T17:02:23Z)
• Model Checking Strategies from Synthesis Over Finite Traces [25.871354900295056]
  モデルチェックでは、2種類のトランスデューサが根本的に異なる。 本研究では,非終端トランスデューサのモデル検査は終端トランスデューサのモデル検査よりも明らかに困難であることを示す。
  論文  参考訳（メタデータ） (2023-05-15T03:09:20Z)
• 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)
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers [70.70479436076238]
  線形、非線形(ポリノミカル)およびパラメトリックモデルに対するリャプノフ関数を合成する。 パラメトリックテンプレートからLyapunov関数を合成するための帰納的フレームワークを利用する。
  論文  参考訳（メタデータ） (2020-07-21T14:45:23Z)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。 提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
  論文  参考訳（メタデータ） (2019-12-31T17:09:49Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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