Reachability in Dynamical Systems with Rounding
| Autor: | Baier, Christel, Funke, Florian, Jantsch, Simon, Karimov, Toghrul, Lefaucheux, Engel, Ouaknine, Joël, Pouly, Amaury, Purser, David, Whiteland, Markus A. |
|---|---|
| Rok vydání: | 2020 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: To appear at FSTTCS'20 |
| Databáze: | arXiv |
| Externí odkaz: |
|