Characterisation of an Algebraic Algorithm for Probabilistic Automata

Nathanaël Fijalkow

STACS, Orléans, February 18th

Probabilistic Automata	Profinite Techniques

Probabilistic Automata

Induces $f : A^* \to [0,1]$

Value $1$ Problem

INPUT: A probabilistic automaton

OUTPUT: Do there exist words accepted with probability arbitrarily close to $1$?

No sequence of actions ensure to reach home almost surely
For every $\varepsilon > 0$, there exists a sequence of actions ensuring to reach home with probability at least $1 - \varepsilon$
This is not true anymore if the probabilities change!

S01E01: Undecidability

Starring: Hugo Gimbert and Youssouf Oualhadj, 2010

Theorem: The value 1 problem is undecidable

S01E02: $\sharp$-acyclic automata

Starring: Hugo Gimbert and Youssouf Oualhadj, 2010

Theorem: The value 1 problem is decidable for $\sharp$-acyclic automata

S01E03: The plot thickens

Starring: Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan, Krishnendu Chatterjee and Mathieu Tracol, Nathanaël Fijalkow, Hugo Gimbert and Youssouf Oualhadj, 2011

Theorem: The value 1 problem is decidable for hierarchical automata, simple automata and leaktight automata

S01E04: Leaktight power

Starring: Nathanaël Fijalkow, Hugo Gimbert, Edon Kelmendi and Youssouf Oualhadj, 2015

Theorem: The class of leaktight automata contains all the others

What does the Markov Monoid Algorithm compute?

Markov Monoid Algorithm

S01E05: Finale

The sequence $((a^n b)^n)_{n \in \mathbb{N}}$ is polynomial, the sequence $((a^n b)^{2^n})_{n \in \mathbb{N}}$ is not.

Theorem:
The Markov Monoid algorithm answers YES
if, and only if,
there exists a polynomial sequence $(u_n)_{n \in \mathbb{N}}$ such that $\lim_n \mathbb{P}(u_n) = 1$

The sequence witnessing value 1 is $((\mathrm{drive}^n \cdot \mathrm{exit})^{2^n})_{n \in \mathbb{N}}$

Theorem:
Determining whether there exist two words $u,v$ such that $\lim_n \mathbb{P}((u^n v)^{2^n}) = 1$ is undecidable

What is the right language for...

Diplomacy: French!

Mathematics: Set theory? A blackboard? Homotopy type theory?

Automata and logics: Profinite theory

The value 1 problem: Prostochastic theory

Profinite	Prostochastic
A sequence converges if for every deterministic automaton, almost all words are accepted, or almost all words are rejected.	A sequence $(u_n)_{n \in \mathbb{N}}$ converges if for every probabilistic automaton, $\lim_n \mathbb{P}(u_n)$ exists.
Two sequences are equivalent if for every deterministic automaton, they agree on almost all words.	Two sequences $(u_n)_{n \in \mathbb{N}}$ and $(v_n)_{n \in \mathbb{N}}$ are equivalent if for every probabilistic automaton, $\lim_n \mathbb{P}(u_n) = \lim_n \mathbb{P}(v_n)$.
A profinite word is an equivalence class of converging sequences.	A prostochastic word is an equivalence class of converging sequences.

Characterisation of an Algebraic Algorithm for Probabilistic Automata

Nathanaël Fijalkow

STACS, Orléans, February 18th

Probabilistic Automata

Induces $f : A^* \to [0,1]$

Value $1$ Problem

S01E01: Undecidability

Theorem: The value 1 problem is undecidable

S01E02: $\sharp$-acyclic automata

Theorem: The value 1 problem is decidable for $\sharp$-acyclic automata

S01E03: The plot thickens

Theorem: The value 1 problem is decidable for hierarchical automata, simple automata and leaktight automata

S01E04: Leaktight power

Theorem: The class of leaktight automata contains all the others

What does the Markov Monoid Algorithm compute?

Markov Monoid Algorithm

S01E05: Finale

Theorem:
The Markov Monoid algorithm answers YES
if, and only if,
there exists a polynomial sequence $(u_n)_{n \in \mathbb{N}}$ such that $\lim_n \mathbb{P}(u_n) = 1$

Theorem:
Determining whether there exist two words $u,v$ such that $\lim_n \mathbb{P}((u^n v)^{2^n}) = 1$ is undecidable

What is the right language for...

Emptiness problem

Theorem: A probabilistic automaton has value 1
if, and only if,
it accepts a prostochastic word

Theorem: The Markov Monoid algorithm answers YES
if, and only if,
it accepts a polynomial prostochastic word

Characterisation of an Algebraic Algorithm for Probabilistic Automata

Nathanaël Fijalkow

STACS, Orléans, February 18th

Probabilistic Automata

Induces $f : A^* \to [0,1]$

Value $1$ Problem

S01E01: Undecidability

Theorem: The value 1 problem is undecidable

S01E02: $\sharp$-acyclic automata

Theorem: The value 1 problem is decidable for $\sharp$-acyclic automata

S01E03: The plot thickens

Theorem: The value 1 problem is decidable for hierarchical automata, simple automata and leaktight automata

S01E04: Leaktight power

Theorem: The class of leaktight automata contains all the others

What does the Markov Monoid Algorithm compute?

Markov Monoid Algorithm

S01E05: Finale

Theorem: The Markov Monoid algorithm answers YES if, and only if, there exists a polynomial sequence $(u_n)_{n \in \mathbb{N}}$ such that $\lim_n \mathbb{P}(u_n) = 1$

Theorem: Determining whether there exist two words $u,v$ such that $\lim_n \mathbb{P}((u^n v)^{2^n}) = 1$ is undecidable

What is the right language for...

Emptiness problem

Theorem: A probabilistic automaton has value 1 if, and only if, it accepts a prostochastic word

Theorem: The Markov Monoid algorithm answers YES if, and only if, it accepts a polynomial prostochastic word

Theorem:
The Markov Monoid algorithm answers YES
if, and only if,
there exists a polynomial sequence $(u_n)_{n \in \mathbb{N}}$ such that $\lim_n \mathbb{P}(u_n) = 1$

Theorem:
Determining whether there exist two words $u,v$ such that $\lim_n \mathbb{P}((u^n v)^{2^n}) = 1$ is undecidable

Theorem: A probabilistic automaton has value 1
if, and only if,
it accepts a prostochastic word

Theorem: The Markov Monoid algorithm answers YES
if, and only if,
it accepts a polynomial prostochastic word