## What's decidable about linear loops?

*Toghrul Karimov*, *Engel Lefaucheux*, *Joël
Ouaknine*, *David Purser*, *Anton Varonka*,
*Markus A. Whiteland*, and *James Worrell*
We consider the MSO model-checking problem for simple linear loops, or
equivalently discrete-time linear dynamical systems, with
semialgebraic predicates (i.e., Boolean combinations of polynomial
inequalities on the variables). We place no restrictions on the number
of variables, or equivalently the ambient dimension. We establish
decidability of the model-checking problem provided that each
semialgebraic predicate *either* has intrinsic dimension at most 1, *or* is
contained within some three-dimensional subspace. We also note that
lifting either of these restrictions and retaining decidability would
necessarily require major breakthroughs in number theory.

*Proceedings of POPL 22*, 2022. 25 pages.

PDF
© 2022 Toghrul Karimov, Engel Lefaucheux, Joël
Ouaknine, David Purser, Anton Varonka,
Markus A. Whiteland, and James Worrell.

Imprint / Data Protection