Model Checking Linear Dynamical Systems under Floating-point Rounding
Résumé
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.
Domaines
Informatique [cs]
Origine : Fichiers produits par l'(les) auteur(s)
