Lower-bound for the decision of guidability

Guidable automata are a subclass of parity tree automata introduced by Colcombet and Löding [ICALP08], with a universal simulation property : An automaton $A$ is guidable if, for all automata $B$ recognizing a sublanguage of $L(A)$, there exists a finite "guiding function" for $B$ that converts an accepting run of $B$ over a tree $t$ in an accepting run of $A$ over $t$. More precisely, let $A = (Q_A, \Sigma, q_0, \Delta_A, col_A : \Delta_A \to \mathbb{N})$ be a parity automaton recognizing a tree language $L$. It is said guidable if, for all parity automaton $B = (Q_B, \Sigma, q_{0,B}, \Delta_B, col_B : \Delta_B \to \mathbb{N})$ recognizing $L'$ a sublanguage of $L$, there exists a guiding function $g_B: Q_A \times \Delta_B \to \Delta_A$ with the following properties: $g_B(p, (q, a, q', q'' )) = (p, a, p', p'' )$ for some $p' , p'' \in Q_A$ For every accepting run $\rho$ of $B$ over a tree $t$, $g_B(\rho)$ is an accepting run of $A$ over $t$, where $g_B(\rho) = \rho'$ is the unique run such that $\rho'(\varepsilon) = q_0$ , and for all $u \in \{0,1\}^*$, $(\rho' (u), t(u), \rho' (u0), \rho'(u1)) = g_B(\rho' (u), (\rho(u), t(u), \rho(u0), \rho(u1)))$. In that case, we say that $B$ guides $A$.

$$$$

Guidable automate can be seen as some kind of extension of History Deterministic automata to tree languages. They also seem to have a strong link with the Mostowski index problem, that is, the minimal index required to recognize a tree language with a parity automaton. Colcombet and Löding established that for all $\omega$-regular tree language $L$ there effectively exists a guidable automaton recognizing $L$, that can be built in 2EXP time and space. Löding also exhibited [Habilitation thesis,09] an automaton that does require this 2EXP blowup in order to exhibit a guidable automaton for this language. Following from these results, Niwiński and Skrzypczak introduced [MFCS21] the guidability game, from which they deduce a decision procedure for guidability in 2EXP-time. The lower bound for this problem, however, remains open. We conjecture that it is at least in EXPTIME.