@article{Almagor:2020aa,
    Abstract = {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∈ℕ{\$}d{$\backslash$}in {$\backslash$}mathbb {\{}N{\}}{\$}, a square matrix A∈ℚd×d{\$}A{$\backslash$}in {$\backslash$}mathbb {\{}Q{\}}\^{}{\{}d{$\backslash$}times d{\}}{\$}, 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⊆ℝd{\$}S,T{$\backslash$}subseteq {$\backslash$}mathbb {\{}R{\}}\^{}{\{}d{\}}{\$}, and the query is whether there exists n∈ℕ{\$}n{$\backslash$}in {\{}{$\backslash$}mathbb {\{}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 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 ℝd{\$}{$\backslash$}mathbb {\{}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.},
    Author = {Almagor, Shaull and Ouaknine, Jo{\"e}l and Worrell, James},
    File = {First-Order Orbit Queries - almagor2020 - a - j.pdf},
    ISBN = {1433-0490},
    Journal = {Theory of Computing Systems},
    Title = {First-Order Orbit Queries},
    URL = {https://doi.org/10.1007/s00224-020-09976-7},
    Year = {2020},
    bdsk-url-1 = {https://doi.org/10.1007/s00224-020-09976-7},
    da = {2020/04/04},
    date-added = {2020-04-25 11:48:10 +0200},
    date-modified = {2020-04-25 11:48:10 +0200},
    file-2 = {First-Order Orbit Queries - AOW20 - a - j.pdf},
    id = {Almagor2020},
    ty = {JOUR},
    doi = {10.1007/s00224-020-09976-7}
}

@article{Almagor:2020aa, Abstract = {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∈ℕ{\$}d{$\backslash$}in {$\backslash$}mathbb {{}N{}}{\$}, a square matrix A∈ℚd×d{\$}A{$\backslash$}in {$\backslash$}mathbb {{}Q{}}\^{}{{}d{$\backslash$}times d{}}{\$}, 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⊆ℝd{\$}S,T{$\backslash$}subseteq {$\backslash$}mathbb {{}R{}}\^{}{{}d{}}{\$}, and the query is whether there exists n∈ℕ{\$}n{$\backslash$}in {{}{$\backslash$}mathbb {{}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 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 ℝd{\$}{$\backslash$}mathbb {{}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.}, Author = {Almagor, Shaull and Ouaknine, Jo{\"e}l and Worrell, James}, File = {First-Order Orbit Queries - almagor2020 - a - j.pdf}, ISBN = {1433-0490}, Journal = {Theory of Computing Systems}, Title = {First-Order Orbit Queries}, URL = {https://doi.org/10.1007/s00224-020-09976-7}, Year = {2020}, bdsk-url-1 = {https://doi.org/10.1007/s00224-020-09976-7}, da = {2020/04/04}, date-added = {2020-04-25 11:48:10 +0200}, date-modified = {2020-04-25 11:48:10 +0200}, file-2 = {First-Order Orbit Queries - AOW20 - a - j.pdf}, id = {Almagor2020}, ty = {JOUR}, doi = {10.1007/s00224-020-09976-7} }