Option 1: The Theory of Regular Cost Functions at No Extra Cost

Option 2: The Theory of Regular Cost Functions: No Pain, Full Gain

Nathanaël Fijalkow, GT-ALGA, Marseille, 11 April 2016

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:

Adam outputs letters,

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.

History-deterministic Automata

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.

Bottom line

To construct history-deterministic cost automata over finite words,
it suffices to prove positional determinacy for cost games.