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.

翻译：我们考虑浮点舍入下的线性动力系统。在这些系统中，矩阵反复应用于向量，但每一步后数字都会被舍入为浮点表示（即，存储为固定精度尾数和指数）。与线性动力系统研究中常采用的精确任意精度设置相比，该方法更忠实地模拟了线性循环的实际实现。我们的结果有两方面：首先，我们证明对于非负矩阵，系统生成的向量序列具有特殊结构：尾数呈周期性，指数呈线性增长。我们利用这一点证明了针对半代数谓词的$\omega$正则时序模型检测的可判定性。这与未舍入设置形成对比——即使在非负情况下，后者仍包含长期悬而未决的Skolem问题和Positivity问题。另一方面，当矩阵允许负数值时，我们通过编码双计数器机证明了可达性问题不可判定。这再次与未舍入设置形成对比——后者中点到点可达性已知可在多项式时间内判定。