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
finite-state automata.
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.
PDF
© 2011 Mark Jenkins, Joël Ouaknine, Alexander Rabinovich,
and James Worrell.