×

First-order orbit queries. (English) Zbl 1518.37014

Summary: 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\in\mathbb{N}\), a square matrix \(A\in\mathbb{Q}^{d\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\subseteq\mathbb{R}^d\), and the query is whether there exists \(n\in\mathbb{N}\) and \(x\in S\) such that \(A^nx\in 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\leq 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 \(\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.

MSC:

37B10 Symbolic dynamics
03B25 Decidability of theories and sets of sentences
11J83 Metric theory
11J86 Linear forms in logarithms; Baker’s method
14P10 Semialgebraic sets and related spaces
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Almagor, S., Ouaknine, J., Worrell, J.: The polytope-collision problem. In: 44Th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, pp. 24:1-24:14. Warsaw (2017) · Zbl 1441.68083
[2] Almagor, S., Ouaknine, J., Worrell, J.: The semialgebraic orbit problem. In: 36Th International Symposium on Theoretical Aspects of Computer Science, STACS 2019, March 13-16, 2019, pp. 6:1-6:15. Berlin (2019) · Zbl 1518.37015
[3] Baker, A.; Wüstholz, G., Logarithmic forms and group varieties, J. Reine Angew. Math, 442, 19-62, 3 (1993) · Zbl 0788.11026
[4] Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry, vol. 20033, Springer (2005) · Zbl 1102.14041
[5] Chonev, V., Ouaknine, J., Worrell, J.: The polyhedron-hitting problem. In: Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 940-956. SIAM (2015) · Zbl 1372.68260
[6] Chonev, V.; Ouaknine, J.; Worrell, J., On the complexity of the orbit problem, J. ACM, 63, 3, 23:1-23:18 (2016) · Zbl 1426.68116 · doi:10.1145/2857050
[7] Cohen, H.: A course in computational algebraic number theory, vol. 138, Springer Science & Business Media (2013)
[8] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Automata Theory and Formal Languages 2Nd GI Conference Kaiserslautern, May 20-23, 1975, pp. 134-183. Springer (1975) · Zbl 0318.02051
[9] Gantmacher, F.R.: The Theory of Matrices. Number v. 2 in The Theory of Matrices Chelsea Publishing Company (1959) · Zbl 0085.01001
[10] Halava, V., Harju, T., Hirvensalo, M., Karhumäki, J.: Skolem’s problem – on the border between decidability and undecidability. Technical Report 683 Turku Centre for Computer Science (2005)
[11] Harrison, M.A.: Lectures on Linear Sequential Machines. Technical report, DTIC Document (1969) · Zbl 0212.34002
[12] Kannan, R., Lipton, R.J.: The orbit problem is decidable. In: Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing, pp. 252-261. ACM (1980)
[13] Kannan, R.; Lipton, RJ, Polynomial-time algorithm for the orbit problem, J. ACM (JACM), 33, 4, 808-821 (1986) · Zbl 1326.68162 · doi:10.1145/6490.6496
[14] Lafferriere, G.; Pappas, GJ; Yovine, S., Symbolic reachability computation for families of linear vector fields, J. Symb Comput., 32, 3, 231-253 (2001) · Zbl 0983.93004 · doi:10.1006/jsco.2001.0472
[15] Mignotte, M.: Some useful bounds. In: Computer Algebra, pp. 259-263. Springer (1983) · Zbl 0498.12019
[16] Mignotte, M., Shorey, T., Tijdeman, R.: The distance between terms of an algebraic recurrence sequence. J. für die reine und angewandte Math., 349 (1984) · Zbl 0521.10011
[17] Müller-Olm, M.; Seidl, H., Computing polynomial program invariants, Inf. Process. Lett., 91, 5, 233-244 (2004) · Zbl 1177.68048 · doi:10.1016/j.ipl.2004.05.004
[18] Ouaknine, J., Worrell, J.: Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences. In: International Colloquium on Automata, Languages, and Programming, pp. 330-341. Springer (2014) · Zbl 1410.11135
[19] Pan, VY, Optimal and nearly optimal algorithms for approximating polynomial zeros, Comput. Math. Appl., 31, 12, 97-138 (1996) · Zbl 0859.65045 · doi:10.1016/0898-1221(96)00080-6
[20] Renegar, J.: A faster PSPACE algorithm for deciding the existential theory of the reals. In: 29Th Annual Symposium on Foundations of Computer Science, pp 291-295. White Plains, New York (1988)
[21] Renegar, J., On the computational complexity and geometry of the first-order theory of the reals. part i: Introduction. preliminaries. the geometry of semi-algebraic sets. the decision problem for the existential theory of the reals, J. Symb. Comput., 13, 3, 255-299 (1992) · Zbl 0763.68042 · doi:10.1016/S0747-7171(10)80003-3
[22] Tao, T.: Structure and randomness: pages from year one of a mathematical blog. American Mathematical Soc. (2008) · Zbl 1245.00024
[23] Tarski, A.: A decision method for elementary algebra and geometry (1951) · Zbl 0044.25102
[24] Vereshchagin, NK, Occurrence of zero in a linear recursive sequence, Mathematical notes of the Academy of Sciences of the USSR, 38, 2, 609-615 (1985) · Zbl 0595.10007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.