What's Decidable about Discrete Linear Dynamical Systems?

TL;DR

This paper surveys the current state of research on the algorithmic analysis of discrete linear dynamical systems, focusing on reachability, model-checking, and invariant-generation, including the role of the Skolem Problem.

Contribution

It provides a comprehensive overview of decidability results and open problems in analyzing discrete linear dynamical systems, highlighting recent advances and challenges.

Findings

Summarizes key decidability results for reachability and model-checking.

Identifies open problems related to the Skolem Problem.

Highlights the role of oracles in the analysis of dynamical systems.

Abstract

We survey the state of the art on the algorithmic analysis of discrete linear dynamical systems, focussing in particular on reachability, model-checking, and invariant-generation questions, both unconditionally as well as relative to oracles for the Skolem Problem.