一句话：提出有理数上的寄存器自动机 RA_Q，支持线性算术，并证明其不变量问题可判定。
论文提出了一种新的有理数字母表上的自动机模型 RA_Q。该模型在传统无限字母表寄存器自动机的基础上，允许寄存器中数值之间的相等、序关系测试，并进一步支持某些变量间的线性算术。RA_Q 表达力较强，不仅推广了标准寄存器自动机，也概括了仿射程序和算术电路等模型。论文的核心贡献是证明了所谓 invariant problem（标准非空性问题的推广）在 RA_Q 上仍可判定。此外，作者还研究了交换性、等价性和可达性等自然判定问题，并表明对于确定性 RA_Q，交换性与等价性都可与 invariant problem 在多项式时间内相互归约。
We propose a novel automata model over the alphabet of rational numbers, which we call register automata over the rationals (RAℚ). It reads a sequence of rational numbers and outputs another rational number. RAℚ is an extension of the well-known register automata (RA) over infinite alphabets, which are finite automata equipped with a finite number of registers/variables for storing values. Like in the standard RA, the RAℚ model allows both equality and ordering tests between values. It, moreover, allows to perform linear arithmetic between certain variables. The model is quite expressive: in addition to the standard RA, it also generalizes other well-known models such as affine programs and arithmetic circuits. The main feature of RAℚ is that despite the use of linear arithmetic, the so-called invariant problem—a generalization of the standard non-emptiness problem—is decidable. We also investigate other natural decision problems, namely, commutativity, equivalence, and reachability. For deterministic RAℚ, commutativity and equivalence are polynomial-time inter-reducible with the invariant problem.