Model Checking Linear Dynamical Systems under Floating-point Rounding

Lefaucheux, Engel ORCID: 0000-0003-0875-300X, Ouaknine, Joël ORCID: 0000-0003-0031-9356, Purser, David ORCID: 0000-0003-0394-1634 and Sharifi, Mohammadamin ORCID: 0000-0002-1987-9487 (2023) Model Checking Linear Dynamical Systems under Floating-point Rounding. In: TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2023-4-24 - 2023-4-27, Paris, France.

Text submission.pdf - Author Accepted Manuscript Download (529kB) | Preview

Abstract

<jats:title>Abstract</jats:title><jats:p>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.</jats:p><jats:p>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 <jats:inline-formula><jats:alternatives><jats:tex-math>$$\omega $$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>ω</mml:mi> </mml:math></jats:alternatives></jats:inline-formula>-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.</jats:p><jats:p>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.</jats:p>

Item Type:	Conference or Workshop Item (Unspecified)
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	09 Feb 2023 11:34
Last Modified:	24 Jun 2023 16:16
DOI:	10.1007/978-3-031-30823-9_3
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3168311