Profinite Techniques for Probabilistic Automata and the Markov Monoid Algorithm
Nathana\"el Fijalkow

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
