Boundedness Pushdown Games

Krishnendu Chatterjee, Nathanaël Fijalkow

A reviewer:

''the subject of research sounds like a parody on esoteric models''

But the problem itself is a very nice riddle, (...) it’s nice to see technical acrobatics in action.

Pushdown Games

$\omega B$-regular Conditions

Typical examples:

$a^{n_1} b a^{n_2} b a^{n_3} b \cdots$ such that $\lim\inf n_i < \infty$
If infinitely many $a$ then $b$ blocks have bounded size, otherwise $c$ blocks have bounded size

A Boundedness Game

Non-determinism

$\omega$-regular conditions = non-deterministic parity automata

Theorem (Mc Naughton, Muller and Schupp): Determinisation of parity automata

To solve $\omega$-regular games: compose with deterministic automaton

$\omega B$-regular conditions = non-deterministic $\omega B$ automata

Theorem: $\omega B$ automata cannot be determinised (at all)!

Quantitative Determinacy

Either Eve can ensure some bound, or Adam can ensure that the counter is unbounded.

Results

Combining:

Quantitative determinacy for pushdown boundedness games
Two-way cost automata (CSL-LICS'2014)
History-determinacy cost automata (ICALP'2009)

We obtain:
Theorem: Solving pushdown games with $\omega B$-regular conditions is decidable.