一句话：证明简单线性递推序列的符号描述几乎周期，并给出判定前缀无关 ω-正则性质的过程。
本文研究由线性循环产生的无限迹上的 ω-正则性质判定问题。给定循环产生的单条无限迹编码程序变量在各时刻的符号信息；形式上，输入一个前缀无关的 ω-正则性质以及满足线性递推的数列，判定其符号描述（正项记“+”、负项记“−”、零项记“0”）是否满足该性质。方法依赖于递推的“简单”性，即底层循环的更新矩阵可对角化。作者证明关键引理：简单线性递推序列的符号描述在 Muchnik、Semenov 和 Ushakov 意义下是几乎周期的；同时给出反例表明一般线性递推序列的符号描述未必几乎周期。最后，将结果从符号描述推广到涉及程序变量上半代数谓词的性质验证。
We consider the problem of deciding ω-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. Formally, our main result is a procedure that inputs a prefix-independent ω-regular property and a sequence of numbers satisfying a linear recurrence, and determines whether the sign description of the sequence (obtained by replacing each positive entry with “+”, each negative entry with “−”, and each zero entry with “0”) satisfies the given property. Our procedure requires that the recurrence be simple, i.e., that the update matrix of the underlying loop be diagonalisable. This assumption is instrumental in proving our key technical lemma: namely that the sign description of a simple linear recurrence sequence is almost periodic in the sense of Muchnik, Sem'enov, and Ushakov. To complement this lemma, we give an example of a linear recurrence sequence whose sign description fails to be almost periodic. Generalising from sign descriptions, we also consider the verification of properties involving semi-algebraic predicates on program variables.
@article{paperbot1154,
title = {Deciding ω-regular properties on linear recurrence sequences},
author = {Shaull Almagor and Toghrul Karimov and Edon Kelmendi and Joël Ouaknine and James Worrell},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434329}
}