論文の概要: Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming
- arxiv url: http://arxiv.org/abs/2606.30820v2
- Date: Sun, 05 Jul 2026 18:15:16 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-07 17:33:48.63706
- Title: Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming
- Title（参考訳）: 混合整数線形計画法による時間窓時間論理仕様のロバストネスに基づく合成
- Authors: Philip Smith, Ahmad Ahmad, Kevin Leahy,
- Abstract要約: Time Window Temporal Logic (TWTL)は、サイバー物理システムのためのリッチな仕様言語である。
本稿では,TWTLタスク仕様に基づく離散時間線形システムの制御入力の合成問題について考察する。
- 参考スコア（独自算出の注目度）: 2.3559161556025887
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Time Window Temporal Logic (TWTL) is a rich specification language for cyber-physical systems that can compactly express sequential tasks with explicit timing constraints. In this paper, we consider the problem of synthesizing control inputs for discrete-time linear systems subject to TWTL task specifications. Building on the quantitative semantics (robustness) recently introduced for TWTL in [1], we encode the robust satisfaction of a TWTL formula as a set of Mixed-Integer Linear constraints and pose synthesis as a Mixed Integer Linear Program (MILP) that maximizes the robustness degree. We prove that any feasible solution with positive objective value guarantees Boolean satisfaction of the specification. We address two synthesis settings: an \emph{open-loop} formulation that optimizes the full control sequence from the initial state, and a \emph{closed-loop} receding-horizon Model Predictive Controller (MPC) formulation that re-solves the MILP at each step using the current measured state. A key feature of our MPC formulation is a \emph{task-adaptive horizon} that exploits the TWTL Deterministic Finite Automaton (DFA) to determine the active sub-task at each step, limiting the prediction horizon to the remaining window of the current task rather than the full formula horizon, this makes each re-solve significantly cheaper than the initial open-loop solve.
- Abstract（参考訳）: Time Window Temporal Logic (TWTL)は、サイバー物理システムのためのリッチな仕様言語であり、明確なタイミング制約で連続的なタスクをコンパクトに表現できる。
本稿では,TWTLタスク仕様に基づく離散時間線形システムの制御入力の合成問題について考察する。
最近TWTLで導入された量的意味論(ロバストネス)に基づいて、TWTL式を混合整数線形制約の集合として強靭な満足度を符号化し、剛性度を最大化する混合整数線形プログラム(MILP)として合成する。
肯定的な客観的価値を持つ実現可能なソリューションが、仕様のブール満足度を保証することを証明します。
初期状態から全制御シーケンスを最適化する \emph{open-loop} の定式化と、現在の測定値を用いて各ステップでMILPを再解決する \emph{closed-loop} Reeding-Horizon Model Predictive Controller (MPC) の定式化である。
我々のMPC定式化の重要な特徴は、TWTL決定論的有限オートマトン(DFA)を利用して各ステップでアクティブなサブタスクを決定することであり、予測の地平線は全公式の地平線よりも現在のタスクの残りのウィンドウに制限されているため、各解は初期開ループ解よりも大幅に安価である。
関連論文リスト
- 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) - SGA-MCTS: Decoupling Planning from Execution via Training-Free Atomic Experience Retrieval [74.1918709002557]
我々は, LLM計画を非パラメトリック検索として活用するフレームワークである textbfSGA-MCTS を紹介する。
オンラインでは、検索増強剤は、関連するステート-ゴール-アクション原子を取得するために、ハイブリッドシンボリック-セマンティック機構を使用する。
SGA-MCTSは、探索の重い計算コストを効果的に減らし、System 1推論速度におけるシステム2推論の深さを達成し、スケーラブルかつリアルタイムに自律的な計画が実現可能である。
論文 参考訳（メタデータ） (2026-04-16T07:22:36Z) - MAny: Merge Anything for Multimodal Continual Instruction Tuning [52.50936513604062]
textbfMAny(textbfMAny)は、textbfCross-modal textbfProjection textbfMergingを通じてタスク固有の知識を統合するフレームワークである。
textbfLow-rank textbfParameter textbfMerging (textbfLPM)
論文 参考訳（メタデータ） (2026-04-15T15:57:23Z) - RRT$^η$: Sampling-based Motion Planning and Control from STL Specifications using Arithmetic-Geometric Mean Robustness [7.121834057343983]
RRT$は,時間点とサブ形式をまたいだロバストネス対策を統合するサンプリングベースの計画フレームワークである。
誘導信号が制限されたマルチ制約シナリオにおいて,従来のSTLロバスト性に基づくプランナよりも優れた性能を示す。
論文 参考訳（メタデータ） (2026-02-18T19:45:43Z) - QTIS: A QAOA-Based Quantum Time Interval Scheduler [0.22940141855172033]
提案手法は、アンシラ支援量子回路を統合し、重なり合うタスクを動的に検出し、ペナルティ化する。
その結果、コンフリクトを最小限に抑えつつ、固定時間窓を用いたスケジューリング作業におけるQTISの有効性を確認した。
論文 参考訳（メタデータ） (2025-11-19T16:29:14Z) - Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。
提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文 参考訳（メタデータ） (2025-10-02T15:15:50Z) - Stochastic Approximation with Delayed Updates: Finite-Time Rates under Markovian Sampling [73.5602474095954]
マルコフサンプリングの遅延更新による近似スキームの非漸近的性能について検討した。
我々の理論的な発見は、幅広いアルゴリズムの遅延の有限時間効果に光を当てた。
論文 参考訳（メタデータ） (2024-02-19T03:08:02Z) - Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
システム実行から形式仕様を自動合成する問題を考察する。
時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。
我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
論文 参考訳（メタデータ） (2023-10-26T14:13:15Z) - Stochastic Finite State Control of POMDPs with LTL Specifications [14.163899014007647]
部分的に観測可能なマルコフ決定プロセス(POMDP)は、不確実性の下での自律的な意思決定のためのモデリングフレームワークを提供する。
本稿では,POMDPに対する準最適有限状態制御器(sFSC)の合成に関する定量的問題について考察する。
本稿では,sFSC サイズが制御される有界ポリシアルゴリズムと,連続的な繰り返しにより制御器の性能が向上する任意の時間アルゴリズムを提案する。
論文 参考訳（メタデータ） (2020-01-21T18:10:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。