vix.ing · top · new · best · stats · spec

Register automata with linear arithmetic

2017/04/13 by Yu‐Fang Chen, Ondřej Lengál, Chen, Yu-Fang +5 · 2 citations
Computer Science · #F.1.1 #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1704.03972

openalex publication_date 2017/04/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

Related