The values of rational probabilistic finite automata are the left-c.e. reals

Which real numbers are values of probabilistic finite automata with rational transition probabilities and a rational initial distribution? We show that they are exactly the left-c.e. reals in [0,1], the limits of computable nondecreasing sequences of rational numbers. Here the value of an automaton is the supremum, over all finite input words, of the probability that the word is accepted. Every value is left-c.e. because the words can be enumerated; we prove that every left-c.e. real in [0,1] occurs, and that two input letters and one fixed number of states suffice for all of them.In particular a single automaton can have a noncomputable value. It was known that no algorithm computes, or even approximates, the value from the automaton; that concerns the map from automata to values, not single values. We give an automaton, specified explicitly relative to a fixed enumeration of Turing machines, whose value is 1/4 plus the sum of 4^-(n+2) over the programs n that halt on input n. The automaton checks claimed runs of a counter machine by a likelihood test in the manner of Condon and Lipton, and pays out a reward read from each run's output. The construction uses a rational interval around the target; from the target's approximations alone no algorithm can produce the automaton, since an automaton of value 0 can be recognized. The halting probability of every prefix-free machine, Chaitin's Ω among them, is the value of a probabilistic finite automaton with two input letters. With a construction of Elkouss and Pérez-García, every left-c.e. real in [0,1] is also the capacity of a finite-state channel with rational transition probabilities; in particular one such channel has a noncomputable capacity.