  It is undecidable whether the language recognized by a probabilistic finite
automaton is empty. Several other undecidability results, in particular
regarding problems about matrix products, are based on this important theorem.
We present three proofs of this theorem from the literature in a self-contained
way, and we derive some strengthenings. For example, we show that the problem
remains undecidable for a fixed probabilistic finite automaton with 11 states,
where only the starting distribution is given as input.
