用于信号时序逻辑的奖励机

# 用于信号时序逻辑的奖励机器
来源：https://arxiv.org/html/2608.13625
商汤·张 余一·莫代
致谢：本工作得到了联邦网络倡议 HV\-2Q25\-035、HC\-2Q25\-033 的支持，以及弗吉尼亚中部节点在奖项 VV\-1Q26\-001 下的资助。
致谢：A\. K\. Bozkurt 和 Y\. Motai 隶属于美国弗吉尼亚州里士满市弗吉尼亚联邦大学电气与计算机工程系（电子邮件：\{bozkurta,ymotai\}@vcu\.edu），S\. Zhang 隶属于美国弗吉尼亚州夏洛茨维尔市弗吉尼亚大学计算机科学系（电子邮件：xdm2bt@virginia\.edu）。
###### 摘要
信号时序逻辑为指定实值观测的实时性质提供了一种形式化语言，并伴有用于监控满足性的定量鲁棒性评分。从 STL 规范进行控制综合具有研究意义，因为随着现实世界系统复杂度的增加，手动控制器设计变得不可行。此外，许多现代自主系统和 AI 系统缺乏精确完整的系统模型，这使得基于优化的综合方法不适用，并推动了基于学习的控制。先前的工作将 STL 鲁棒性评分用作强化学习中的奖励，以获得满足给定规范的控制策略；然而，鲁棒性依赖于执行历史，导致对于具有任意嵌套时序算子的通用长时域规范，状态空间呈棘手扩展。本文提出了一种新颖的基于自动机的方法，该方法提供了一种高效的记忆机制以及适合 RL 框架的相关马尔可夫奖励。我们的方法从给定的 STL 规范构造一个定时交替自动机，用自动机位置和时钟估值来增强状态空间，并从自动机的接受条件推导出奖励。我们通过经验表明，与使用基于鲁棒性的奖励所学策略相比，我们方法所学策略实现了更高的鲁棒性评分和满足率。
###### 索引术语：交替定时自动机、强化学习、鲁棒满足、信号时序逻辑
## I 引言
信号时序逻辑是一种用于表达实时、实值信号需求的形式化规范语言\[1 (https://arxiv.org/html/2608.13625#bib.bib1)\]。STL 将数值谓词（表示为信号值的不等式）与施加显式实时约束的度量时序算子相结合。STL 通过使用鲁棒性评分评估执行轨迹来实现系统化验证\[2 (https://arxiv.org/html/2608.13625#bib.bib2)\]，该评分不仅捕捉规范是否被满足，还捕捉满足的强度，这对于有噪声信号或不完美模型至关重要。这些特性使 STL 非常适合具有连续或混合动力学的时临界控制系统，并已成功应用于机器人\[3 (https://arxiv.org/html/2608.13625#bib.bib3)\]、交通\[4 (https://arxiv.org/html/2608.13625#bib.bib4)\]和医疗系统\[5 (https://arxiv.org/html/2608.13625#bib.bib5)\]等领域。
在过去的二十年里，STL 在许多方向上得到了扩展，包括鲁棒性的在线监测方法\[6 (https://arxiv.org/html/2608.13625#bib.bib6),7 (https://arxiv.org/html/2608.13625#bib.bib7),8 (https://arxiv.org/html/2608.13625#bib.bib8)\]以及更丰富的鲁棒性概念，这些概念不仅考虑空间扰动，还考虑时序扰动和其他形式的不确定性\[9 (https://arxiv.org/html/2608.13625#bib.bib9)\]。
尽管运行时验证对现有控制系统具有实用价值，但直接从 STL 规范综合控制器是必需的，因为对于许多现实世界系统，手动控制器设计不切实际\[10 (https://arxiv.org/html/2608.13625#bib.bib10)\]。通过优化对具有可用模型的系统从 STL 规范进行控制综合已得到广泛研究（例如，\[11 (https://arxiv.org/html/2608.13625#bib.bib11),12 (https://arxiv.org/html/2608.13625#bib.bib12),13 (https://arxiv.org/html/2608.13625#bib.bib13),14 (https://arxiv.org/html/2608.13625#bib.bib14),15 (https://arxiv.org/html/2608.13625#bib.bib15)\]）。然而，随着现代自主系统变得更加复杂并融入更多 AI 组件，适合标准优化技术的高保真模型通常不可用，因此需要数据驱动的学习。结果，越来越多的工作试图将 STL 直接整合到基于学习的控制中，利用其定量鲁棒性评分作为强化学习管道中的奖励。然而，鲁棒性评分在轨迹上的历史依赖语义违反了马尔可夫性质，这是标准 RL 框架中的一个常见假设。现有方法通过将先前访问的状态添加到状态中来解决此问题\[16 (https://arxiv.org/html/2608.13625#bib.bib16),17 (https://arxiv.org/html/2608.13625#bib.bib17)\]，这对于长时域规范来说是难以处理的；或者通过将注意力限制在 STL 的有限片段上\[18 (https://arxiv.org/html/2608.13625#bib.bib18),19 (https://arxiv.org/html/2608.13625#bib.bib19),20 (https://arxiv.org/html/2608.13625#bib.bib20),21 (https://arxiv.org/html/2608.13625#bib.bib21),22 (https://arxiv.org/html/2608.13625#bib.bib22)\]。据我们所知，目前还没有 RL 方法在考虑完整 STL 的同时，比使用整个历史进行状态增强更具可处理性。
在这项工作中，我们通过构建奖励机器来减轻 STL 满足性的历史依赖性，RM 提供了高效的记忆机制并诱导马尔可夫奖励，从而实现从 STL 规范进行基于 RL 的控制综合。我们的贡献如下：
- •我们引入了一种新颖的基于自动机的框架，用于从 STL 规范学习控制器。我们将随机控制系统建模为半马尔可夫决策过程，并采用基于事件的 STL 语义，从而能够从规范推导出单时钟交替定时自动机。
- •我们利用其接受条件从推导出的 OCATAs 构建 STL-RM，同时额外融入了对观测扰动的鲁棒性，灵感来自\[24 (https://arxiv.org/html/2608.13625#bib.bib24)\]中的可微奖励。除了提供奖励之外，我们的 RM 还维护了一个包含时钟估值的自动机位置列表，作为状态增强的记忆，这使得奖励具有马尔可夫性，并与现成的 RL 算法兼容。我们形式化证明，使用我们的 RM 学习的任何控制策略，只要达到最大累积奖励 1，就以概率 1 满足给定的 STL 规范。
- •我们表明，通过在几个模拟实验中更快地学习控制策略并在长时域规范上实现更高的满足率，我们的方法优于现有方法。
本文其余部分的组织结构如下。在第 II 节（https://arxiv.org/html/2608.13625#S2）中，我们回顾相关工作；在第 III 节（https://arxiv.org/html/2608.13625#S3）中，我们提供必要的背景信息并建立我们的符号。我们在第 V 节（https://arxiv.org/html/2608.13625#S5）介绍我们的方法，并在第 VI 节（https://arxiv.org/html/2608.13625#S6）展示我们的实验结果。最后，我们在第 VII 节（https://arxiv.org/html/2608.13625#S7）得出结论。
## II 相关工作
先前关于从 STL 规范综合控制器的工作分为两类，具体取决于是否假设系统模型可用：基于模型和无模型。我们下面讨论这两个类别中突出的方法及其缺点。详细讨论请参考\[25 (https://arxiv.org/html/2608.13625#bib.bib25)\]。
### II-A 基于模型的综合方法
先前的研究主要集中在建立混合整数规划以从 STL 规范综合控制器\[26 (https://arxiv.org/html/2608.13625#bib.bib26),27 (https://arxiv.org/html/2608.13625#bib.bib27),28 (https://arxiv.org/html/2608.13625#bib.bib28),29 (https://arxiv.org/html/2608.13625#bib.bib29)\]。一种常见的方法是利用模型预测控制，其中在每个时间步，通过基于系统动态制定的 MIP 获得有限时域上的最优控制策略；然后以滚动时域方式迭代重复此过程\[11 (https://arxiv.org/html/2608.13625#bib.bib11)\]。这种方法已扩展到最坏情况\[30 (https://arxiv.org/html/2608.13625#bib.bib30)\]、对抗性设置\[12 (https://arxiv.org/html/2608.13625#bib.bib12)\]、有扰动的系统\[31 (https://arxiv.org/html/2608.13625#bib.bib31)\]、不确定或随机环境\[32 (https://arxiv.org/html/2608.13625#bib.bib32),33 (https://arxiv.org/html/2608.13625#bib.bib33),34 (https://arxiv.org/html/2608.13625#bib.bib34)\]、弹性控制\[35 (https://arxiv.org/html/2608.13625#bib.bib35)\]、多目标\[36 (https://arxiv.org/html/2608.13625#bib.bib36)\]和无界规范\[37 (https://arxiv.org/html/2608.13625#bib.bib37)\]。这些 MPC 形式化中的一个主要问题是，较短的规划时域可能导致不理想的近视解决方案，而较长的时域则计算代价高昂。一些方法提出使用控制屏障函数来提高计算效率；然而，它们通常仅考虑 STL 的片段\[38 (https://arxiv.org/html/2608.13625#bib.bib38),3 (https://arxiv.org/html/2608.13625#bib.bib3)\]，假设线性\[39 (https://arxiv.org/html/2608.13625#bib.bib39)\]，或需要额外的可达集计算\[40 (https://arxiv.org/html/2608.13625#bib.bib40)\]。另一系列研究，例如\[41 (https://arxiv.org/html/2608.13625#bib.bib41),42 (https://arxiv.org/html/2608.13625#bib.bib42),43 (https://arxiv.org/html/2608.13625#bib.bib43),44 (https://arxiv.org/html/2608.13625#bib.bib44),45 (https://arxiv.org/html/2608.13625#bib.bib45),46 (https://arxiv.org/html/2608.13625#bib.bib46)\]，提出了鲁棒性的平滑版本以实现基于梯度的优化从而加快计算，并且也探索了通过反向传播将这些方法与神经网络结合\[47 (https://arxiv.org/html/2608.13625#bib.bib47),48 (https://arxiv.org/html/2608.13625#bib.bib48)\]。其他方法包括基于管道的\[49 (https://arxiv.org/html/2608.13625#bib.bib49),50 (https://arxiv.org/html/2608.13625#bib.bib50)\]、规定的性能控制\[51 (https://arxiv.org/html/2608.13625#bib.bib51),52 (https://arxiv.org/html/2608.13625#bib.bib52),53 (https://arxiv.org/html/2608.13625#bib.bib53)\]、时间区间分解\[54 (https://arxiv.org/html/2608.13625#bib.bib54),55 (https://arxiv.org/html/2608.13625#bib.bib55)\]、系统变换\[56 (https://arxiv.org/html/2608.13625#bib.bib56)\]，都引入了额外要求，例如对 STL 公式或系统动力学。总体而言，STL 的基于模型综合是一个活跃的研究领域，产生了许多研究。然而，STL 鲁棒性评分的历史依赖性仍是控制综合中的一个主要障碍。这种依赖性增加了 MILP 形式化中更长规划时域的计算负担，并且在通过长历史进行反向传播时可能导致梯度消失/爆炸问题。此外，所有这些方法都依赖于系统模型可用的假设，限制了其适用性。
### II-B 无模型学习方法
现代 RL 在从交互数据中直接学习奖励最大化控制器方面取得了强大的经验性能，而无需显式的动力学模型\[57 (https://arxiv.org/html/2608.13625#bib.bib57)\]。这一成功激发了将 RL 用于从 STL 规范进行控制综合，即在 RL 目标中使用鲁棒性评分作为奖励\[58 (https://arxiv.org/html/2608.13625#bib.bib58),59 (https://arxiv.org/html/2608.13625#bib.bib59),60 (https://arxiv.org/html/2608.13625#bib.bib60)\]。一个核心挑战是，满足率和鲁棒性评分是基于整个轨迹计算的，这使得它们依赖于历史，从而破坏了大多数 RL 公式所假设的马尔可夫性质。这种非马尔可夫依赖性会破坏学习的稳定性，并可能导致性能不佳，甚至发散，特别是对于基于值的方法（如 Q 学习和 Actor-Critic 算法）。一种恢复马尔可夫结构的常用技术是用访问状态的最近历史来增强状态空间，所需的历史长度由 STL 规范的时序结构决定\[16 (https://arxiv.org/html/2608.13625#bib.bib16),17 (https://arxiv.org/html/2608.13625#bib.bib17),61 (https://arxiv.org/html/2608.13625#bib.bib61),62 (https://arxiv.org/html/2608.13625#bib.bib62)\]。虽然概念简单，但这种方法可能会显著增加状态维度，由此产生的复杂性对于长时域规范来说变得难以承受。为了缓解这种爆炸式增长，几项工作将注意力限制在可处理的 STL 片段上，或引入避免完整历史增强的替代中间表示。例如，用用于有限嵌套的紧凑簿记变量增强状态\[18 (https://arxiv.org/html/2608.13625#bib.bib18),19 (https://arxiv.org/html/2608.13625#bib.bib19),20 (https://arxiv.org/html/2608.13625#bib.bib20)\]、规定的性能控制公式\[21 (https://arxiv.org/html/2608.13625#bib.bib21)\]、基于采样的规划方法\[63 (https://arxiv.org/html/2608.13625#bib.bib63)\]、使用控制屏障函数学习\[22 (https://arxiv.org/html/2608.13625#bib.bib22)\]以及基于漏斗的控制\[64 (https://arxiv.org/html/2608.13625#bib.bib64)\]。尽管取得了这些进展，但仍然没有一种无模型方法能够在扩展到完整 STL 的同时避免棘手的基于历史的状态增强。
与我们密切相关的一类工作侧重于通过将时序逻辑规范编译成自动机并在乘积系统上进行学习，从而为 RL 设计基于自动机的奖励。大多数现有方法从没有实时约束的逻辑（如线性时序逻辑）获得的 omega 自动机构建奖励，例如\[65 (https://arxiv.org/html/2608.13625#bib.bib65),66 (https://arxiv.org/html/2608.13625#bib.bib66),67 (https://arxiv.org/html/2608.13625#bib.bib67),68 (https://arxiv.org/html/2608.13625#bib.bib68),69 (https://arxiv.org/html/2608.13625#bib.bib69),70 (https://arxiv.org/html/2608.13625#bib.bib70),71 (https://arxiv.org/html/2608.13625#bib.bib71),72 (https://arxiv.org/html/2608.13625#bib.bib72),73 (https://arxiv.org/html/2608.13625#bib.bib73)\]，少数考虑为给定定时自动机进行奖励塑造\[74 (https://arxiv.org/html/2608.13625#bib.bib74)\]，这是一种扩展了具有时钟变量和时间约束的迁移系统的形式化。然而，据我们所知，先前的工作尚未以与标准 RL 设置兼容的方式，从直接从 STL 推导出的自动机构建奖励。虽然 STL 可以转换为连续时间信号转换器\[13 (https://arxiv.org/html/2608.13625#bib.bib13)\]，但这些表示与 RL 并不匹配，在 RL 中，智能体通常在离散决策时间接收逐点状态观测。在这项工作中，我们将 STL 规范转换为 OCATAs，并设计奖励以适应其合取分支结构和相关的接受条件，这可以通过增强