We consider linear dynamical systems under floating-point rounding. In
these systems, a matrix is repeatedly applied to a vector, but the
numbers are rounded into floating-point representation after each step
(i.e., stored as a fixed-precision mantissa and an exponent). The
approach more faithfully models realistic implementations of linear
loops, compared to the exact arbitrary-precision setting often
employed in the study of linear dynamical systems.
Our results are
twofold: We show that for non-negative matrices there is a special
structure to the sequence of vectors generated by the system: the
mantissas are periodic and the exponents grow linearly. We leverage
this to show decidability of ω-regular temporal model checking
against semialgebraic predicates. This contrasts with the unrounded
setting, where even the non-negative case encompasses the
long-standing open Skolem and Positivity problems.
On the other
hand, when negative numbers are allowed in the matrix, we show that
the reachability problem is undecidable by encoding a two-counter
machine. Again, this is in contrast with the unrounded setting where
point-to-point reachability is known to be decidable in polynomial
time.
Proceedings of TACAS 23, LNCS 13993, 2023. 26 pages.
PDF
© 2023
Springer-Verlag.