Extensions of the Church Synthesis Problem (a survey of results on Church's Problem)

Alex Rabinovich

Church's Problem (1963) asks for the construction of a procedure which, given a logical specification R on sequence pairs, realizes for any input sequence I an output sequence O such that (I,O) satisfies R.

McNaughton reduced Church's Problem to a problem about two-person omega-games.

The fundamental result due to Buchi and Landweber provides a solution for Monadic Second-Order Logic of Order specifications in terms of finite-state strategies.

We survey our recent results on three natural and orthogonal
generalizations of Church's problem.

1. The first considers strategies definable in logical formalisms.
2. The second considers parametrized version of the church problem.
3. The third deals with long games of any ordinal length.

Tuesday 9th February 2010, 14:00
Robert Recorde Room
Department of Computer Science