The complexity of being monitorable

技术摘要：可监测性的复杂性

问题陈述
运行时验证（Runtime Verification, RV）依赖于合成监视器，以确定系统执行是否满足或违反了规范。一个核心挑战是可监测性（monitorability）：即规范是否允许合成一个能够基于观测执行最终达到判定结果（满足或违反）的监视器。虽然对于特定的规范语言，可监测性通常在语法层面进行研究，但 Diekert 和 Leucker [DL14] 提出了一种语义化的拓扑方法。在该框架下，系统行为是拓扑空间 $X$ 中的点，而观测则是开集。一个属性（子集 $A \subseteq X$）是可监测的，如果对于每一个非空开观测 $U$，都可以将其细化为一个非空的 $V \subseteq U$，使得 $V$ 完全包含在 $A$ 中或完全包含在其补集中。

本文研究了可监测集合族 $M(X)$ 的描述集合论复杂度，将其视为幂集 $\mathcal{P}(X)$ 的一个子集。具体而言，作者研究了判断一个任意的计数空间 $X$ 的子集是否为可监测集的难度如何。他们根据 $X$ 的拓扑性质，分析了 $M(X)$ 在 Borel 层级和射影层级中的位置。

方法论
作者使用了来自描述集合论 [Kec95] 和 Wadge 还原的工具。

1. 拓扑设置： 他们通过特征函数将 $\mathcal{P}(X)$ 与 Cantor 空间 $2^X$ 对应起来，并赋予乘积拓扑。由于 $X$ 是可数的，因此 $\mathcal{P}(X)$ 是一个 Polish 空间。
2. 可监测性的刻画： 他们利用了如下刻画：一个集合 $A$ 是可监测的，当且仅当其边界的内部为空（$\text{Int}(\text{Fr}(A)) = \emptyset$）。这等价于说 $A$ 在任何非空开集中都不可能既是稠密又是共稠的。
3. 复杂度分析： 他们通过确定 $M(X)$ 是否属于特定的点类（$\Sigma^0_\alpha, \Pi^0_\alpha, \Sigma^1_1, \Pi^1_1$）以及是否为这些类的完全集，来对 $M(X)$ 进行分类。这涉及构造从已知困难集（例如 $\Sigma^0_3$-完全集或 $\Pi^1_1$-完全集）到 $M(X)$ 的连续还原。
4. 情况区分： 分析分为两个主要情况：
   • 第二可数空间： $X$ 具有可数基。
   • 非第二可数空间： $X$ 是可数的但缺乏可数基。

核心贡献与结果

1. 第二可数情况
对于一个可数的、第二可数的拓扑空间 $X$，集合族 $M(X)$ 始终是 $\mathcal{P}(X)$ 的一个 $\Pi^0_3$ 子集。论文提供了 $M(X)$ 可能达到的精确复杂度的分类：

• $\Delta^0_1$ (Clopen/既开又闭)： 当 $M(X) = \mathcal{P}(X)$ 时发生，这当且仅当孤立点的集合在 $X$ 中是稠密的。
• $\Sigma^0_2$-完全： 发生在如可数集上的余有限拓扑（cofinite topology）等空间中。
• $\Pi^0_3$-完全： 发生在如带有特定偏序关系的 $\mathbb{N}^2$ 上的 Alexandrov 拓扑等空间中。
• 不可能结果： 作者证明了对于第二可数空间，$M(X)$ 不可能是 $\Sigma^0_1$-完全的、$\Delta^0_2$-尖锐的（sharp）或 $\Pi^0_2$-完全的。

一个关键的操作准则被推导出来（注 3.15）：$M(X)$ 是 $\Pi^0_3$-完全的，当且仅当在移除所有极小非空开集的并集后，剩余的内部包含无限多个两两不相交的开子集。否则，$M(X)$ 是 $\Sigma^0_2$。

2. 对转移关系的适用性
作者将这些结果应用于由可数状态集（模拟分支时间系统）上的转移关系诱导的拓扑。他们定义 $R_0$ 为诱导 $\Sigma^0_2$ 可监测集合族的转移关系集合，$R_1$ 为诱导 $\Pi^0_3$-完全集合族的集合。

• 定理 3.18： $R_0$ 和 $R_1$ 都是所有转移关系空间中的 Borel 子集。此外，$R_0$ 是 稠密（comeagre/residual） 的，这意味着“大多数”转移关系（在 Baire 范畴意义下）诱导一个拓扑结构简单的可监测集合族（$\Sigma^0_2$）。

3. 非第二可数情况
论文表明，对第二可数空间的限制是至关重要的。

• 示例： 作者构造了一个可数的、非第二可数的空间（基于带有顶元素 $\infty$ 的有限序列的 Scott 拓扑）。
• 结果： 对于该空间，可监测集合族 $M(X)$ 是 $\Pi^1_1$-完全的（完全解析集/complete coanalytic）。这与第二可数情况相比，在复杂度上有了显著的跃升，表明在缺乏第二可数性的情况下，判定可监测性的问题可以像判定树的良基性（well-foundedness）一样困难。

意义
本文提供了一个统一的、与语法无关的框架来理解可监测性。通过将问题映射到描述集合论，它确立了：

1. 在标准设置（包括许多运行时验证模型）的第二可数空间中，判定可监测性的复杂度被限制在 Borel 层级内，具体在 $\Pi^0_3$ 级别。
2. 存在一个清晰的结构准则（与极小开集和不相交性相关），决定了特定的系统模型是产生“简单”（$\Sigma^0_2$）还是“复杂”（$\Pi^0_3$-完全）的可监测性问题。
3. 第二可数性的假设是关键的；放宽这一限制允许出现任意高的复杂度（高达 $\Pi^1_1$-完全），这突显了拓扑约束在运行时验证理论分析中的重要性。

这项工作并非提出了新的监视器合成算法，而是划定了不同拓扑模型下可监测性判定问题的理论极限和结构属性。