面向信号时序逻辑的奖励机
文章背景与核心概要
信号时序逻辑（STL）为规范实时属性提供了形式化语言，并可通过定量鲁棒性得分来监测满足情况。尽管先前的研究将 STL 鲁棒性得分用作强化学习（RL）中的奖励以综合控制策略，但这些鲁棒性得分依赖于执行历史，导致针对长期规范时出现难以处理的状态空间膨胀。
本文引入了一种新颖的基于自动机的框架，为强化学习量身定制了高效的记忆机制和马尔可夫奖励。通过从给定的 STL 规范构建定时交替自动机（将状态空间扩充为自动机位置和时钟赋值，并直接从接受条件中推导奖励），该方法成功学习到了比现有基于鲁棒性的奖励方法具有更高鲁棒性得分和满足率的策略。
Metadata
- arXiv ID: arXiv:2608.13625 [cs.AI]
- Subjects: 人工智能 (
cs.AI); 机器学习 (cs.LG); 机器人学 (cs.RO) - Authors: Alper Kamil Bozkurt, Shangtong Zhang, Yuichi Motai
- Submission Date: 13 August 2026
- DOI: 10.48550/arXiv.2608.13625
Abstract
信号时序逻辑（STL）为规范实值观测的实时属性提供了一种形式化语言，并提供了一个用于监测满足情况的定量鲁棒性得分。随着真实世界系统复杂性的增加，手动设计控制器变得不可行，因此从 STL 规范进行控制综合备受关注。此外，许多现代自主系统和启用人工智能的系统缺乏准确且完整的系统模型，这使得基于优化的综合方法不再适用，并推动了基于学习的控制的发展。先前的工作在强化学习（RL）中使用 STL 鲁棒性得分作为奖励，以获得满足给定规范的控制策略；然而，鲁棒性取决于执行历史，导致对于具有任意嵌套时序算子的通用长期规范，会出现难以处理的状态空间膨胀。本工作引入了一种新颖的基于自动机的方法，该方法提供了一种高效的记忆机制以及适合 RL 框架的相关马尔可夫奖励。我们的方法从给定的 STL 规范构建定时交替自动机，用自动机位置和时钟赋值扩充状态空间，并从自动机接受条件中推导奖励。我们通过实验证明，我们的方法所学习到的策略比现有使用基于鲁棒性奖励的方法实现了更高的鲁棒性得分和满足率。
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.
