Skip to main content

Extensions of the Church Synthesis Problem

Alex Rabinovich ( Tel Aviv University, Visiting Oxford )
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 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.

Share this: