= Buchi game
{c}
{title2=$\text{visit }F\text{ infinitely often}$}
In a turn-based game on a set of positions, Player I wins if the play visits a specified set $F$ infinitely often. Such games are determined even on infinite arenas. With $\operatorname{Pre}(X)$ meaning positions where I can force the next position into $X$, the winning region is the greatest fixed point of $X\mapsto\mu Y((F\cap\operatorname{Pre}(X))\cup\operatorname{Pre}(Y))$. Inner ordinal ranks force the next visit; outer removal ranks give Player II only finitely many visits outside the winning region.
Back to article page
