Unforgettable Forgetful Determinacy

Publisher Website
Google Scholar
Abstract
This paper presents a relatively compact yet complete proof of the forgetful Determinacy Theorem (FDT) of Yuri Gurevich and Leo Harrington. The original motivation for this theorem was to provide a simpler proof of a powerful decidability result by Michael Rabin. Rabin's result and related techniques have found considerable application in computer science in dealing with the satisfiability problem for modal logics of programs. The FDT asserts the existence of a special kind of winning strategy in a particular class of infinite games. Although it first appeared as part of an alternative proof of Rabin's theorem, the FDT is a game-theoretic result that applies to more general situations than those in which it was originally used. Both the FDT and an earlier result by Richard Büchi and Lawrence Landweber address the issue of what kind of information is necessary to execute the winning strategy. Recently infinite games have been used to model non-terminating computations, and common methods of specification for such computations produce games to which the FDT applies. The original proof of the FDT was sketchy. Other proofs have been given, including one by Alexander and Vladimir Yakhnis that strengthened the result by providing more explicit strategies for the players. Nevertheless, there was still need for a more compact proof. To produce such a proof, we apply a modified version of the one by Yakhnis and Yakhnis to the slightly more general setting of graph-games. We use the notion of graph-games to emphasize the relationship between the FDT and the earlier result by Büchi and Landweber.

This publication has 0 references indexed in Scilit: