Solving sequential conditions by finite-state strategies

Abstract

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.