2025/09/09 by Zeyu Chen, Junde Wu, Chen, Zeyu +1
Computer Science · #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2509.07857
openalex publication_date 2025/09/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Affine automata provide a finite-state computational model that preserves the linear-algebraic structure of quantum computation while operating entirely over the reals. Recent work has shown that affine automata can far surpass classical probabilistic finite-state verifiers. However, prior constructions relied on arbitrary real-valued transition matrices, leaving open whether the observed power stems from the affine mechanism itself or from computational resources implicitly encoded in irrational or infinite-precision parameters. This paper studies one-way and two-way automata with deterministic and affine states as verifiers in Arthur--Merlin proof systems under the restriction that every affine transition matrix has rational entries, and shows that the resulting rational model still supports the main verification advantages of affine finite-state verification. At the one-way level, we verify benchmark nonregular languages that are provably hard or impossible for classical two-way probabilistic verifiers. At the two-way level, we achieve weak verification of every Turing-recognizable language, strong bounded-error verification for every language in ATIME(2O(n)), and perfect-completeness strong verification for every language in PSPACE. These results establish that the remarkable verification power of affine finite-state automata is structural.