## First-order orbit queries

*Shaull Almagor*,
*Joël
Ouaknine*, and *James Worrell*
*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* ∈
**Q**^{dxd}, 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* ∈
**R**^{d}, and the query is whether there exists
*n* ∈ **N** and *x* ∈ *S* such that
*A*^{n}*x* ∈ *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
**R**^{d} 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*, 2020. 22 pages.

PDF
© 2020 Shaull Almagor, Joël
Ouaknine, and James Worrell.

Imprint / Data Protection