main-content

## Weitere Artikel dieser Ausgabe durch Wischen aufrufen

04.04.2020 | Ausgabe 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.

### 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

Zur Ausgabe