Algebraic model checking for discrete linear dynamical systems
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, engineeri...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer Nature
2022
|
| _version_ | 1826310915619815424 |
|---|---|
| author | Luca, F Ouaknine, J Worrell, J |
| author_facet | Luca, F Ouaknine, J Worrell, J |
| author_sort | Luca, F |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T08:00:34Z |
| format | Conference item |
| id | oxford-uuid:7b4db5ba-777f-416b-a8fe-40324aec7788 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:00:34Z |
| publishDate | 2022 |
| publisher | Springer Nature |
| record_format | dspace |
| spelling | oxford-uuid:7b4db5ba-777f-416b-a8fe-40324aec77882023-09-27T12:02:45ZAlgebraic model checking for discrete linear dynamical systemsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:7b4db5ba-777f-416b-a8fe-40324aec7788EnglishSymplectic ElementsSpringer Nature2022Luca, FOuaknine, JWorrell, JModel 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. |
| spellingShingle | Luca, F Ouaknine, J Worrell, J Algebraic model checking for discrete linear dynamical systems |
| title | Algebraic model checking for discrete linear dynamical systems |
| title_full | Algebraic model checking for discrete linear dynamical systems |
| title_fullStr | Algebraic model checking for discrete linear dynamical systems |
| title_full_unstemmed | Algebraic model checking for discrete linear dynamical systems |
| title_short | Algebraic model checking for discrete linear dynamical systems |
| title_sort | algebraic model checking for discrete linear dynamical systems |
| work_keys_str_mv | AT lucaf algebraicmodelcheckingfordiscretelineardynamicalsystems AT ouakninej algebraicmodelcheckingfordiscretelineardynamicalsystems AT worrellj algebraicmodelcheckingfordiscretelineardynamicalsystems |