  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 $\langle s, Ms, M^2s,
\ldots\rangle$. Given a collection $T_1, T_2, \ldots, 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^ns
\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.
