First-order orbit queries

Journal article

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 𝑑∈ℕ, a square matrix 𝐴∈ℚ𝑑×𝑑, 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 𝑆,𝑇⊆ℝ𝑑, and the query is whether there exists 𝑛∈ℕ 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 a 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 ℝ𝑑 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.

Authors: Almagor, S; Ouaknine, J; Worrell, J

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer
• Journal: Theory of Computing Systems
• Volume: 65
• Issue: 4
• Pages: 638-661
• Publication date: 2020-04-04
• Acceptance date: 2020-02-24
• DOI: 10.1007/s00224-020-09976-7
• EISSN: 1433-0490
• ISSN: 1432-4350
• Language: English
• Keywords: orbit problem; first-order theory of the reals; linear dynamical systems; FFR