Verification power of rational-valued automata with deterministic and affine states
Abstract
We investigate the verification power of rational-valued affine automata within Arthur--Merlin proof systems. For one-way verifiers, we give real-time protocols with perfect completeness and tunable bounded error for two benchmark nonregular languages, the balanced-middle language and the centered-palindrome language, illustrating a concrete advantage over probabilistic and quantum finite-state verifiers. For two-way verifiers, we first design a weak protocol that verifies every Turing-recognizable language by streaming and checking a configuration history. We then strengthen it with a probabilistic continuation check that bounds the prover's transcript length and ensures halting with high probability, yielding strong verification with expected running time proportional to the product of the simulated machine's space and time (up to input length and a factor polynomial in the inverse error parameter). Combining these constructions with standard alternation--space correspondences, we place alternating exponential time, equivalently deterministic exponential space, inside affine Arthur--Merlin with two-way affine automata. We also present a reduction-based route with perfect completeness via a Knapsack-game verifier, which, together with linear-space reductions, yields that the class PSPACE admits affine Arthur--Merlin verification by two-way affine automata. Two simple primitives drive our protocols: a probabilistic continuation check to control expected time and a restart-on-accept affine register that converts exact algebraic checks into eventually halting bounded-error procedures.