## The power of Positivity

*Toghrul Karimov*, *Edon Kelmendi*, *Joris Nieuwveld*,
*Joël
Ouaknine*, and *James Worrell*
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*^{n}*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*_{1},...,*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.

Imprint / Data Protection