Profinite Techniques for Probabilistic Automata and the Markov Monoid Algorithm

TL;DR

This paper introduces a profinite topological framework called prostochastic theory to analyze the Markov Monoid algorithm for the undecidable value 1 problem in probabilistic automata, providing new insights and proofs.

Contribution

It characterizes the Markov Monoid algorithm and develops a novel prostochastic theory offering a topological perspective on the value 1 problem.

Findings

Prostochastic theory provides a topological reformulation of the value 1 problem.

The paper offers a simple, modular proof of the algorithm's properties.

Characterization of the Markov Monoid algorithm within the new framework.

Abstract

We consider the value 1 problem for probabilistic automata over finite words: it asks whether a given probabilistic automaton accepts words with probability arbitrarily close to 1. This problem is known to be undecidable. However, different algorithms have been proposed to partially solve it; it has been recently shown that the Markov Monoid algorithm, based on algebra, is the most correct algorithm so far. The first contribution of this paper is to give a characterisation of the Markov Monoid algorithm. The second contribution is to develop a profinite theory for probabilistic automata, called the prostochastic theory. This new framework gives a topological account of the value 1 problem, which in this context is cast as an emptiness problem. The above characterisation is reformulated using the prostochastic theory, allowing us to give a simple and modular proof.