Deciding the value 1 problem for probabilistic leaktight automata

In this talk, I will present some recent work on the value 1 problem for probabilistic automata over finite words: given a probabilistic automaton, are there words accepted with probability arbitrarily close to 1?

This problem was proved undecidable recently. However, it shows some similarities with another problem, the boundedness problem for distance automata, which was shown decidable by Hashiguchi in 1982. Initially derived from a very long and complicated proof, this decidability result has been considerably simplified, the major steps being an algebraic algorithm proposed by Leung in 1991 and algebraic techniques developed by Simon in 1990 and 1994. The decidability result was later extended to nested desert distance automata and conceptually simplified by Kirsten in 2005.

We have transferred the underlying ideas to probabilistic automata. Our main contribution is to introduce a new class of probabilistic automata, called leaktight automata, for which the value 1 problem is shown decidable (and PSPACE-complete). We construct an algorithm based on the computation of a monoid abstracting the behaviors of the automaton, following Leung's algorithm. As in the case of distance automata, the correctness proof relies on the algebraic techniques developed by Simon, namely factorization and decomposition trees.