## Deciding ω-regular properties on linear recurrence sequences

*Shaull Almagor*, *Toghrul Karimov*, *Edon Kelmendi*,
*Joël
Ouaknine*, and *James Worrell*
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 a "-", 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ënov, 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.

*Proceedings of POPL 21*, 2021. 24 pages.

PDF
© 2021 Shaull Almagor, Toghrul Karimov, Edon Kelmendi,
Joël Ouaknine, and James Worrell.

Imprint / Data Protection