論文の概要: Incremental LTLf Synthesis
- arxiv url: http://arxiv.org/abs/2603.01201v1
- Date: Sun, 01 Mar 2026 17:42:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-03 19:50:56.563035
- Title: Incremental LTLf Synthesis
- Title(参考訳): インクリメンタルLTLf合成
- Authors: Giuseppe De Giacomo, Yves Lespérance, Gianmarco Parretti, Fabio Patrizi, Moshe Y. Vardi,
- Abstract要約: インクリメンタルな合成 — 実行中に目標が漸進的に与えられる,リアクティブな合成形式 — について検討する。
本稿では,複数目標に対するインクリメンタルな合成を効率的に行う解法を提案する。
また、補助公式の進行に基づく代替解法についても検討する。
- 参考スコア(独自算出の注目度): 33.806490809038415
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In this paper, we study incremental LTLf synthesis -- a form of reactive synthesis where the goals are given incrementally while in execution. In other words, the protagonist agent is already executing a strategy for a certain goal when it receives a new goal: at this point, the agent has to abandon the current strategy and synthesize a new strategy still fulfilling the original goal, which was given at the beginning, as well as the new goal, starting from the current instant. In this paper, we formally define the problem of incremental synthesis and study its solution. We propose a solution technique that efficiently performs incremental synthesis for multiple LTLf goals by leveraging auxiliary data structures constructed during automata-based synthesis. We also consider an alternative solution technique based on LTLf formula progression. We show that, in spite of the fact that formula progression can generate formulas that are exponentially larger than the original ones, their minimal automata remain bounded in size by that of the original formula. On the other hand, we show experimentally that, if implemented naively, i.e., by actually computing the automaton of the progressed LTLf formulas from scratch every time a new goal arrives, the solution based on formula progression is not competitive.
- Abstract(参考訳): 本稿では,実行中に目標が漸進的に与えられる反応合成の形式であるインクリメンタルTLLf合成について検討する。
言い換えると、主人公エージェントは、新しいゴールを受け取った時点で、既に特定のゴールのための戦略を実行している。この時点で、エージェントは現在の戦略を捨て、当初から与えられた目標をまだ満たしている新しい戦略と、現在の瞬間から始まる新しいゴールを合成しなければならない。
本稿では、インクリメンタルな合成の問題を正式に定義し、その解について研究する。
本稿では,自動合成時に構築した補助データ構造を利用して,複数のLTLf目標に対するインクリメンタルな合成を効率的に行う手法を提案する。
また,LTLf公式の進行に基づく代替解法についても検討する。
式進行が元の式よりも指数関数的に大きい式を生成できるにもかかわらず、それらの最小限のオートマトンは元の式と大きく結びついていることが示される。
一方,新たな目標が到着する度にスクラッチから進行するLTLf公式のオートマトンを実際に計算することにより,公式の進行に基づく解が競合しないことを示す。
関連論文リスト
- Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions [61.479946958462754]
エージェントが単一のユニバーサルポリシーを学習する環境であるマルチタスク強化学習(RL)について検討する。
本稿では,新世代の意味翻訳を利用したタスク埋め込み手法を提案する。
論文 参考訳(メタデータ) (2026-02-06T14:46:27Z) - Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。
提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文 参考訳(メタデータ) (2025-10-02T15:15:50Z) - Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。
合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。
我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
論文 参考訳(メタデータ) (2024-08-18T14:25:44Z) - On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts [20.14001970300658]
トップダウン決定論的オートマトン構築に基づく有限トレース(LTLf)上での線形時間論理のオンザフライフレームワークを提案する。
論文 参考訳(メタデータ) (2024-08-14T06:52:58Z) - Double-Ended Synthesis Planning with Goal-Constrained Bidirectional Search [27.09693306892583]
材料制約を始点とする合成計画の定式化について述べる。
本稿では,双方向グラフ探索方式に基づく新しいCASPアルゴリズムであるDouble-Ended Synthesis Planning (DESP)を提案する。
DESPは既存のワンステップ逆合成モデルを利用することができ、これらのワンステップモデルの性能が向上するにつれて、その性能が拡大すると予想する。
論文 参考訳(メタデータ) (2024-07-08T18:56:00Z) - SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
トピック分類,感情分析,トーン検出,ユーモアの6つのデータセットの合成について検討した。
その結果,SynthesizRRは語彙や意味の多様性,人文との類似性,蒸留性能を大幅に向上させることがわかった。
論文 参考訳(メタデータ) (2024-05-16T12:22:41Z) - ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。
本稿では,ExeDecを提案する。ExeDecは,実行サブゴールを予測し,各ステップでプログラム実行によって段階的に通知される問題を解くための,新しい分解ベースの戦略である。
論文 参考訳(メタデータ) (2023-07-26T01:07:52Z) - Forward LTLf Synthesis: DPLL At Work [1.370633147306388]
有限トレース(LTLf)上での線形時間論理の合成のための新しいAND-ORグラフ探索フレームワークを提案する。
このようなフレームワーク内では、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムにインスパイアされたプロシージャを考案し、次に利用可能なエージェント環境の動きを生成する。
また,状態公式の構文的等価性に基づく探索ノードの等価性チェックも提案する。
論文 参考訳(メタデータ) (2023-02-27T14:33:50Z) - Synthesis from Satisficing and Temporal Goals [21.14507575500482]
既存のアプローチでは、割引合成からの合成技術とDS報酬の最適化を組み合わせているが、音響アルゴリズムは得られていない。
合成と満足なDS報酬(しきい値を達成するリワード)を組み合わせた別のアプローチは、整数割引係数に対して健全で完備であるが、実際には分数割引係数が望まれる。
この研究は、DS報酬を分数割引係数で提示することから合成するための第1音素アルゴリズムへの既存の充足アプローチを拡張した。
論文 参考訳(メタデータ) (2022-05-20T23:46:31Z) - Distributed Control using Reinforcement Learning with
Temporal-Logic-Based Reward Shaping [0.2320417845168326]
本研究では,異種ロボットの分散制御戦略を部分的に観測可能な環境下で合成するためのフレームワークを提案する。
提案手法では,合成問題をゲームとして定式化し,ポリシーグラフ法を用いて各エージェントのメモリによる制御戦略を求める。
我々はTLTLの量的意味論をゲームの報酬として使用し、さらに有限状態オートマトンを用いて学習プロセスのガイドと高速化を行う。
論文 参考訳(メタデータ) (2022-03-08T16:03:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。