一句话：论文刻画了带半代数谓词的简单线性循环在MSO模型检测下的可判定片段，并指出放宽条件需数论突破。
论文研究简单线性循环（等价于离散时间线性动力系统）的MSO模型检测问题，允许半代数谓词作为布尔组合的多项式不等式，且不限制程序变量个数或环境维数。作者证明：若每个半代数谓词的内蕴维数至多为一，或包含在某个三维子空间内，则模型检测问题是可判定的。该结果给出了一类无限状态线性循环的可判定边界；同时指出，若去掉任一限制仍保持可判定，将必然需要数论上的重大突破。
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 program 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.
@article{paperbot1574,
title = {What’s decidable about linear loops?},
author = {Toghrul Karimov and Engel Lefaucheux and Joël Ouaknine and David Purser and Anton Varonka and Markus A. Whiteland and James Worrell},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498727}
}