## Reachability in dynamical systems with rounding

*Christel Baier*, *Florian Funke*,
*Simon Jantsch*, *Toghrul Karimov*,
*Engel Lefaucheux*,
*Joël
Ouaknine*, *Amaury Pouly*,
*David Purser*, and *Markus A. Whiteland*
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.

Imprint / Data Protection