-
Reachability in Injective Piecewise Affine Maps
Authors:
Faraz Ghahremani,
Edon Kelmendi,
Joël Ouaknine
Abstract:
One of the most basic, longstanding open problems in the theory of dynamical systems is whether reachability is decidable for one-dimensional piecewise affine maps with two intervals. In this paper we prove that for injective maps, it is decidable. We also study various related problems, in each case either establishing decidability, or showing that they are closely connected to Diophantine proper…
▽ More
One of the most basic, longstanding open problems in the theory of dynamical systems is whether reachability is decidable for one-dimensional piecewise affine maps with two intervals. In this paper we prove that for injective maps, it is decidable. We also study various related problems, in each case either establishing decidability, or showing that they are closely connected to Diophantine properties of certain transcendental numbers, analogous to the positivity problem for linear recurrence sequences. Lastly, we consider topological properties of orbits of one-dimensional piecewise affine maps, not necessarily with two intervals, and negatively answer a question of Bournez, Kurganskyy, and Potapov, about the set of orbits in expanding maps.
△ Less
Submitted 17 March, 2023; v1 submitted 23 January, 2023;
originally announced January 2023.
-
What's Decidable about Discrete Linear Dynamical Systems?
Authors:
Toghrul Karimov,
Edon Kelmendi,
Joël Ouaknine,
James Worrell
Abstract:
We survey the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability, model-checking, and invariant-generation questions, both unconditionally as well as relative to oracles for the Skolem Problem.
We survey the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability, model-checking, and invariant-generation questions, both unconditionally as well as relative to oracles for the Skolem Problem.
△ Less
Submitted 19 September, 2022; v1 submitted 22 June, 2022;
originally announced June 2022.
-
Computing the Density of the Positivity Set for Linear Recurrence Sequences
Authors:
Edon Kelmendi
Abstract:
The set of indices that correspond to the positive entries of a sequence of numbers is called its positivity set. In this paper, we study the density of the positivity set of a given linear recurrence sequence, that is the question of how much more frequent are the positive entries compared to the non-positive ones. We show that one can compute this density to arbitrary precision, as well as decid…
▽ More
The set of indices that correspond to the positive entries of a sequence of numbers is called its positivity set. In this paper, we study the density of the positivity set of a given linear recurrence sequence, that is the question of how much more frequent are the positive entries compared to the non-positive ones. We show that one can compute this density to arbitrary precision, as well as decide whether it is equal to zero (or one). If the sequence is diagonalisable, we prove that its positivity set is finite if and only if its density is zero. Further, arithmetic properties of densities are treated, in particular we prove that it is decidable whether the density is a rational number, given that the recurrence sequence has at most one pair of dominant complex roots. Finally, we generalise all these results to symbolic orbits of linear dynamical systems, thereby showing that one can decide various properties of such systems, up to a set of density zero.
△ Less
Submitted 27 November, 2023; v1 submitted 24 September, 2021;
originally announced September 2021.
-
Invariants for Continuous Linear Dynamical Systems
Authors:
Shaull Almagor,
Edon Kelmendi,
Joël Ouaknine,
James Worrell
Abstract:
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of…
▽ More
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of error states. In this paper we study the problem of synthesising inductive invariants that are definable in o-minimal expansions of the ordered field of real numbers. In particular, assuming Schanuel's conjecture in transcendental number theory, we establish effective synthesis of o-minimal invariants in the case of semi-algebraic error sets. Without using Schanuel's conjecture, we give a procedure for synthesizing o-minimal invariants that contain all but a bounded initial segment of the orbit and are disjoint from a given semi-algebraic error set. We further prove that effective synthesis of semi-algebraic invariants that contain the whole orbit, is at least as hard as a certain open problem in transcendental number theory.
△ Less
Submitted 28 April, 2020; v1 submitted 24 April, 2020;
originally announced April 2020.
