論文の概要: Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions
- arxiv url: http://arxiv.org/abs/2607.18731v1
- Date: Tue, 21 Jul 2026 05:43:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-22 19:05:05.319139
- Title: Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions
- Title（参考訳）: 信号時相論理仕様からの正しい構成行動木合成とロボットミッションへの応用
- Abstract要約: 動作木(BT)は、ロボット工学における複雑なタスク実行に広く採用されている。
この文字は、Signal Temporal Logic (STL)仕様から正しい構成BTを合成する。
- 参考スコア（独自算出の注目度）: 5.524204636266904
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Behavior Trees (BTs) are widely adopted for complex task execution in robotics, providing modular, reactive control but lacking formal guarantees. However, existing correct-by-construction synthesis from Linear Temporal Logic (LTL) cannot express quantitative timing constraints. This letter synthesizes correct-by-construction BTs from Signal Temporal Logic (STL) specifications. The workspace is modeled as a timed transition system and abstracted into a zone graph, and an augmented state space tracking both logical progress and timing constraints is introduced. A hierarchical fixed-point algorithm computes winning sets for an STL fragment encompassing safety, reachability, response, recurrence, and persistence, yielding BT subtrees with a runtime constraint function. Correctness guarantees are proven and complexity bounds are derived. Simulations demonstrate specification satisfaction with strictly positive robustness, and a physical quadrotor experiment with six STL specifications validates practical deployability.
- Abstract（参考訳）: 動作木(BT)は、ロボット工学における複雑なタスク実行に広く採用されており、モジュラーでリアクティブな制御を提供するが、正式な保証はない。
しかし,LTL(Linear Temporal Logic)からの既存の正しい構成合成では,時間的制約を定量的に表現することはできない。
この文字は、Signal Temporal Logic (STL)仕様から正しい構成BTを合成する。
ワークスペースはタイムトトランジションシステムとしてモデル化され、ゾーングラフに抽象化され、論理的進行とタイミング制約の両方を追跡する拡張状態空間が導入された。
階層的固定点アルゴリズムは、安全性、到達性、応答性、繰り返し性、永続性を含むSTLフラグメントの勝利集合を計算し、実行時制約関数を持つBTサブツリーを生成する。
正確性保証が証明され、複雑性境界が導出される。
シミュレーションでは、厳密な正のロバスト性を持つ仕様満足度が示され、6つのSTL仕様を持つ物理的四重項実験が実用的デプロイ可能性を検証する。
関連論文リスト
- An Operator-Based Approach to STL [10.103844123344057]
本稿では,到達可能性値関数に作用する演算子に基づく信号時間論理(STL)に対する新しいアプローチを提案する。
これは、複雑なマルチネスト式を扱うための新しい理論的枠組みを構成する。
STLに基づくリーチビリティ関数の設計に重点を置くのとは対照的に,我々は演算子ベースのネストルールを開発する。
論文 参考訳（メタデータ） (2026-05-27T07:47:45Z) - Signal Temporal Logic Motion Planning via Graphs of Convex Sets [8.443328067924298]
本稿では,STL(Signal Temporal Logic)仕様の下での連続的な動作計画について検討する。
本稿では,時間自動推論と凸集合のグラフを組み合わせたフレームワークを提案する。
低次元のベンチマークの数値実験、$$Drotor、$30$DoFのヒューマノイド、UR-3ロボットアームのハードウェア実験は、提案手法が複雑なSTL動作計画問題を効率的に解くことを実証している。
論文 参考訳（メタデータ） (2026-05-22T05:19:43Z) - How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
我々は,認知理論に触発された問題解決性に基づく新しい誤り分類法を導入する。
我々の分類学は、障害を構文、意味、解決可能な機能、解決不可能な機能タイプに分類する。
論文 参考訳（メタデータ） (2026-04-26T14:34:49Z) - Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis [5.99447754429793]
テンポラルBTは、既存の時間論理形式を利用してBTの実行を特定し検証することで、有望なアプローチを提供する。
制御可能な3値信号時間論理(STL)を用いてTBTを再構成する。
本稿では,3次論理を用いた部分トラジェクトリSTLとTBTの混合整数線形符号化を提案する。
論文 参考訳（メタデータ） (2026-04-13T22:07:05Z) - Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
本研究では,大規模状態空間を持つ決定過程(MDP)における非マルコフ報酬の論理的仕様に関する新しい枠組みを提案する。
我々のアプローチは有限トレース(LTLfMT)上での線形時間論理モデュロ理論を利用する
本稿では,報酬マシンとHER(Hindsight Experience Replay)をベースとした一階述語論理仕様の翻訳手法を提案する。
論文 参考訳（メタデータ） (2026-02-05T22:11:28Z) - Zero-Shot Instruction Following in RL via Structured LTL Representations [54.08661695738909]
リニア時間論理(LTL)は、強化学習(RL)エージェントのための複雑で構造化されたタスクを特定するための魅力的なフレームワークである。
近年の研究では、命令を有限オートマトンとして解釈し、タスク進捗を監視する高レベルプログラムと見なすことができ、テスト時に任意の命令を実行することのできる1つのジェネラリストポリシーを学習できることが示されている。
本稿では,この欠点に対処する任意の命令に従うために,マルチタスクポリシーを学習するための新しいアプローチを提案する。
論文 参考訳（メタデータ） (2025-12-02T10:44:51Z) - Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。
提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文 参考訳（メタデータ） (2025-10-02T15:15:50Z) - AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
Autoは、クローズドループの自己検証プロセスをデュアルシステムフレームワークに統合する、完全に自動化された方法である。
Autoの有効性は8つの異なるシナリオで検証され、SOTA法よりも10.1%改善された。
論文 参考訳（メタデータ） (2025-07-06T08:35:22Z) - STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification [9.039665244779185]
STLCG++は、STL計算と時間ステップ間のバックプロパゲーションを並列化するマスキングベースのアプローチである。
また、時間間隔境界の微分を可能にするスムース化手法を導入し、勾配に基づく最適化タスクにおけるSTLの適用性を拡大する。
論文 参考訳（メタデータ） (2025-01-08T00:06:43Z) - DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL [59.01527054553122]
線形時間論理(LTL)は、最近、複雑で時間的に拡張されたタスクを特定するための強力なフォーマリズムとして採用されている。
既存のアプローチにはいくつかの欠点がある。
これらの問題に対処するための新しい学習手法を提案する。
論文 参考訳（メタデータ） (2024-10-06T21:30:38Z) - LTLDoG: Satisfying Temporally-Extended Symbolic Constraints for Safe Diffusion-based Planning [12.839846486863308]
本研究では,新しい静的かつ時間的に拡張された制約/命令に準拠する長い水平軌道を生成することに焦点を当てる。
本稿では、線形時間論理を用いて指定された命令を与えられた逆プロセスの推論ステップを変更する、データ駆動拡散に基づくフレームワーク、 finiteDoGを提案する。
ロボットナビゲーションと操作の実験では、障害物回避と訪問シーケンスを指定する公式を満たす軌道を生成することができる。
論文 参考訳（メタデータ） (2024-05-07T11:54:22Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。