The power of Positivity

The Positivity Problem for linear recurrence sequences over a ring R of real algebraic numbers is to determine, given an LRS (u_n)_n∈N over R, whether u_n ≥ 0 for all n. It is known to be Turing-equivalent to the following reachability problem: given a linear dynamical system (M, s) ∈ R^d×d×R^d and a halfspace H ⊆ R^d, determine whether the orbit (Mⁿs)_n∈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 T₁,...,T_m ⊆ R^d, whether the orbit of (M, s) satisfies φ.

In this paper, we establish the following:

1) The Positivity Problem for LRS over real algebraic numbers reduces to the Positivity Problem for LRS over the integers; and
2) 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.

Proceedings of LICS 23, 2023. 11 pages.

PDF © 2023 IEEE.