Boundedness Games

(an invitation to)


Nathanaël Fijalkow



Cassting, Eindhoven, 2 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.

The Mostowski index problem



Mostowski index problem: given a property over graphs, what is the minimal alternation of a modal $\mu$-calculus formula denoting it?

Spuriousness problem: given $\mu X \phi(X)$, is the $\mu$ operator spurrious, ie can it be captured by a finite unfolding of the formula?

Translation to automata over infinite trees

Just hook in a counter to get the following:

Proposition: For every $\mu X \phi(X)$, one can compute a cost automaton such that the $\mu$ operator is spurrious if, and only if, the cost automaton is bounded.

Be very smart, hook in several counters to get the following:

Theorem (Colcombet, Loeding 2008): For every modal $\mu$-calculus formula and level of the Mostowski hierarchy, one can compute a cost automaton such that the formula belongs to the level of the hierarchy, if and only if, the cost automaton is bounded.

Bottom line

To solve the Mostowski index problem and the spuriousness problem,
it suffices to solve the boundedness problem for cost automata over infinite trees



Corollary: the spuriousness problem is decidable.

The Mostowski index problem remains open!

Cost Monadic Second-Order Logic

A cost MSO formula has one special variable $N$. Syntactically, it is an MSO formula using the atomic formula $\text{Card}(X) \le N$ positively.

Cost MSO can be defined over (finite or infinite) words or trees.

Cost MSO problem: given a cost MSO formula $\phi$, $$\exists N \in \mathbb{N},\ \forall s,\ s,N \models \phi$$

B- and S-automata

To translate cost MSO into automata, define:
The crux is in proving that B- and S-automata are equivalent.

This has been proved for finite and infinite words, as well as for finite trees. Infinite trees still elude us!

Alternating automata

Idea: consider non-deterministic and alternating B- and S-automata.

To prove the equivalence between the four models, we extend the Muller-Schupp construction, which requires:
  • history-deterministic cost automata over infinite words,
  • finite-memory determinacy for boundedness games.

Bottom line

To solve cost MSO over infinite trees, it suffices to:



Cost MSO over infinite trees remains open!

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.

Example: $B(N) \cap \text{Buchi}(F)$

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

(Simplified) statement

There exists a trade-off function $\alpha : \mathbb{N} \to \mathbb{N}$ and a constant $m \in \mathbb{N}$ such that:
  for all games,
      if Eve has a strategy to ensure $B(N) \cap \text{Parity}$,
        then she has a strategy to ensure $B(\alpha(N)) \cap \text{Parity}$
        using $m$ memory states
Theorem (F., Horn, Kuperberg, Skrzypczak 2015): There is no trade-off in general!
Idea: play $K$ copies of the previous game with different timelines
Theorem (F., Horn, Kuperberg, Skrzypczak 2015): There exists a trade-off for games played over thin tree arenas