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

TL;DR

This paper introduces a new framework called the Decomposition Method that leverages o-minimality to decide certain reachability problems in linear dynamical systems across arbitrary dimensions, overcoming previous limitations.

Contribution

The paper presents the Decomposition Method, enabling the decidability of the Robust Safety Problem for LDS with bounded initial sets in any dimension using o-minimality.

Findings

Decidability of the Robust Safety Problem in arbitrary dimensions.

Introduction of the Decomposition Method framework.

Application of o-minimality to LDS decision problems.

Abstract

A discrete-time linear dynamical system (LDS) is given by an update matrix $M \in \mathbb{R}^{d\times d}$, and has the trajectories $\langle s, Ms, M^2s, \ldots \rangle$ for $s \in \mathbb{R}^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 $\varepsilon > 0$ such that all orbits that begin in the $\varepsilon$-ball around $S$ avoid $T$.