Reachability in dynamical systems with rounding

We consider reachability in dynamical systems with discrete linear updates, but with fixed decimal precision, i.e., such that values of the system are rounded at each step. Given a matrix M ∈ Q^d×d, an initial vector x ∈ Q^d, a granularity g ∈ Q₊ and a rounding operation [-] projecting a vector of Q^d onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit O = <[x], [M[x]], [M[M[x]]], ... >, 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 ∈ Q^d belongs to 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.

Proceedings of FSTTCS 20, LIPIcs 182, 2020. 25 pages.

PDF © 2020 Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland.