論文の概要: Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

• arxiv url: http://arxiv.org/abs/2604.12092v1
• Date: Mon, 13 Apr 2026 22:07:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-15 19:11:32.136006
• Title: Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis
• Title（参考訳）: 時間的行動木の3次論理エンコーディングと制御合成への応用
• Authors: Ryan Matheu, John S. Baras, Calin Belta,
• Abstract要約: テンポラルBTは、既存の時間論理形式を利用してBTの実行を特定し検証することで、有望なアプローチを提供する。 制御可能な3値信号時間論理(STL)を用いてTBTを再構成する。 本稿では,3次論理を用いた部分トラジェクトリSTLとTBTの混合整数線形符号化を提案する。
• 参考スコア（独自算出の注目度）: 5.99447754429793
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Behavior Trees (BTs) provide designers an intuitive graphical interface to construct long-horizon plans for autonomous systems. To ensure their correctness and safety, rigorous formal models and verification techniques are essential. Temporal BTs (TBTs) offer a promising approach by leveraging existing temporal logic formalisms to specify and verify the executions of BTs. However, this analysis is currently limited to offline post hoc analysis and trace repair. In this paper, we reformulate TBTs using a ternary-valued Signal Temporal Logic (STL) amenable for control synthesis. Ternary logic introduces a third truth value \textit{Unknown}, formally capturing cases where a trajectory has neither fully satisfied or dissatisfied a specification. We propose mixed-integer linear encodings for partial trajectory STL and TBTs over ternary logic allowing for correct-by-construction control strategies for linear dynamical systems via mixed-integer optimization. We demonstrate the utility of our framework by solving optimal control problems.
• Abstract（参考訳）: 振舞い木(BT)は、デザイナーが自律システムのための長期計画を構築するための直感的なグラフィカルインターフェースを提供する。 正確性と安全性を確保するため、厳密な形式モデルと検証技術が不可欠である。 TBT(Temporal BT)は、既存の時間論理形式を利用してBTの実行を特定し検証することで、有望なアプローチを提供する。 しかし、この分析は、現在オフラインのポストホック分析とトレース修復に限られている。 本稿では,制御合成に有効な3値信号時間論理(STL)を用いてTBTを再構成する。 第三の論理は第三の真理値 \textit{Unknown} を導入し、トラジェクトリが完全に満足していない場合や仕様に不満がある場合を正式にキャプチャする。 線形力学系に対する混合整数最適化により, 3次論理上の部分軌道STLおよびTBTに対する混合整数線形符号化を提案する。 最適制御問題を解くことにより,フレームワークの有用性を実証する。

関連論文リスト

• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。 本稿では,再構築による理解という,新しいパラダイムを提案する。 マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-11T09:23:20Z)
• LOGIGEN: Logic-Driven Generation of Verifiable Agentic Tasks [4.6880826836662814]
  検証可能なトレーニングデータを合成するロジック駆動フレームワークである textbfLOGIGEN を紹介する。 2$-Benchでは、LOGIGEN-32B(RL)がtextbf79.5%の成功率を獲得し、ベースモデルを大幅に上回っている。
  論文  参考訳（メタデータ） (2026-02-28T08:35:30Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。 提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
  論文  参考訳（メタデータ） (2025-10-02T15:15:50Z)
• Foundation Models for Logistics: Toward Certifiable, Conversational Planning Interfaces [59.80143393787701]
  大規模言語モデル(LLM)は不確実性に対処し、導入障壁を低くしながら再計画の加速を約束する。 本稿では,自然言語対話のアクセシビリティと目標解釈の検証可能な保証とを組み合わせたニューロシンボリック・フレームワークを提案する。 わずか100個の不確実性フィルタで微調整された軽量モデルは、GPT-4.1のゼロショット性能を上回り、推論遅延を50%近く削減する。
  論文  参考訳（メタデータ） (2025-07-15T14:24:01Z)
• LTLDoG: Satisfying Temporally-Extended Symbolic Constraints for Safe Diffusion-based Planning [12.839846486863308]
  本研究では,新しい静的かつ時間的に拡張された制約/命令に準拠する長い水平軌道を生成することに焦点を当てる。 本稿では、線形時間論理を用いて指定された命令を与えられた逆プロセスの推論ステップを変更する、データ駆動拡散に基づくフレームワーク、 finiteDoGを提案する。 ロボットナビゲーションと操作の実験では、障害物回避と訪問シーケンスを指定する公式を満たす軌道を生成することができる。
  論文  参考訳（メタデータ） (2024-05-07T11:54:22Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  本稿では,STL式を学習するニューラルネットワークシンボリックフレームワークであるTLINetを紹介する。 従来の手法とは対照的に,時間論理に基づく勾配法に特化して設計された最大演算子の近似法を導入する。 我々のフレームワークは、構造だけでなく、STL公式のパラメータも学習し、演算子と様々な論理構造の柔軟な組み合わせを可能にします。
  論文  参考訳（メタデータ） (2024-05-03T16:38:14Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Temporal Answer Set Programming [3.263632801414296]
  本稿では,その知識表現と宣言的問題解決への応用の観点から,時間論理プログラミングの概要を述べる。 本研究は,TEL(Temporal Equilibrium Logic)と呼ばれる非単調な形式論の最近の成果に焦点を当てる。 第2部では,ASP.NET に近い時間論理プログラムと呼ばれる構文的断片を定義し,この問題が解決器 TEINGO の構築においてどのように活用されたかを説明する。
  論文  参考訳（メタデータ） (2020-09-14T16:13:36Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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