Conteurs et allée A hantée au riz des autos mates


Nathanaël Fijalkow

October 16th, 2015, Paris



PhD Defense


Counting and Randomising in Automata Theory


Nathanaël Fijalkow

October 16th, 2015, Paris



PhD Defense

Induces $L \subseteq A^*$

Automata with Counters


word read "" counter value = 0 word read "b" counter value = 0 word read "ba" counter value = 1 word read "baa" counter value = 2 word read "baaa" counter value = 3 word read "baaab" counter value = 3

Induces   $f : A^* \to \mathbb{N} \cup \{ \infty \}$

Probabilistic Automata


word read "" 1 0 word read "1" .5 .5 word read "11" .25 .75 word read "110" .625 .375 word read "1101" .3125 .6875

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

Contributions

Finite-memory Determinacy for Games with Counters The Value 1 Problem for Probabilistic Automata

Boundedness Questions


Given a function   $f : A^* \to \mathbb{N}$, is it bounded?


  • Success story: Hashiguchi (1990), Leung (1991), Simon (1994), Kirsten (2005)
    Reducing the star-height problem to boundedness of automata with counters
  • Extensions: Bojańczyk (2004), Colcombet (2008)
    MSO + U and cost MSO: logical formalisms to express boundedness questions

The LoCo Conjecture



Theorem [Colcombet and Loeding (2008)]

LoCo Conjecture

$\implies$ decidability of cost MSO over infinite trees

$\implies$ decidability of the Mostowski index

Parity Games


Eve Adam
Strategy in general form $\sigma : V^+ \rightarrow E$

Positional (memoryless) strategies $\sigma : V \rightarrow E$


Theorem In parity games, both players have memoryless winning strategies.

Boundedness Games


Winning condition: parity and all counters are bounded

Two Semantics


Eve wins means:

(à la cost-MSO)

(à la MSO + U)
$\exists \sigma$ (strategy for Eve),

   $\exists N \in \mathbb{N}$,

      $\forall \pi$ (paths),

 $\exists \sigma$ (strategy for Eve),

   $\forall \pi$ (paths),

      $\exists N \in \mathbb{N}$,
$\pi$ satisfies parity and B(N) (i.e. each counter is bounded by $N$)

Example


Eve wants to ensure:
  • The counter value is bounded by N,
  • and the state F is visited infinitely many times


Memory
Bound
$N+1$
$N$
$2$
$2N-1$
$1$
$\infty$

The LoCo Conjecture


Finite-memory strategies $$\left \{ \begin{array}{c} \sigma : V \times M \rightarrow E \\ \mu : M \times E \rightarrow M \end{array} \right.$$

(Simplified) statement

$\forall c$ (number of priorities), $\forall k$ (number of counters),

   $\exists \alpha : \mathbb{N} \to \mathbb{N}$ (trade-off function), $\exists m \in \mathbb{N}$,

      $\forall G$ (games), $\forall N \in \mathbb{N}$,

            ($\exists \sigma$ strategy for $B(N) \cap \mathrm{Parity}$

$\implies \exists \sigma$ strategy for $B(\alpha(N)) \cap \mathrm{Parity}$ with $m$ memory states)

Contributions

Finite-memory Determinacy for Games with Counters The Value 1 Problem for Probabilistic Automata
  • A counter-example to the LoCo conjecture (with Kuperberg, Horn & Skrzypczak)
  • The LoCo conjecture over thin trees (with Kuperberg, Horn & Skrzypczak)

Theorem

The LoCo conjecture does not hold

The constant is at least 3:

Idea: play $K$ copies of the previous game with different timelines

Theorem

The LoCo conjecture holds over thin tree graphs

Contributions

Finite-memory Determinacy for Games with Counters The Value 1 Problem for Probabilistic Automata
  • A positive instance: cost-parity games (with Zimmermann)
  • Collapse for pushdown graphs (with Chatterjee)
  • Memory characterisation for topologically closed conditions (with Colcombet & Horn)
  • Memoryless strategies for stochastic infinite games (with Pinchinat & Serre)
  • A counter-example to the LoCo conjecture (with Kuperberg, Horn & Skrzypczak)
  • The LoCo conjecture over thin trees (with Kuperberg, Horn & Skrzypczak)

Contributions

Finite-memory Determinacy for Games with Counters The Value 1 Problem for Probabilistic Automata

An Unboundednes Question


Given a probabilistic automaton, do there exist words accepted with probability arbitrarily close to $1$?


Sad story: Gimbert and Oualhadj (2010)
It is undecidable!

But to what extent?



  • 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!

Contributions

Finite-memory Determinacy for Games with Counters The Value 1 Problem for Probabilistic Automata
  • The Markov Monoid algorithm (with Gimbert & Oualhadj)

An example

Markov Monoid algorithm


The Markov Monoid is a stabilisation monoid:
  • binary composition
  • stabilisation, denoted $\sharp$ (intuition: $u^\sharp = \lim_n u^n$)
It satisfies some natural axioms: $$u \cdot (v \cdot u)^\sharp = (u \cdot v)^\sharp \cdot u$$
If there exists an element $M$ such that $$\forall t \in Q, M(s_0, t) = 1 \implies t \in F$$ then the Markov Monoid algorithm answers "$\mathcal{A}$ has value 1", otherwise "$\mathcal{A}$ does not have value 1".

Contributions

Finite-memory Determinacy for Games with Counters The Value 1 Problem for Probabilistic Automata
  • The Markov Monoid algorithm (with Gimbert & Oualhadj)
  • Leaktight automata: extending and unifying results (with Gimbert, Oualhadj & Kelmendi)

Leaktight automata


Theorem

The Markov Monoid algorithm is correct for leaktight automata

Contributions

Finite-memory Determinacy for Games with Counters The Value 1 Problem for Probabilistic Automata
  • The Markov Monoid algorithm (with Gimbert & Oualhadj)
  • Leaktight automata: extending and unifying results (with Gimbert, Oualhadj & Kelmendi)
  • A characterisation: convergence speeds
  • The prostochastic theory

Convergence speeds


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

Characterisation


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$

Optimality


Theorem

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

The Markov Monoid algorithm is in some sense optimal

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.

Free Prostochastic Monoid


Theorem

The free prostochastic monoid, denoted $\mathcal{PA}$, is the set of all prostochastic words. It forms a compact metric space, satisfying a universal property:
''Every morphism $\phi : A^* \to Stoch(\mathbb{R})$ extends uniquely to a continuous morphism $\widehat{\phi} : \mathcal{PA} \to Stoch(\mathbb{R})$.''

Reformulation


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