一句话：证明实代数数上线性递推序列的正性问题可归约到整数上，并给出可对角化线性动力系统半代数模型检测的相对可判定性。
本文研究实代数数上线性递推序列（LRS）的正性问题：判定序列是否所有项均非负。该问题与线性动力系统（LDS）的半空间可达性图灵等价；更一般的 LDS 模型检测需判定轨道是否满足由半代数谓词定义的 ω-正则性质。论文证明两项结果：一是实代数数上的 LRS 正性问题可归约到整数上的 LRS 正性问题；二是可对角化 LDS 的半代数模型检测在简单整数 LRS 正性 oracle 下可判定。因此，可对角化 LDS 的完整半代数模型检测不比简单整数 LRS 的正性问题更难，这与任意 LDS 及任意整数 LRS 的情形形成鲜明对比。
The Positivity Problem for linear recurrence sequences over a ring R of real algebraic numbers is to determine, given an LRS ${\left( {{u_n}} \right)_{n \in \mathbb{N}}}$ over R, whether un ≥ 0 for all n. It is known to be Turing-equivalent to the following reachability problem: given a linear dynamical system (M, s) Rd×d×Rd and a halfspace H ⊆ ℝd, determine whether the orbit ${\left( {{M^n}s} \right)_{n \in \mathbb{N}}}$ ever enters H. The more general model-checking problem for LDS is to determine, given (M, s) and an ω-regular property φ over semialgebraic predicates T1,…, Tℓ ⊆ ℝd, whether the orbit of (M, s) satisfies φ.In this paper, we establish the following1)The Positivity Problem for LRS over real algebraic numbers reduces to the Positivity Problem for LRS over the integers; and2)The model-checking problem for LDS with diagonalisable M is decidable subject to a Positivity oracle for simple LRS over the integers.In other words, the full semialgebraic model-checking problem for diagonalisable linear dynamical systems is no harder than the Positivity Problem for simple integer linear recurrence sequences. This is in sharp contrast with the situation for arbitrary (not necessarily diagonalisable) LDS and arbitrary (not necessarily simple) integer LRS, for which no such correspondence is expected to hold.