A discrete-time linear dynamical system (LDS) is given by an update matrix $M \in \mathbb{R}^{d\times d}$, and has the trajectories $\langle s, Ms, M^2s, \ldots \rangle$ for $s \in \mathbb{R}^d$. Reachability-type decision problems of linear dynamical systems, most notably the Skolem Problem, lie at the forefront of decidability: typically, sound and complete algorithms are known only in low dimensions, and these rely on sophisticated tools from number theory and Diophantine approximation. Recently, however, o-minimality has emerged as a counterpoint to these number-theoretic tools that allows us to decide certain modifications of the classical problems of LDS without any dimension restrictions. In this paper, we first introduce the Decomposition Method, a framework that captures all applications of o-minimality to decision problems of LDS that are currently known to us. We then use the Decomposition Method to show decidability of the Robust Safety Problem (restricted to bounded initial sets) in arbitrary dimension: given a matrix $M$, a bounded semialgebraic set $S$ of initial points, and a semialgebraic set $T$ of unsafe points, it is decidable whether there exists $\varepsilon > 0$ such that all orbits that begin in the $\varepsilon$-ball around $S$ avoid $T$.

翻译：离散时间线性动力系统由更新矩阵$M \in \mathbb{R}^{d\times d}$定义，其轨迹为$\langle s, Ms, M^2s, \ldots \rangle$（其中$s \in \mathbb{R}^{d}$）。线性动力系统的可达性判定问题（尤其是Skolem问题）处于可判定性研究的前沿：通常仅在低维情况下存在可靠且完备的算法，这些算法依赖于数论和丢番图逼近中的复杂工具。然而近年来，o-极小性作为这些数论工具的对立面出现，使得我们能够在无维度限制的情况下判定LDS经典问题的某些变体。本文首先提出分解方法——一个能涵盖目前已知所有o-极小性在LDS判定问题中应用的框架。随后运用该框架证明任意维度下鲁棒安全性问题（限于有界初始集）的可判定性：给定矩阵$M$、有界半代数初始点集$S$及半代数不安全点集$T$，可判定是否存在$\varepsilon > 0$使得所有始于$S$的$\varepsilon$邻域内的轨道均能避开$T$。