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

TL;DR

This paper proves that model checking linear dynamical systems against LTL specifications is decidable for systems of dimension three or less, advancing verification methods for such systems.

Contribution

It establishes the decidability of LTL model checking for discrete linear dynamical systems in dimensions up to three, a significant theoretical result.

Findings

Decidability proven for systems in dimension three or less.

Framework for verifying properties of linear dynamical systems.

Extension of model checking techniques to continuous state spaces.

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 $\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.