I couldn't decide!


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


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 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 \}$ $$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:
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$ word read "" counter value = 0 (max = 0) counter value = 0 (max = 0) counter value = 0 (max = 0) word read "a" counter value = 0 (max = 0) counter value = 1 (max = 1) counter value = 1 (max = 1) word read "aa" counter value = 0 (max = 0) counter value = 2 (max = 2) counter value = 2 (max = 2) word read "aaa" counter value = 0 (max = 0) counter value = 3 (max = 3) counter value = 0 (max = 2) word read "aaab" counter value = 0 (max = 0) counter value = 3 (max = 3) counter value = 0 (max = 2) word read "aaaba" counter value = 1 (max = 1) counter value = 3 (max = 3) counter value = 1 (max = 2) word read "aaabaa" counter value = 2 (max = 2) counter value = 3 (max = 3) counter value = 1 (max = 2) word read "aaabaab" counter value = 2 (max = 2) counter value = 3 (max = 3) counter value = 0 (max = 2)

Constructing history-deterministic automata

Idea (F., Colcombet 2016): composition of:

Bottom line

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

Cost Games