Skip to main content
main-content

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

04.04.2020 | Ausgabe 4/2021

Theory of Computing Systems 4/2021

First-Order Orbit Queries

Zeitschrift:
Theory of Computing Systems > Ausgabe 4/2021
Autoren:
Shaull Almagor, Joël Ouaknine, James Worrell
Wichtige Hinweise
This article belongs to the Topical Collection: Special Issue on Theoretical Aspects of Computer Science (2019)
Guest Editors: Rolf Niedermeier and Christophe Paul
Joël Ouaknine is supported by ERC grant AVS-ISS (648701) and by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science). James Worrell is supported by EPSRC Fellowship EP/N008197/1. Shaull Almagor has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skodowska-Curie grant agreement No 837327.

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

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.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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




Testen Sie jetzt 30 Tage kostenlos.

Literatur
Über diesen Artikel

Weitere Artikel der Ausgabe 4/2021

Theory of Computing Systems 4/2021 Zur Ausgabe

Premium Partner