A Robust Class of Linear Recurrence Sequences

线性递推序列自动机与抽象数制系统的加法

Linear Recurrence Sequence Automata and the Addition of Abstract Numeration Systems

引入序列自动机计算抽象数制系统中的$\mathbb{Z}$-有理非交换形式级数，利用Pisot条件下级数支持集的正则性，推导出计算Dumont-Thomas数制系统加法关系及数制转换的确定性有限自动机，并提供了Walnut实现。

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

为四阶线性递归序列的斯科姆问题补全画面

Completing the picture for the Skolem Problem on order-4 linear recurrence sequences

本文证明了对于阶数最多为4的代数线性递归序列，斯科姆问题的可判定性

Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences

We consider the decidability and complexity of the Ultimate Positivity Problem, which asks whether all but finitely many terms of a given rational linear recurrence sequence (LRS) are positive. Using lower bounds in Diophantine approximation concerning sums of S-units, we show that for simple LRS (those whose characteristic polynomial has no repeated roots) the Ultimate Positivity Problem is decidable in polynomial space. If we restrict to simple LRS of a fixed order then we obtain a polynomial-time decision procedure. As a complexity lower bound we show that Ultimate Positivity for simple LRS…