Model checking infinite-state systems is one of the central challenges in automated verification. In this survey we focus on an important and fundamental subclass of infinite-state systems, namely discrete linear dynamical systems. While such systems are ubiquitous in mathematics, physics, engineering, etc., in the present context our motivation stems from their relevance to the formal analysis and verification of program loops, weighted automata, hybrid systems, and control systems, amongst many others. Our main object of study is the problem of model checking temporal properties on the infinite orbit of a linear dynamical system, and our principal contribution is to show that for a rich class of properties this problem can be reduced to certain classical decision problems on linear recurrence sequences, notably the Skolem Problem. This leads us to discuss recent advances on the latter and to highlight the prospects for further progress on charting the algorithmic landscape of linear recurrence sequences and linear dynamical systems.
Proceedings of FORMATS 22 (invited paper), LNCS 13465, 2022. 13 pages.
PDF
© 2022 Florian Luca, Joël Ouaknine, and James Worrell.