Model Checking Linear Dynamical Systems under Floating-point Rounding

TL;DR

This paper studies the behavior of linear dynamical systems with floating-point rounding, revealing decidability results for non-negative matrices and undecidability when negatives are involved, thus better modeling real-world computations.

Contribution

It introduces a novel analysis of floating-point rounded linear systems, showing decidability for non-negative matrices and undecidability with negatives, contrasting with unrounded system complexities.

Findings

Decidability of omega-regular model checking for non-negative matrices.

Periodic mantissas and linearly growing exponents in non-negative systems.

Undecidability of reachability when negative numbers are allowed.

Abstract

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.