Verification power of rational-valued automata with deterministic and affine states
By: Zeyu Chen, Junde Wu
Potential Business Impact:
Helps computers prove hard math problems faster.
Previous research has shown that two-way automata with deterministic and affine states have strong verification capabilities, and that this power persists when all transition matrices are restricted to rational values. We investigate rational-valued affine automata as verifiers in Arthur--Merlin proof systems. For one-way verifiers, we give protocols with perfect completeness for two nonregular languages. For two-way verifiers, we first describe a weak protocol that verifies every Turing-recognizable language. We then strengthen this construction with a probabilistic continuation check to obtain strong verification with bounded error, establishing that every language decidable in deterministic exponential space is verifiable in Arthur--Merlin systems by rational-valued two-way affine automata. In a complementary, reduction-based route, we present a Knapsack-game verifier with perfect completeness, which implies that every language in PSPACE admits Arthur--Merlin verification by two-way affine automata with rational transitions. Taken together, these results illuminate the verification power of two-way affine automata while keeping arithmetic fully rational.
Similar Papers
Verification power of rational-valued automata with deterministic and affine states
Formal Languages and Automata Theory
Makes computers check math problems faster.
Polynomial Complementation of Nondeterministic 2-Way Finite Automata by 1-Limited Automata
Formal Languages and Automata Theory
Makes computers understand all languages perfectly.
ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
Logic in Computer Science
Checks computer systems for safety flaws faster.