O-Minimal Invariants for Discrete-Time Dynamical Systems

Termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination relates to deep open problems in number theory, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this article, we introduce the class of o-minimal invariants , which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel’s conjecture is transcendental number theory.

Download Full-text

What’s decidable about linear loops?

Proceedings of the ACM on Programming Languages ◽

10.1145/3498727 ◽

2022 ◽

Vol 6 (POPL) ◽

pp. 1-25

Author(s):

Toghrul Karimov ◽

Engel Lefaucheux ◽

Joël Ouaknine ◽

David Purser ◽

Anton Varonka ◽

...

Keyword(s):

Number Theory ◽

Dynamical Systems ◽

Model Checking ◽

Discrete Time ◽

Three Dimensional ◽

Dimensional Subspace ◽

Intrinsic Dimension ◽

Linear Dynamical Systems ◽

Polynomial Inequalities ◽

Time Linear

We consider the MSO model-checking problem for simple linear loops, or equivalently discrete-time linear dynamical systems, with semialgebraic predicates (i.e., Boolean combinations of polynomial inequalities on the variables). We place no restrictions on the number of program variables, or equivalently the ambient dimension. We establish decidability of the model-checking problem provided that each semialgebraic predicate either has intrinsic dimension at most 1, or is contained within some three-dimensional subspace. We also note that lifting either of these restrictions and retaining decidability would necessarily require major breakthroughs in number theory.

Download Full-text

Positivity Problems for Low-Order Linear Recurrence Sequences

Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms ◽

10.1137/1.9781611973402.27 ◽

2013 ◽

Cited By ~ 14

Author(s):

Joël Ouaknine ◽

James Worrell

Keyword(s):

Linear Recurrence ◽

Order Linear ◽

Recurrence Sequences ◽

Positivity Problems ◽

Low Order

Download Full-text

Impulsive controllability of linear dynamical systems with applications to maneuvers of spacecraft

Mathematical Problems in Engineering ◽

10.1155/s1024123x9600035x ◽

1996 ◽

Vol 2 (4) ◽

pp. 277-299 ◽

Cited By ~ 98

Author(s):

Xinzhi Liu ◽

Allan R. Willms

Keyword(s):

Dynamical Systems ◽

Discrete Time ◽

Sufficient Conditions ◽

Necessary And Sufficient Conditions ◽

Linear Dynamical Systems ◽

Novel Approach ◽

Necessary And Sufficient

Necessary and sufficient conditions for impulsive controllability of linear dynamical systems are obtained, which provide a novel approach to problems that are basically defined by continuous dynamical systems, but on which only discrete-time actions are exercised. As an application, impulsive maneuvering of a spacecraft is discussed.

Download Full-text