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 ∈ Qd×d, an initial vector x ∈ Qd, a granularity g ∈ Q+ and a rounding operation [-] projecting a vector of Qd 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 ∈ Qd 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.
© 2020 Christel Baier, Florian Funke, Simon Jantsch,
Toghrul Karimov, Engel Lefaucheux,
Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland.