Games are used to model many instances arising from interaction of more than one computational agent. In program synthesis, existence of strategy is the key in deciding the existence of a program with a given set of specifications.

In this talk, we will observe Martin's proof of the existence of strategy in a class of two-player infinite games with perfect information (namely Borel games). One instance of this result is that in the initial stage of a game of chess, at least one of the players has a strategy to prevent from losing.

Link of the paper: https://www.jstor.org/stable/pdf/1971035.pdf?refreqid=excelsior%3Aed93a8...