Linear Recurrence Sequences

Computing the Density of the Positivity Set for Linear Recurrence Sequences

The set of indices that correspond to the positive entries of a sequence of numbers is called its positivity set. In this paper, we study how dense is the positivity set of a given linear recurrence sequence. We show that one can compute this density …

Deciding ω-Regular Properties on Linear Recurrence Sequences

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. …