Skip to main content
Erschienen in: Theory of Computing Systems 4/2021

04.04.2020

First-Order Orbit Queries

verfasst von: Shaull Almagor, Joël Ouaknine, James Worrell

Erschienen in: Theory of Computing Systems | Ausgabe 4/2021

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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\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 xS such that AnxT. 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 \(\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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
Note that this representation is not unique.
 
2
Technically, the indices should be I,JI, but we omit the dependency of J on I for simplicity.
 
3
Formally, only rational numbers should be allowed. However, the results of this section are meant to apply for a formula obtained by removing quantifiers in a general fooq. Thus, we must account for algebraic numbers as well.
 
4
By splitting modulo 2, we could actually improve the bound in the proposition from 4k to 2k, but this further complicates the proof.
 
5
We use x1,x2,x3 to represent constants or variables from x1,…,xm. For readability, we do not introduce double indices for these variables.
 
Literatur
1.
Zurück zum Zitat 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) 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)
2.
Zurück zum Zitat 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) 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)
3.
Zurück zum Zitat Baker, A., Wüstholz, G.: Logarithmic forms and group varieties. J. Reine Angew. Math 442(19-62), 3 (1993)MathSciNetMATH Baker, A., Wüstholz, G.: Logarithmic forms and group varieties. J. Reine Angew. Math 442(19-62), 3 (1993)MathSciNetMATH
4.
Zurück zum Zitat Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry, vol. 20033, Springer (2005) Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry, vol. 20033, Springer (2005)
5.
Zurück zum Zitat 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) 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)
6.
Zurück zum Zitat Chonev, V., Ouaknine, J., Worrell, J.: On the complexity of the orbit problem. J. ACM 63(3), 23:1–23:18 (2016)MathSciNetCrossRef Chonev, V., Ouaknine, J., Worrell, J.: On the complexity of the orbit problem. J. ACM 63(3), 23:1–23:18 (2016)MathSciNetCrossRef
7.
Zurück zum Zitat Cohen, H.: A course in computational algebraic number theory, vol. 138, Springer Science & Business Media (2013) Cohen, H.: A course in computational algebraic number theory, vol. 138, Springer Science & Business Media (2013)
8.
Zurück zum Zitat 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) 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)
9.
Zurück zum Zitat Gantmacher, F.R.: The Theory of Matrices. Number v. 2 in The Theory of Matrices Chelsea Publishing Company (1959) Gantmacher, F.R.: The Theory of Matrices. Number v. 2 in The Theory of Matrices Chelsea Publishing Company (1959)
10.
Zurück zum Zitat 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) 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.
Zurück zum Zitat Harrison, M.A.: Lectures on Linear Sequential Machines. Technical report, DTIC Document (1969) Harrison, M.A.: Lectures on Linear Sequential Machines. Technical report, DTIC Document (1969)
12.
Zurück zum Zitat 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) 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.
Zurück zum Zitat Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM (JACM) 33(4), 808–821 (1986)MathSciNetCrossRef Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM (JACM) 33(4), 808–821 (1986)MathSciNetCrossRef
14.
Zurück zum Zitat Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb Comput. 32(3), 231–253 (2001)MathSciNetCrossRef Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb Comput. 32(3), 231–253 (2001)MathSciNetCrossRef
15.
Zurück zum Zitat Mignotte, M.: Some useful bounds. In: Computer Algebra, pp. 259–263. Springer (1983) Mignotte, M.: Some useful bounds. In: Computer Algebra, pp. 259–263. Springer (1983)
16.
Zurück zum Zitat 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) 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)
17.
Zurück zum Zitat Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233–244 (2004)MathSciNetCrossRef Müller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233–244 (2004)MathSciNetCrossRef
18.
Zurück zum Zitat 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) 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)
19.
Zurück zum Zitat Pan, V.Y.: Optimal and nearly optimal algorithms for approximating polynomial zeros. Comput. Math. Appl. 31(12), 97–138 (1996)MathSciNetCrossRef Pan, V.Y.: Optimal and nearly optimal algorithms for approximating polynomial zeros. Comput. Math. Appl. 31(12), 97–138 (1996)MathSciNetCrossRef
20.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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)MathSciNetCrossRef 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)MathSciNetCrossRef
22.
Zurück zum Zitat Tao, T.: Structure and randomness: pages from year one of a mathematical blog. American Mathematical Soc. (2008) Tao, T.: Structure and randomness: pages from year one of a mathematical blog. American Mathematical Soc. (2008)
23.
Zurück zum Zitat Tarski, A.: A decision method for elementary algebra and geometry (1951) Tarski, A.: A decision method for elementary algebra and geometry (1951)
24.
Zurück zum Zitat Vereshchagin, N.K.: Occurrence of zero in a linear recursive sequence. Mathematical notes of the Academy of Sciences of the USSR 38(2), 609–615 (1985)MATH Vereshchagin, N.K.: Occurrence of zero in a linear recursive sequence. Mathematical notes of the Academy of Sciences of the USSR 38(2), 609–615 (1985)MATH
Metadaten
Titel
First-Order Orbit Queries
verfasst von
Shaull Almagor
Joël Ouaknine
James Worrell
Publikationsdatum
04.04.2020
Verlag
Springer US
Erschienen in
Theory of Computing Systems / Ausgabe 4/2021
Print ISSN: 1432-4350
Elektronische ISSN: 1433-0490
DOI
https://doi.org/10.1007/s00224-020-09976-7

Weitere Artikel der Ausgabe 4/2021

Theory of Computing Systems 4/2021 Zur Ausgabe