Reachability in Dynamical Systems with Rounding

Christel BaierChristel Baier, Florian FunkeFlorian Funke, Simon JantschSimon Jantsch, Toghrul KarimovToghrul Karimov, Engel LefaucheuxEngel Lefaucheux, Joël OuaknineJoël Ouaknine, Amaury PoulyAmaury Pouly, David PurserDavid Purser, Markus A. WhitelandMarkus A. Whiteland

DOI Link

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, Markus A. Whiteland
Reachability in Dynamical Systems with Rounding
In Nitin Saxena and Sunil Simon, eds., Proc. of 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020), volume 182 of Leibniz International Proceedings in Informatics (LIPIcs), 36:1--36:17, 2020. Schloss Dagstuhl--Leibniz-Zentrum für Informatik

Details
Bibtex

KurzfassungAbstract
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 ∈ 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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BFJKLOPPW2020,
  author    = {Christel Baier and Florian Funke and Simon Jantsch and Toghrul
               Karimov and Engel Lefaucheux and Jo{\"{e}}l Ouaknine and Amaury
               Pouly and David Purser and Markus A. Whiteland},
  title     = {Reachability in Dynamical Systems with Rounding},
  editor    = {Nitin Saxena and Sunil Simon},
  booktitle = {Proc. of 40th {IARCS} Annual Conference on Foundations of
               Software Technology and Theoretical Computer Science (FSTTCS
               2020)},
  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume    = {182},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2020},
  pages     = {36:1--36:17},
  doi       = {10.4230/LIPIcs.FSTTCS.2020.36}
}