Abstract

We extend Gurevich-Harrington's Restricted Memory Determinacy Theorem), which served in their paper as a tool to give their celebrated “short proof” of Robin's decision method for S2S. We generalize the determinacy problem by attaching to the game two opposing strategies called restraints, and by asking “which player has a strategy which is a refinement of the restraint for the player and such that it wins the game against the restraint of the opponent?” We give a solution for the Determinacy with Restraints Problem in the class of strategies with restricted memory for the GH games. The solution includes a criterion for the winning player and an explicit class of winning strategies. A determinacy result which includes similar information was first discovered by Büchi and Landweber and extended by Büchi . However, these pioneering works do not consider the determinacy with restraints. Also, the explicit presentation of winning strategies in these insightful papers does not emphasize their modular construction as do GH's and our proofs. In our view, this is a source of a difficulty in understanding these papers. Games with restraints and modular construction of winning strategies have applications to the semantics, development and verification of concurrent programs. A concurrent program can be viewed as a strategy in a certain game and a program specification can be regarded as a combination of a winning condition and restraints for the game , A. Yakhnis and V. Yakhnis ). The modularity of a winning strategyfor the game helps to generate a concurrent program from the strategy that satisfies the specification ). It turns out that such program specification requirements as mutual exclusion and an absence of a lockout or a deadlock are naturally represented as Büchi's or Gurevich-Harrington's winning conditions. The present paper can be read independently of the paper by Gurevich and Harrington