Solving sequential conditions by finite-state strategies
J. Richard Buchi, Lawrence H. Landweber · Transactions of the American Mathematical Society · 1969
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 [4] and contains, as a very special case, the answer to Case 4 left open in [6].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.