What's Decidable about Linear Loops?
summary
The paper proves decidability of MSO model checking for discrete-time linear dynamical systems with semialgebraic predicates provided every predicate is either intrinsic dimension ≤1 or contained in some linear dimension ≤3 subspace, with no bound on the number of variables. The method reduces trajectories of rational (or algebraic) matrices to symbolic words by a circle-rotation encoding and shows those words are effectively almost periodic. Removing the restrictions collapses to Skolem‑hard reachability.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:50MODEL CHECKING FOR LINEAR LOOPS
- 1:36LINEAR LOOPS IN PL RESEARCH
- 2:46STEP I PREDICATES
- 3:43EVOLUTION OVER TIME
- 4:22STEP II FORMULAS
- 5:23THE PROBLEM
- 6:39LINEAR DYNAMICAL SYSTEMS
- 8:26INSIDER: WHAT ARE PREDICATES?
- 10:18INTRINSIC AND LINEAR DIMENSION
- 13:05PROPERTIES OF THE WORD
- 14:28MAIN RESULT
- 17:59ALMOST PERIODIC WORDS