Orbit Problems are a class of fundamental reachability
questions that arise in the analysis of discrete-time linear dynamical
systems such as automata, Markov chains, recurrence sequences, and
linear while loops. Instances of the problem comprise a dimension
d ∈ N, a square matrix A ∈
Qdxd, and a query regarding the
behaviour of some sets under repeated applications of A. For
instance, in the Semialgebraic Orbit Problem, we are given
semialgebraic source and target sets S, T ∈
Rd, and the query is whether there exists
n ∈ N and x ∈ S such that
Anx ∈ T.
The main contribution of this paper is to introduce a unifying
formalism for a vast class of orbit problems, and show that this
formalism is decidable for dimension d ≤ 3. Intuitively, our
formalism allows one to reason about any first-order query whose
atomic propositions are membership queries of orbit elements in
semialgebraic sets. 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.
Theory of Computing Systems 65(4), 2020. 22 pages.
PDF
© 2020 Shaull Almagor, Joël
Ouaknine, and James Worrell.