基于嵌入时序逻辑的感知自主系统运行时监控

# 基于嵌入时态逻辑的感知型自主系统运行时监控
来源：https://arxiv.org/html/2605.12651
Parv Kapoor 卡内基梅隆大学软件与社会系统系 parvk@andrew\.cmu\.edu &Abigail Hammer∗ 卡内基梅隆大学软件与社会系统系 arhammer@andrew\.cmu\.edu Ashish Kapoor Scaled Foundations ashish@generalrobotics\.company &Karen Leung 华盛顿大学航空与航天系 kymleung@uw\.edu &Eunsuk Kang 卡内基梅隆大学软件与社会系统系 eunsukk@andrew\.cmu\.edu

###### 摘要

自主系统的运行时监控传统上依赖于将连续的传感器观测映射到定义在低维状态变量上的离散逻辑命题。这种抽象在感知驱动场景中失效，因为此类映射需要额外的学习模块，这些模块通常计算昂贵、脆弱且语义不对齐。在本文中，我们提出*嵌入时态逻辑*（ETL），一种直接在学习的嵌入空间中进行监控的时态逻辑。ETL通过观测嵌入与从参考观测中导出的目标嵌入之间的距离来定义谓词。这种表述使得规约能够捕捉高层感知概念，例如与视觉目标的相似性或语义区域的避让，这些概念难以或无法使用传统谓词来表达。通过将这些谓词与时态算子组合，ETL自然表达了时间延展和顺序性的感知行为。我们介绍了用于在有界嵌入轨迹上评估规约的ETL监视器，以及一种提供可靠且面向安全的谓词评估的共形校准过程。我们在多个操作环境中评估了我们的方法，结果显示ETL与真实语义具有强经验一致性，包括对时态组合行为的准确监控。

## 1 引言

从自动驾驶汽车到机器人操作器，现代自主系统越来越依赖学习到的表示来进行感知、预测和决策（hafner2020dreamer;tdmpc2;Zhou等，2025（https://arxiv.org/html/2605.12651#bib.bib42）；kim24openvla;intelligence2025pi06vlalearnsexperience;ye2026worldactionmodelszeroshot）。这些表示使自主系统能够克服在显式状态空间表示（如物体位姿和速度）上运行的挑战，因为这些显式表示通常需要状态估计流水线和辅助定位模块。我们将基于学习表示运行的系统称为*感知型系统*。感知型系统将高维传感器流（如图像、视频或激光雷达）映射到紧凑的潜在表示，然后由下游策略、规划器或世界模型使用（nvidia2026worldsimulationvideofoundation;baniodeh2025scalinglawsmotionforecasting）。

实现高可信度自主性的一种有前景的方法涉及正式规约系统的期望属性，并应用形式化验证（verification-survey2019）和运行时监控（Maler和Nickovic,2004（https://arxiv.org/html/2605.12651#bib.bib10））等技术来检查系统是否满足这些属性（Seshia等，2018（https://arxiv.org/html/2605.12651#bib.bib3））。特别是，*运行时监控*引起了广泛兴趣，因为它可以*在线*部署，以提供关于系统行为的严格保证，而无需承担穷举离线分析的成本。运行时监视器定期评估系统的执行情况，并在系统表现出不良行为时发出警报（Colombo和Pace,2022（https://arxiv.org/html/2605.12651#bib.bib86））。这种提供轻量级但严格在线保证的能力导致了在自动驾驶车辆（schon2026spatiotemporal）、无人机（gu2023successful）和机器人操作器（8836933）等领域的成功应用。

运行时监控依赖于*形式规约*的可用性，这些规约捕捉系统的期望属性。对于具有低维状态表示的系统，规约表示法如信号时态逻辑（STL）（Maler和Nickovic,2004（https://arxiv.org/html/2605.12651#bib.bib10））提供了一种表达性形式体系，用于在逻辑*谓词*上指定行为属性。每个谓词编码一个关于状态变量的条件，可以在执行的每一步评估为真或假，例如，其位置、速度或力是否低于或高于给定阈值。

然而，对于感知型系统，在学习的表示上编写这样的形式规约仍然是一个开放挑战（Seshia等，2018（https://arxiv.org/html/2605.12651#bib.bib3））。对于这些系统，低维状态表示通常不可用，或者需要专门的临时感知模块。例如，将“机器人靠近障碍物”或“夹爪夹持物体”等属性转化为谓词，需要额外的分类器或检测器，或者为任务定制的手工特征提取器（例如，检测当前场景中是否存在夹爪“夹持”物体的概念）（Hekmatnejad等，2024（https://arxiv.org/html/2605.12651#bib.bib89））。添加这些模块可能会引入新的脆弱性来源、校准误差和领域依赖性。更糟糕的是，每当规约的概念词汇变化时（例如，为了也能表达关于夹爪“掉落”物体的属性），可能需要增强现有的感知模块或添加新模块来支持新概念。总体而言，存在一个*根本性不匹配*：一方面（i）典型感知系统运行的潜在空间，另一方面（ii）现有时态逻辑表示法中规约所表达的低维状态空间。

本文提出了一种新方法，用于正式规约和监控感知型自主系统的行为属性。关键思想是将*嵌入*（观测的预训练向量表示）作为规约中的一等概念，并根据*目标嵌入*（系统与之交互的真实世界概念的理想表示）与*观测嵌入*（系统执行期间由编码器从传感器观测生成的表示）之间的距离来表达属性。其核心洞见是：*预训练编码器已经将语义邻近性嵌入几何中*（Radford等，2021（https://arxiv.org/html/2605.12651#bib.bib11）；Oquab等，2024（https://arxiv.org/html/2605.12651#bib.bib95））：语义相似场景的观测映射到潜在空间中邻近的向量。这使得感知属性可以直接表达为几何谓词；例如，“靠近障碍物”可以表示为“‖zt−zobstacle‖2\\\|z\_\{t\}\-z\_\{\\mathrm\{obstacle\}\}\\\|\_\{2\}较小”，其中zobstaclez\_\{\\mathrm\{obstacle\}\}是障碍物参考图像的编码器表示，ztz\_\{\\mathrm\{t\}\}是当前场景图像的编码。然后，可以通过组合多个基于嵌入的谓词来构建表达性的时态逻辑规约，并用作运行时监视器的一部分，以确保系统满足其期望属性（例如，“如果夹爪夹持物体，则在物体被移动到投递箱之前不会掉落物体”）。

尽管这个想法在概念上很简单，但使其适用于形式规约面临多个挑战。首先，如何生成目标嵌入的问题：它们可以来自参考图像、演示或两者的集合，不同的选择可能产生有意义的谓词差异。此外，嵌入是学习的、连续的且依赖模型的表示，几何邻近性并不保证与监控所需的逻辑区分完全对齐。因此，一个核心挑战是将嵌入空间相似性转化为定义明确的规约基元：必须决定哪些几何关系对应谓词满足，如何校准决策阈值，以及如何组合这些谓词以创建系统规约。这些问题使得基于嵌入的规约比简单地在现有监视器内重用学到的特征更具挑战性。

在本文中，我们做出以下四项贡献：（i）引入了*嵌入时态逻辑*（ETL），一种直接在观测上指定感知行为的时态逻辑（第3.1节（https://arxiv.org/html/2605.12651#S3.SS1））；（ii）正式定义了有界嵌入轨迹上的布尔满足语义，从而得到一个用于感知规约的在线监视器（第3.1节（https://arxiv.org/html/2605.12651#S3.SS1）和3.2节（https://arxiv.org/html/2605.12651#S3.SS2））；（iii）提出了校准嵌入谓词阈值的数据驱动方法，使其适用于面向安全的监控（第4节（https://arxiv.org/html/2605.12651#S4））；（iv）在导航和操作领域评估了基于ETL的监视器，显示它们能够在不同环境中忠实地监控原子性和顺序性的感知行为（第5节（https://arxiv.org/html/2605.12651#S5））。

## 2 背景与相关工作

#### 机器人系统的形式规约

时态逻辑，如线性时态逻辑（LTL）、STL和度量时态逻辑（MTL）已被用于形式化验证信息物理系统和机器人系统中的复杂行为。这些逻辑已被用于轨迹规划（Kress-Gazit等，2009（https://arxiv.org/html/2605.12651#bib.bib79）；Sun等，2022（https://arxiv.org/html/2605.12651#bib.bib63）；Leung等，2023（https://arxiv.org/html/2605.12651#bib.bib52））、强化学习（Aksaray等，2016（https://arxiv.org/html/2605.12651#bib.bib66）；Alur等，2023（https://arxiv.org/html/2605.12651#bib.bib82）；Aloor等，2023（https://arxiv.org/html/2605.12651#bib.bib73））、运行时监控（Bartocci等，2018（https://arxiv.org/html/2605.12651#bib.bib49））和自适应控制（Raman等，2014（https://arxiv.org/html/2605.12651#bib.bib37）；Belta和Sadraddini,2019（https://arxiv.org/html/2605.12651#bib.bib57）；Lindemann和Dimarogonas,2019（https://arxiv.org/html/2605.12651#bib.bib68）；Kapoor等，2025（https://arxiv.org/html/2605.12651#bib.bib96））。这些逻辑在处理依赖ML进行感知的系统时可能遇到困难，因为输入数据中的物体数量可变且边界框不断变化。最近，引入了时空感知逻辑（STPL）（Hekmatnejad等，2024（https://arxiv.org/html/2605.12651#bib.bib89）），它将定时质量时态逻辑（Dokhanchi等，2018（https://arxiv.org/html/2605.12651#bib.bib88））与空间逻辑结合，允许对对象进行量化以及2D和3D空间推理。

#### 预训练视觉编码器

表示学习的最新进展产生了预训练视觉编码器，它们具有足够的表达能力，可以作为跨广泛视觉领域的通用感知表示（Oquab等，2024（https://arxiv.org/html/2605.12651#bib.bib95））。因此，这些模型为将时态逻辑扩展到低维状态空间表示之外提供了实用基础。预训练视觉编码器如CLIP（Radford等，2021（https://arxiv.org/html/2605.12651#bib.bib11））和DINOv2（Oquab等，2024（https://arxiv.org/html/2605.12651#bib.bib95））提供了一个共享嵌入空间，可以在其中测量感知相似性，使其成为定义基于观测的规约谓词的自然选择。

#### 基于规约的运行时监控

给定一个在有界轨迹上定义良好且编码了期望系统属性的逻辑规约，运行时监视器是在执行过程中每个时间步进行的在线评估，以判断执行是否满足给定规约（Maler和Nickovic,2004（https://arxiv.org/html/2605.12651#bib.bib10）；Bartocci等，2018（https://arxiv.org/html/2605.12651#bib.bib49））。在实践中，运行时监控通常超越布尔判决，采用定量语义，例如时态逻辑中的*鲁棒性*度量，它提供一个实值信号，指示轨迹满足或违反规约的程度（Fainekos和Pappas,2009（https://arxiv.org/html/2605.12651#bib.bib9））。这些定量监视器在连续和随机系统中特别有用，因为它们提供分级反馈，并且可以集成到优化或控制算法中以进行实时决策。

#### 共形预测

共形预测（10.5555/1062391）是一种无分布校准框架，它仅在*可交换性*假设下，将留出的校准集转化为有限样本统计保证。数据可交换性意味着校准和测试样本同分布且顺序无关。概括而言，它是一种校准模型的方法，使得模型在未见示例上的预测具有可靠性保证。我们在第4节（https://arxiv.org/html/2605.12651#S4）中使用共形预测理论来校准ETL谓词的阈值。

## 3 嵌入时态逻辑

参考图题图 1：基于嵌入的运行时监控概览。上：目标观测OG=\{og1,...,ogn\}O\_\{G\}=\\\{o\_\{g1\},\\dots,o\_\{gn\}\\\}和在线观测oto\_\{t\}由预训练视觉编码器编码为目标嵌入zGz\_\{G\}和当前嵌入ztz\_\{t\}。然后，嵌入谓词评估ztz\_\{t\}是否到达目标集。左下：嵌入轨迹投影到其前两个主成分上，显示其相对于目标嵌入的演变。右下：运行时监控随时间计算ztz\_\{t\}到zGz\_\{G\}的距离，使用ε\\epsilon对其阈值化，并评估时态逻辑规约。### 3.1 语法与语义

在我们的方法中，感知型系统被假定在其执行的每一步通过传感器（例如，摄像头）对真实世界进行观测。然后，该观测通过编码器转化为嵌入。我们形式化地将这样的系统建模为*嵌入时态结构*。

###### 定义 1（嵌入时态结构）。

一个*嵌入时态结构*是一个元组

M≡\(S,O,Z,φobs,ψenc,DZ,APz\)，\\mathcal\{M\}\\equiv\(\\mathcal\{S\},\\mathcal\{O\},\\mathcal\{Z\}\{\},\\phi\_\{obs\},\\psi\_\{enc\},D\_\{\\mathcal\{Z\}\{\}\},AP\_\{z\}\)，其中S,O,Z\\mathcal\{S\},\\mathcal\{O\},\\mathcal\{Z\}\{\}分别表示真实状态、观测和嵌入空间的集合；φobs:S→O\\phi\_\{obs\}:\\mathcal\{S\}\\to\\mathcal\{O\}是将真实状态映射到给定传感器可观测状态的观测函数；ψenc:O→Z\\psi\_\{enc\}:\\mathcal\{O\}\\to\\mathcal\{Z\}\{\}是将观测转化为嵌入的嵌入函数；DZD\_\{\\mathcal\{Z\}\{\}\}是允许的距离/相似性函数d:Z×Z→R≥0d:\\mathcal\{Z\}\{\}\\times\\mathcal\{Z\}\{\}\\to\\mathbb\{R\}\_\{\\geq 0\}的集合；APzAP\_\{z\}是嵌入谓词的集合（定义5（https://arxiv.org/html/2605.12651#Thmdefinition5））。

从概念上讲，zz是潜在变量的近似；即世界的状态，它只是i