Deciding $\omega$-Regular Properties on Linear Recurrence Sequences

TL;DR

This paper presents a method to decide whether infinite traces generated by simple linear recurrence sequences satisfy given omega-regular properties, leveraging the almost periodic nature of their sign descriptions.

Contribution

It introduces a procedure for verifying omega-regular properties on sequences from simple linear recurrences, utilizing the almost periodicity of their sign descriptions.

Findings

The sign description of simple linear recurrence sequences is almost periodic.

The procedure can determine property satisfaction for sequences with diagonalisable update matrices.

An example shows that not all linear recurrence sequences have almost periodic sign descriptions.

Abstract

We consider the problem of deciding $\omega$-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 $\omega$-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, \ie, 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.