  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 $\omega$-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.
