## The star-height problem

• $(a + b^*)^* + a b^*$ has star-height $2$
• $a^* b^* + (ba)^*$ has star-height $1$

Star-height problem: given a regular language $L$, what is the minimal star-height of a regular expression denoting $L$?

## Cost automata

Theorem (Hashiguchi): the star-height problem can be reduced to the boundedness problem of cost automata
Induces   $f : A^* \to \mathbb{N} \cup \{ \infty \}$ $$f(w) = \text{min} \left\{ \text{max} \text{ counter value in } \rho \mid \rho \text{ accepting run} \right\}$$

## Reduction

A string expression of height $h$ and width $m$ is $$\bigcup w_1\ f_1^*\ w_2\ f_2^*\ \ldots\ w_i\ f_i^*$$ where:
• $i \le m$
• $|w_\ell| \le m$
• $f_\ell$ are string expressions of height $h-1$ and width $m$

Proposition (Kirsten 2005): For every regular language $L$ and $h \in \mathbb{N}$ one can compute a cost automaton such that for every $w \in A^*$, the following are equivalent:
• there is a string expression $e$ of height $h$ and width $m$ such that $w \in e \subseteq L$
• the automaton has a run on $w$ with value at most $m$

### Boundedness of cost automata

$$\exists N \in \mathbb{N},\ \forall w \in A^*,\ f(w) \le N$$ Remark: generalises universality

Proposition (Bojańczyk 2015): A cost automaton is bounded if, and only if, Eve wins the Gale-Stewart game where:
• Eve outputs sets of transitions.
Eve wins if there exists $N$ such that:
• at every point there exists an accepting run,
• in all runs the value of the counters are bounded by $N$.

## Bottom line

### To solve the star-height problem, it suffices to solve boundedness games

Corollary: the star-height problem is decidable.

## An example

$$f(a^{n_1} b a^{n_2} b \cdots a^{n_k} b) = \text{min}\ n_\ell$$ $n = 2$

### Constructing history-deterministic automata

Idea (F., Colcombet 2016): composition of:
• A history-deterministic automaton $\mathcal{B}$ that inputs letters and outputs a run tree. To prove that $\mathcal{B}$ is history-deterministic we need a positionality result for cost games.
• A deterministic B-automaton $\mathcal{C}$ that inputs a run tree and checks whether all paths have small values. To obtain a deterministic B-automaton $\mathcal{C}$ we rely on Safra's construction used as a black-box.