Our main purpose is to present an algorithm which decides whether or not a condition &(X, Y) stated in sequential calculus admits a finite automata solution, and produces one if it exists. This solves a problem stated in In an equally appealing form the result can be restated in the terminology of [7], [10], [15]: Every cu-game definable in sequential calculus is determined. Moreover the player who has a winning strategy, in fact, has a winning finite-state strategy, that is one which can effectively be played in a strong sense. The main proof, that of the central Theorem 1, will be presented at the end. We begin with a discussion of its consequences.
No takes yet. Share an insight, caveat, or question.
Büchi et al. (1969) studied this question.