On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems

Abstract

Consider a discrete dynamical system given by a square matrix $M\in {\mathbb{Q}}^{d\times d}$ and a starting point $s\in {\mathbb{Q}}^d$. The orbit of such a system is the infinite trajectory $⟨s,Ms,M^{2}s,\dots ⟩$. Given a collection $T_1,T_2,\dots ,T_m\subseteq {\mathbb{R}}^d$ of semialgebraic sets, we can associate with each $T_i$ an atomic proposition $P_i$ which evaluates to true at time $n$ if, and only if, $M^{n}s\in T_i$. 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.

Long version of MFCS 2020 paper (19 pages)