The Semialgebraic Orbit Problem is a fundamental reachability question that arises in the
analysis of discrete-time linear dynamical systems such as automata, Markov chains, recurrence
sequences, and linear while loops. An instance of the problem comprises a dimension d ∈ N, a
square matrix A ∈ Qdxd, and
semialgebraic source and target sets S, T ∈ Rd. The question is
whether there exists x ∈ S and n ∈
N such that Anx
∈ T.
The main result of this paper is that the Semialgebraic Orbit Problem
is decidable for dimension
d ≤ 3. Our decision procedure relies on separation bounds for algebraic numbers as
well as a classical result of transcendental number theory -- Baker's theorem on linear forms in
logarithms of algebraic numbers. We moreover argue that our main result represents a natural
limit to what can be decided (with respect to reachability) about the orbit of a single matrix. On
the one hand, semialgebraic sets are arguably the largest general
class of subsets of Rd
for which
membership is decidable. On the other hand, previous work has shown that in dimension d = 4,
giving a decision procedure for the special case of the Orbit Problem with singleton source set S
and polytope target set T would entail major breakthroughs in Diophantine approximation.
Proceedings of STACS 19, LIPIcs 126, 2019. 20 pages.
PDF
© 2019 Shaull Almagor, Joël
Ouaknine, and James Worrell.