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. (shrink)

We consider games over a finite alphabet with Gurevich-Harrington's winning conditions and restraints as in Yakhnis-Yakhnis . The game tree, the Gurevich-Harrington's kernels of the winning condition and the restraints are defined by finite automata. We give an effective criterion to determine the winning player and an effective presentation of a class of finite automata defined winning strategies.Our approach yields an alternative solution to the games considered by Büchi and Landweber . The BL algorithm is an important tool for solving (...) effectively presented games. The differences between the BL and our algorithms are as follows. Our algorithm is uniformly applicable to winning sets that correspond to boolean combinations of BL winning conditions, while the BL algorithm requires a transformation of such boolean combinations into a single BL condition. Our algorithm directly applies to a larger class of game trees for a given game alphabet than does the BL one. We describe Büchi-Landweber's class of winning conditions in a more transparent way by using finite automata and Gurevich-Harrington's form of winning conditions. Our algorithms that determine the winner of the game and find a winning strategy, are based on a translation of the events in the game in terms of the transition table of the automaton representing the game. This automaton differs from the ones that represent BL winning conditions. Both algorithms need further investigation.The algorithm determining the winner in the game, can be used as a verifier of concurrent programs. This is because programs can be viewed as strategies in Gurevich-Harrington's games and program specifications could be regarded as winning conditions for such games. The algorithm which finds a winning strategy could be used as a basis for automated concurrent program design.The present paper is a sequel to Annals of Pure and Applied Logic 48 277–297. (shrink)