Boundedness Games

Boundedness games are two player games played on graphs equipped with counters, where the winning condition for the first player is to ensure that the values of the counters remain bounded. They appeared in various contexts in the study of boundedness logics, in particular MSO + U by Bojanczyk and cost-MSO by Colcombet. Prominently, it was shown by Colcombet and Loeding that proving a finite-memory determinacy for boundedness games would imply the decidability of the Mostowski index problem for modal-mu calculus, a decades old open problem. The objective is this presentation is to report on the most recent results on boundedness games, and in particular on the decidability of a new special case of the Mostowski index problem.

Authors

• Nathanaël Fijalkow LaBRI, CNRS, France

Keywords

No keywords are indexed for this paper.