Extensions of the Church synthesis Problem
Alex Rabinovich (Tel-Aviv University)
Abstract
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 Buhi 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 the Church problem.
The first considers strategies definable in logical formalisms.
The second considers parametrized version of the Church problem.
The third deals with long games of any ordinal length.