Register automata with linear arithmetic

TL;DR

This paper introduces register automata over the rationals (RA-Q), a new model that extends traditional register automata with linear arithmetic, maintaining decidability of key problems despite increased expressiveness.

Contribution

It presents a novel automata model over rational numbers that incorporates linear arithmetic while preserving decidability of the invariant problem.

Findings

RA-Q generalizes affine programs and arithmetic circuits.

The invariant problem for RA-Q is decidable.

For deterministic RA-Q, commutativity and equivalence are polynomial-time inter-reducible with the invariant problem.

Abstract

We propose a novel automata model over the alphabet of rational numbers, which we call register automata over the rationals (RA-Q). It reads a sequence of rational numbers and outputs another rational number. RA-Q 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-Q 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-Q 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-Q, commutativity and equivalence are polynomial-time inter-reducible with the invariant problem.