基于实数 O-最小性的线性动力系统验证

离散时间线性动力系统（LDS）由矩阵 $M \in \mathbb{R}^{d\times d}$ 给出，其轨迹为 $\langle s, Ms, M^2s, \ldots \rangle$ 其中 $s \in \mathbb{R}^d$。到达类型决策问题（最著名的是 Skolem 问题）位于可判定性的最前沿：通常仅在低维度中已知完备且可靠的算法，这些算法依赖于数论和 Diophantine 逼近的高级工具。最近，然而，O-最小性已然出现作为这些数论工具的反面，允许我们在无需维度限制的情况下判定线性动力系统的某些修改后的经典问题。在本文中，我们首先引入分解方法（Decomposition Method），该方法概括了 O-最小性应用于 LDS 决策问题的所有已知应用。随后，我们使用分解方法显示，在任意维度中，鲁棒安全问题（限制于有界初始集合）是可判定的：给定矩阵 $M$，一个有界半代数集 $S$ 的初始点集合，以及一个不安全点集合 $T$，判定是否存在 $\varepsilon > 0$，使得所有开始于 $S$ 周围 $\varepsilon$ 球内的轨迹都避开 $T$。