強化学習/時相論理2026/8/13arXiv:2608.13625

信号時相論理のための報酬機械

Reward Machines for Signal Temporal Logic

信号時相論理（STL）仕様を強化学習で満たすための、オートマトンに基づく効率的な記憶機構とマルコフ報酬を導入し、既存のロバスト性報酬より高い満足率とロバスト性を達成した。

詳しい要約

1. どんなもの？

本論文は、Signal Temporal Logic (STL) 仕様を満たす制御ポリシーを強化学習 (RL) で学習するための、オートマトンに基づく新しい報酬設計手法を提案している。STL の定量的ロバスト性スコアを報酬として直接用いる既存手法は、ロバスト性が実行履歴に依存するため、長期的な仕様や任意にネストした時間演算子を含む場合に状態空間が爆発し非効率である。提案手法は、STL 仕様から timed alternating automaton を構築し、オートマトンの状態とクロック値を RL の状態に追加することで、マルコフ性を持つ報酬を導出する。これにより、履歴全体を保持することなく効率的に学習できる。

2. 先行研究と比べてどこがすごい？

先行研究では、STL のロバスト性スコアをそのまま RL の報酬として使用していたが、ロバスト性は実行履歴に依存するため、状態空間が非マルコフ的になり、長期的な仕様や複雑な時間演算子を含む場合に状態空間が爆発する問題があった。提案手法は、オートマトンを用いて必要な履歴情報を有限状態のメモリに圧縮し、マルコフ報酬を構成することで、この問題を解決している。これにより、より長い時間軸の仕様や複雑なネスト構造を持つ仕様に対しても、効率的に学習可能である点が優れている。

3. 技術・手法の肝は？

手法の核は、STL 仕様から timed alternating automaton を構築し、そのオートマトンの状態とクロック値を RL の状態空間に追加することである。具体的には、STL 式を timed alternating automaton に変換し、各時点でのオートマトンの状態遷移とクロック値を監視することで、仕様の充足度を表すマルコフ報酬を定義する。報酬はオートマトンの受理条件から導出され、履歴全体を保持する代わりにオートマトンの状態とクロック値のみで十分となる。これにより、状態空間の拡大を抑えつつ、仕様の時間的制約を正確に捉える。

4. どうやって有効だと検証した？

実験では、提案手法と既存のロバスト性ベースの報酬を用いた RL 手法を比較し、学習されたポリシーのロバスト性スコアと仕様充足率を評価している。具体的な環境や仕様の詳細は要旨からは不明だが、提案手法が既存手法よりも高いロバスト性スコアと充足率を達成したと報告されている。

5. 議論はある？

要旨からは、提案手法の限界や課題についての議論は不明である。ただし、オートマトン構築の複雑さや、クロック値の連続性による状態空間の扱い、実環境でのスケーラビリティなどが潜在的な課題として考えられるが、要旨には記載がない。

6. 次に読むべき論文は？

要旨で参照されている先行研究として、STL のロバスト性スコアを RL 報酬として用いる研究が挙げられる。具体的な論文名は不明だが、関連する分野の定番として、Signal Temporal Logic のロバスト性評価に関する研究や、LTL (Linear Temporal Logic) を報酬に変換するオートマトン手法 (e.g., LTL to DFA) を扱った論文が参考になる。

※ AIが要旨から生成した要約です。正確性は原文をご確認ください。

著者: Alper Kamil Bozkurt, Shangtong Zhang, Yuichi Motai

分類: cs.AI, cs.LG, cs.RO

原文アブストラクト

Signal temporal logic (STL) provides a formal language for specifying real-time properties of real-valued observations, along with a quantitative robustness score for monitoring satisfaction. Control synthesis from STL specifications is of interest since manual controller design becomes infeasible as real-world systems grow in complexity. Moreover, many modern autonomous and AI-enabled systems lack accurate and complete system models, which makes optimization-based synthesis approaches unsuitable and motivates learning-based control. Prior work uses STL robustness scores as rewards in reinforcement learning (RL) to obtain control policies satisfying given specifications; however, robustness depends on execution history, leading to intractable state space expansion for general long-horizon specifications with arbitrarily nested temporal operators. This work introduces a novel automata-based approach that provides an efficient memory mechanism and associated Markovian rewards suitable for RL frameworks. Our approach constructs a timed alternating automaton from the given STL specifications, augments the state space with automaton locations and clock valuations, and derives rewards from the automaton acceptance condition. We empirically demonstrate that our approach learns policies that achieve higher robustness scores and satisfaction rates than those learned by existing approaches using robustness-based rewards.

arXivで原文を読む →arXiv概要ページ

← 論文一覧