Core Concepts
The language recognized by a probabilistic finite automaton is undecidable, even under various restrictions on the automaton's parameters.
Abstract
The paper presents two independent proofs that the Probabilistic Finite Automaton (PFA) Emptiness Problem is undecidable.
The first proof, due to Condon and Lipton, is based on the undecidability of the Halting Problem for 2-Counter Machines. It proceeds by constructing a PFA that can check the consistency of a 2-Counter Machine computation by running multiple "Equality Checker" sub-routines in parallel. The PFA accepts an input if it represents a valid accepting computation, and rejects otherwise, with a strong separation of probabilities.
The second proof, due to Nasu and Honda, uses a reduction from Post's Correspondence Problem (PCP). It constructs a PFA that can test the equality of two binary strings by exploiting a special multiplication property of the transition matrices. The PFA accepts an input if it represents a solution to the PCP, and rejects otherwise.
Both proofs are presented in a self-contained manner, with the Nasu-Honda-Claus proof taking only 3 pages. The paper also introduces several strengthened versions of the undecidability result, where the number of states, input symbols, or other parameters of the PFA are restricted.