The limitedness is a question of boundedness: given a function from words to integers described by some suitable model of finite state machines (distance automata, B-automata, …), determine whether the function it computes is bounded. It happens that for distance automata [Hashiguchi81, Leung82, Simon84] and B-automata [Kirsten05, Bojańczyk&C.06, C.09], this problem turns out to be decidable. This deep result is used in many situations, and in particular for solving the famous star-height problem [Hashiguchi88, Kirsten05]. (This problems asks, given a regular language L and a non-negative integer k, whether it is possible to describe L by means of a regular expression with nesting of Kleene stars bounded by k).

In his recent LICS15 paper, Bojańczyk gave a much shorter and self-contained proof of the decidability of limitedness (and in fact also star-height). It relies on a reduction to finite games of infinite duration, and involves arguments of positionality of stragegies in quantitative games [C.&Löding08]. The topic of this talk is the presentation of this elegant proof.

The decidability of limitedness was already presented in the LAAG seminar (using the algebraic approach of stabilization monoids), but the proof here is entirely different.