What is known about the Value 1 Problem for Probabilistic Automata?

TL;DR

This paper reviews the value 1 problem for probabilistic automata, discussing various algorithms and establishing the Markov Monoid Algorithm as the most effective partial solution.

Contribution

It provides a comprehensive review of existing results and algorithms for the value 1 problem, clarifying their relationships and highlighting the Markov Monoid Algorithm's significance.

Findings

Markov Monoid Algorithm is the most correct known partial solution.

Several algorithms have been proposed and related.

The value 1 problem remains undecidable in general.

Abstract

The value 1 problem is a decision problem for probabilistic automata over finite words: are there words accepted by the automaton with arbitrarily high probability? Although undecidable, this problem attracted a lot of attention over the last few years. The aim of this paper is to review and relate the results pertaining to the value 1 problem. In particular, several algorithms have been proposed to partially solve this problem. We show the relations between them, leading to the following conclusion: the Markov Monoid Algorithm is the most correct algorithm known to (partially) solve the value 1 problem.