Consider a discrete dynamical system given by a square matrix M ∈ Qd×d and a starting point s ∈ Qd. The orbit of such a system is the infinite trajectory <s, Ms, M2s,...> . Given a collection T1, T2, ... , Tm ⊆ Rd of semialgebraic sets, we can associate with each Ti an atomic proposition Pi which evaluates to true at time n if, and only if, Mns ∈ Ti. This gives rise to the LTL Model-Checking Problem for discrete linear dynamical systems: given such a system (M, s) and an LTL formula over such atomic propositions, determine whether the orbit satisfies the formula. The main contribution of the present paper is to show that the LTL Model-Checking Problem for discrete linear dynamical systems is decidable in dimension 3 or less.
Proceedings of MFCS 20, LIPIcs 170, 2020. 18 pages.
© 2020 Toghrul Karimov, Joël Ouaknine, and James Worrell.