Document Open Access Logo

Reachability in Dynamical Systems with Rounding

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

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.36.pdf
  • Filesize: 1.6 MB
  • 17 pages

Document Identifiers

Author Details

Christel Baier
  • Technische Universität Dresden, Germany
Florian Funke
  • Technische Universität Dresden, Germany
Simon Jantsch
  • Technische Universität Dresden, Germany
Toghrul Karimov
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Engel Lefaucheux
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
  • Department of Computer Science, Oxford University, UK
Amaury Pouly
  • Université de Paris, CNRS, IRIF, F-75006, Paris, France
David Purser
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Markus A. Whiteland
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

Funding

This work was funded by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science), the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy), DFG-projects BA-1679/11-1 and BA-1679/12-1, and the Research Training Group QuantLA (GRK 1763).
  • Ouaknine, Joël: Supported by ERC grant AVS-ISS (648701).
  • Pouly, Amaury: Supported by CODYS project ANR-18-CE40-0007.

Cite AsGet BibTex

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

Abstract

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 ∈ ℚ^{d × d}, an initial vector x ∈ ℚ^{d}, a granularity g ∈ ℚ_+ and a rounding operation [⋅] projecting a vector of ℚ^{d} onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit 𝒪 = ⟨[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 ∈ ℚ^{d} belongs to 𝒪 - 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.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • dynamical systems
  • rounding
  • reachability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Shigeki Akiyama, Tibor Borbély, Horst Brunotte, Attila Pethő, and Jörg Thuswaldner. Generalized radix representations and dynamical systems. I. Acta Mathematica Hungarica, 108:207-238, August 2005. URL: https://doi.org/10.1007/s10474-005-0221-z.
  2. Shigeki Akiyama and Attila Pethő. Discretized rotation has infinitely many periodic orbits. Nonlinearity, 26(3):871-880, 2013. URL: https://doi.org/10.1088/0951-7715/26/3/871.
  3. S Akshay, Timos Antonopoulos, Joël Ouaknine, and James Worrell. Reachability problems for Markov chains. Information Processing Letters, 115(2):155-158, 2015. Google Scholar
  4. Shaull Almagor, Joël Ouaknine, and James Worrell. The semialgebraic orbit problem. In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science, STACS 2019, March 13-16, 2019, Berlin, Germany, volume 126 of LIPIcs, pages 6:1-6:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  5. C. Beck and G. Roepstorff. Effects of phase space discretization on the long-time behavior of dynamical systems. Physica D: Nonlinear Phenomena, 25(1):173-180, 1987. URL: https://doi.org/10.1016/0167-2789(87)90100-X.
  6. Michael Blank. Ergodic properties of discretizations of dynamic systems. Dokl. Akad. Nauk SSSR, 278(4):779-782, 1984. Google Scholar
  7. Michael Blank. Ergodic properties of a method of numerical simulation of chaotic dynamical systems. Mathematical Notes of the Academy of Sciences of the USSR, 45:267–273, 1989. URL: https://doi.org/10.1007/BF01158885.
  8. Michael Blank. Small perturbations of chaotic dynamical systems. Russian Mathematical Surveys, 44(6):1-33, December 1989. URL: https://doi.org/10.1070/rm1989v044n06abeh002302.
  9. Michael Blank. Pathologies generated by round-off in dynamical systems. Physica D: Nonlinear Phenomena, 78(1):93-114, 1994. URL: https://doi.org/10.1016/0167-2789(94)00103-0.
  10. Michael Blank. Discreteness and Continuity in Problems of Chaotic Dynamics. Translations of mathematical monographs. American Mathematical Society, 1997. Google Scholar
  11. D. Bosio and F. Vivaldi. Round-off errors and p-adic numbers. Nonlinearity, 13(1):309-322, 1999. URL: https://doi.org/10.1088/0951-7715/13/1/315.
  12. Jin-yi Cai. Computing Jordan normal forms exactly for commuting matrices in polynomial time. Int. J. Found. Comput. Sci., 5(3/4):293-302, 1994. URL: https://doi.org/10.1142/S0129054194000165.
  13. Rebekah Carter and Eva M. Navarro-López. Dynamically-driven timed automaton abstractions for proving liveness of continuous systems. In Marcin Jurdziński and Dejan Ničković, editors, Formal Modeling and Analysis of Timed Systems, pages 59-74, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-33365-1_6.
  14. Ventsislav Chonev, Joël Ouaknine, and James Worrell. The polyhedron-hitting problem. In Piotr Indyk, editor, Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2015, San Diego, CA, USA, January 4-6, 2015, pages 940-956. SIAM, 2015. Google Scholar
  15. Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, and Robert Bastian. Daisy - framework for analysis and optimization of numerical programs (tool paper). In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 270-287, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89960-2_15.
  16. Phil Diamond and Igor Vladimirov. Asymptotic independence and uniform distribution of quantization errors for spatially discretized dynamical systems. International Journal of Bifurcation and Chaos, 8:1479-1490, 1998. URL: https://doi.org/10.1142/S0218127498001133.
  17. Phil Diamond and Igor Vladimirov. Set-valued Markov chains and negative semitrajectories of discretized dynamical systems. Journal of Nonlinear Science, 12:113-141, 2002. URL: https://doi.org/10.1007/s00332-001-0450-4.
  18. S.P. Dias, L. Longa, and E. Curado. Influence of the finite precision on the simulations of discrete dynamical systems. Communications in Nonlinear Science and Numerical Simulation, 16(3):1574-1579, 2011. URL: https://doi.org/10.1016/j.cnsns.2010.07.003.
  19. Eric Goubault and Sylvie Putot. Static analysis of finite precision computations. In Ranjit Jhala and David Schmidt, editors, Verification, Model Checking, and Abstract Interpretation, pages 232-247, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-18275-4_17.
  20. Stephen Hammel, James Yorke, and Celso Grebogi. Numerical orbits of chaotic processes represent true orbits. Bull. Amer. Math. Soc., 19:465-, April 1988. URL: https://doi.org/10.1090/S0273-0979-1988-15701-1.
  21. Anastasiia Izycheva and Eva Darulova. On sound relative error bounds for floating-point arithmetic. In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD ’17, page 15–22, Austin, Texas, 2017. FMCAD Inc. URL: https://doi.org/10.23919/FMCAD.2017.8102236.
  22. Ravindran Kannan and Richard J. Lipton. Polynomial-time algorithm for the orbit problem. J. ACM, 33(4):808-821, 1986. URL: https://doi.org/10.1145/6490.6496.
  23. Anatole Katok and Boris Hasselblatt. Introduction to the Modern Theory of Dynamical Systems. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995. URL: https://doi.org/10.1017/CBO9780511809187.
  24. John Lowenstein, Spyros Hatjispyros, and Franco Vivaldi. Quasi-periodicity, global stability and scaling in a model of Hamiltonian round-off. Chaos: An Interdisciplinary Journal of Nonlinear Science, 7(1):49-66, 1997. URL: https://doi.org/10.1063/1.166240.
  25. Victor Magron, George Constantinides, and Alastair Donaldson. Certified roundoff error bounds using semidefinite programming. ACM Trans. Math. Softw., 43(4), 2017. URL: https://doi.org/10.1145/3015465.
  26. Oded Maler and Grégory Batt. Approximating continuous systems by timed automata. In Jasmin Fisher, editor, Formal Methods in Systems Biology, pages 77-89, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-68413-8_6.
  27. Mariano Moscato, Laura Titolo, Aaron Dutle, and César A. Muñoz. Automatic estimation of verified floating-point round-off errors via static analysis. In Stefano Tonetta, Erwin Schoitsch, and Friedemann Bitsch, editors, Computer Safety, Reliability, and Security, pages 213-229, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-66266-4_14.
  28. Ivan Niven. Irrational Numbers. Number 11 in The Carus Mathematical Monographs. The Mathematical Association of America, 1956. URL: https://doi.org/10.5948/9781614440116.
  29. Helena E. Nusse and James A. Yorke. Is every approximate trajectory of some process near an exact trajectory of a nearby process? Comm. Math. Phys., 114(3):363-379, 1988. URL: https://doi.org/10.1007/BF01242136.
  30. Joël Ouaknine and James Worrell. On linear recurrence sequences and loop termination. ACM SIGLOG News, 2(2):4-13, 2015. Google Scholar
  31. Attila Pethö, Jörg M. Thuswaldner, and Mario Weitzer. The finiteness property for shift radix systems with general parameters. Integers, 19:A50, 2019. URL: http://math.colgate.edu/%7Eintegers/t50/t50.Abstract.html.
  32. Stefano Schivo and Rom Langerak. Discretization of continuous dynamical systems using UPPAAL. In Joost-Pieter Katoen, Rom Langerak, and Arend Rensink, editors, ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, volume 10500 of Lecture Notes in Computer Science, pages 297-315. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-68270-9_15.
  33. Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamarić, and Ganesh Gopalakrishnan. Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. In Nikolaj Bjørner and Frank de Boer, editors, FM 2015: Formal Methods, pages 532-550, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-19249-9_33.
  34. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1-9. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
  35. Franco Vivaldi. The arithmetic of discretized rotations. AIP Conference Proceedings, 826, March 2006. URL: https://doi.org/10.1063/1.2193120.
  36. Franco Vivaldi and Igor Vladimirov. Pseudo-randomness of round-off errors in discretized linear maps on the plane. International Journal of Bifurcation and Chaos, 13(11):3373-3393, 2003. URL: https://doi.org/10.1142/S0218127403008557.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact