Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers

Abstract

A discrete-time linear dynamical system (LDS) is given by an update matrix M ∈ ℝ^{d× d}, and has the trajectories ⟨s, Ms, M²s, …⟩ for s ∈ ℝ^d. Reachability-type decision problems of linear dynamical systems, most notably the Skolem Problem, lie at the forefront of decidability: typically, sound and complete algorithms are known only in low dimensions, and these rely on sophisticated tools from number theory and Diophantine approximation. Recently, however, o-minimality has emerged as a counterpoint to these number-theoretic tools that allows us to decide certain modifications of the classical problems of LDS without any dimension restrictions. In this paper, we first introduce the Decomposition Method, a framework that captures all applications of o-minimality to decision problems of LDS that are currently known to us. We then use the Decomposition Method to show decidability of the Robust Safety Problem (restricted to bounded initial sets) in arbitrary dimension: given a matrix M, a bounded semialgebraic set S of initial points, and a semialgebraic set T of unsafe points, it is decidable whether there exists ε > 0 such that all orbits that begin in the ε-ball around S avoid T.