技术摘要：实线性循环的终止性

问题陈述

本文解决了实数域上离散时间线性及仿射动力系统的通用逃逸问题。具体而言，给定矩阵 $A \in \mathbb{R}^{n \times n}$ 和多面体 $P$（由矩阵 $B$ 及可能存在的向量 $\eta$ 定义），该问题询问：在映射 $x \mapsto Ax$（线性情形）或 $x \mapsto Ax + b$（仿射情形）的迭代下，是否 $P$ 中的每一点 $x$ 最终都会逃逸出 $P$。

作者在实计算的位模型（可计算分析）框架下开展工作。在此模型中，输入是以近似形式表示的实数。该设定下的一个根本限制是：由于连续性的要求，欧几里得空间的任何非平凡子集都不具有可计算的特征函数。因此，对于任意实数输入，该问题在经典意义上是不可判定的。本文旨在确定该问题在多大程度上是可判定的，重点关注鲁棒实例——即那些在输入数据发生充分微小扰动时，其答案（逃逸或被困）保持不变的实例。

方法论

作者采用了一个结合可计算分析与线性动力系统理论的框架。

1. 最大部分可判定性：作者并非寻求一个总体的判定过程，而是追求最大部分可判定性。如果一个算法对所有鲁棒实例（解集的内点）都能停机并报告正确答案，而对边界实例要么停机要么无限运行，则该算法是最大部分可判定的。
2. 通过一阶公式的特征刻画：核心方法论贡献在于推导出了刻画鲁棒逃逸和鲁棒被困实例的一阶逻辑公式。这些公式涉及对以下集合的量化：
   • 紧集：具体为单位球面 $S^{n-1}$ 和谱 $\sigma(A)$ 的子集。
   • 显集（Overt sets）：即其开集成员资格可半判定的集合。
   • 作者利用了在可计算分析中，对紧集和显集的量化是半可判定的这一事实。
3. 扰动分析：为了证明所推导的公式能正确刻画解集的内部（即鲁棒实例），本文利用了几项关于矩阵扰动的技术引理。这些引理表明，对于任何非鲁棒实例，都存在任意微小的扰动，能够改变谱性质（例如分裂特征值、改变重数）或特征向量与多面体边界之间的几何关系，从而将该实例移入鲁棒区域。
4. 齐次化与归约：针对仿射情形，作者通过齐次化研究了其与线性情形的关系。他们证明，虽然仿射问题在经典意义上可归约为线性问题，但这种归约并不保持鲁棒性（即无法将鲁棒的仿射实例映射为鲁棒的线性实例）。因此，仿射情形需要独立的特征刻画。

主要贡献与结果

1. 鲁棒线性实例的特征刻画

本文确立了实例 $(A, B)$ 为鲁棒逃逸或鲁棒被困的必要充分条件。

• 鲁棒逃逸：实例是鲁棒逃逸的，当且仅当：
  $$\forall \lambda \in \sigma_{\ge 0}(A). \forall v \in S^{n-1}. \left( Av = \lambda v \implies \exists j \in \{1, \dots, m\}. B_j v < 0 \right)$$
  该公式断言：对于每一个非负特征值，其对应的特征向量必须相对于定义多面体的至少一个半空间指向“外部”。

• 鲁棒被困：实例是鲁棒被困的，当且仅当：
  $$\exists \lambda \in \sigma^{odd}_{>0}(A). \forall v \in S^{n-1}. \left( Av = \lambda v \implies (Bv \rhd 0 \lor Bv \lhd 0) \right)$$
  该公式断言：存在一个具有奇数代数重数的正实特征值，使得其特征向量严格包含在多面体内部（即相对于所有约束严格为正或严格为负）。

2. 鲁棒仿射实例的特征刻画

对于仿射问题 $(A, B, b, \eta)$，作者提供了涉及齐次化矩阵 $\hat{A}$ 和向量 $\hat{B}$ 的类似特征刻画。

• 鲁棒逃逸：由限制在特征值 $\ge 1$ 上的 $\hat{A}$ 谱的条件来刻画。
• 鲁棒被困：由两个条件的析取来刻画：
  1. 系统具有一个位于多面体之外的唯一不动点（具体而言，$1 \notin \sigma(A)$ 且该不动点满足逃逸条件）。
  2. 存在一个具有奇数重数的特征值 $\lambda > 1$，使得其特征向量被严格困住。

3. 算法结果

• 定理 1 与 3：线性与仿射通用逃逸问题均是最大部分可判定的。作者构建了可靠的偏算法，这些算法在所有鲁棒实例上均能停机。
• 半可判定性：刻画鲁棒实例的公式被证明是可半判定的，这利用了可计算分析中的标准结果（例如多项式根的可计算性、球面的紧性以及显集的性质）。

4. 测度论结果

• 定理 5：线性和仿射问题的边界实例（非鲁棒实例）集合的勒贝格测度为零。
  • 这意味着所提出的算法在“几乎所有”输入上都会停机。
  • 该证明依赖于表明边界实例对应于余维数至少为 1 的实代数集的投影。

意义与主张

本文主张，在实计算的位模型框架内，实线性及仿射循环的通用逃逸问题“已接近人们所能期望的可判定极限”。

• 鲁棒性作为不可判定性的解决方案：作者认为，由于连续性的约束，针对实数数据的精确判定是不可能的，但最大部分可判定性提供了一种有意义且实用的替代方案。算法保证对所有不在决策边界“刀刃”上的输入终止。
• 效率与实用性：与针对有理数输入的先前方法（例如 Tiwari [Tiw04]）不同，后者依赖于若尔当标准形的计算（对于实矩阵而言，这是一项计算昂贵且往往不可计算的操作），本方法利用验证数值方法。通过一阶公式进行的特征刻画避免了符号化的若尔当分解，从而可能提供更高的效率。
• 与验证的联系：该工作与精确实计算和程序验证（例如针对实数据的霍逻辑框架）的最新发展相联系，为在参数仅近似已知或为实值的系统中验证活性属性提供了理论基础。
• 局限性：作者明确指出，从仿射系统到线性系统的归约无法保持鲁棒性，因此需要对仿射情形进行单独分析。他们并未声称解决所有输入的问题，而仅针对鲁棒子集，从测度论的角度看，这构成了几乎所有输入。

总之，本文通过从精确可判定性转向鲁棒部分可判定性，并提供构造性算法和测度论保证，为实线性系统的终止性判定提供了一个严谨的理论框架。