Games Programs Play: Analyzing Multiplayer Programs [Extended Version]

In particular, we show how weak-recurrence solvability can be lifted from finite-state programs to higher-order recursive programs. Our strategy reduces the search for a proof of a winning strategy to nontermination of higher-order programs for safety games, termination for liveness games, and an iterated combination of the two— along with winning preconditions—for weak recurrence games. We can thus leverage existing r