Church's Problem asks for the construction of a procedure which, given
a logical specification φ(I,O) between input
strings I and output strings O, determines whether there
exists an operator F that implements the specification in the
sense that φ(I,F(I)) holds for all
inputs I. Büchi and Landweber gave a procedure to solve
Church's problem for MSO specifications and operators computable by
We consider extensions of Church's problem in two orthogonal directions: (i) we address the problem in a more general logical setting, where not only the specifications but also the solutions are presented in a logical system; (ii) we consider not only the canonical discrete time domain of the natural numbers, but also the continuous domain of reals.
We show that for every fixed bounded length interval of the reals, Church's problem is decidable when specifications and implementations are described in the monadic second-order logics over the reals with order and the +1 function.
Proceedings of CSL 11, LIPIcs 12, 2011. 15 pages.
© 2011 Mark Jenkins, Joël Ouaknine, Alexander Rabinovich,
and James Worrell.