GUREVICH-HARRINGTON GAMES DEFINED BY FINITE AUTOMATA

We consider games over a finite alphabet with Gurevich-Harrington's wi nning conditions and restraints as in Yakhnis-Yakhnis (1990). The game tree, the Gurevich-Harrington's kernels of the winning condition and the restraints are defined by finite automata. We give an effective cr iterion 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 Buchi and L andweber (1969) (BL). The BL algorithm is an important tool for solvin g effectively presented games. The differences between the BL and our algorithms are as follows. Our algorithm is uniformly applicable to wi nning sets that correspond to boolean combinations of BL winning condi tions, while the BL algorithm requires a transformation of such boolea n combinations into a single BL condition. Our algorithm directly appl ies to a larger class of game trees for a given game alphabet than doe s the BL one. We describe Buchi-Landweber's class of winning condition s in a more transparent way by using finite automata and Gurevich-Harr ington's (1982) form of winning conditions. Our algorithms that determ ine 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 tabl e of the automaton representing the game. This automaton differs from the ones that represent BL winning conditions. Both algorithms need fu rther investigation. The algorithm determining the winner in the game, can be used as a verifier of concurrent programs. This is because pro grams can be viewed as strategies in Gurevich-Harrington's games and p rogram 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 (1990) 277-297.