Reachability in Dynamical Systems with Rounding

TL;DR

This paper studies the reachability problem in linear dynamical systems with fixed digital precision, showing PSPACE-completeness in general and decidability for certain classes of rounding functions.

Contribution

It introduces a formal model for rounded linear systems and establishes complexity and decidability results for reachability problems within this framework.

Findings

Deciding reachability is PSPACE-complete for hyperbolic systems.

Reachability is decidable for several natural rounding functions.

The results extend understanding of digital-precision effects in dynamical systems.

Abstract

We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix $M \in \mathbb{Q}^{d \times d}$, an initial vector $x\in\mathbb{Q}^{d}$, a granularity $g\in \mathbb{Q}_+$ and a rounding operation $[\cdot]$ projecting a vector of $\mathbb{Q}^{d}$ onto another vector whose every entry is a multiple of $g$, we are interested in the behaviour of the orbit $\mathcal{O}={<}[x], [M[x]],[M[M[x]]],\dots{>}$, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability---whether a given target $y \in\mathbb{Q}^{d}$ belongs to $\mathcal{O}$---is PSPACE-complete for hyperbolic systems (when no eigenvalue of $M$ has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.