DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2011.307

The Church Synthesis Problem with Metric

Authors: Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, and James Worrell

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract

Church's Problem asks for the construction of a procedure which, given a logical specification S(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 S(I,F(I)) holds for all inputs I. Buechi 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.

Cite as

Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, and James Worrell. The Church Synthesis Problem with Metric. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 307-321, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{jenkins_et_al:LIPIcs.CSL.2011.307,
  author =	{Jenkins, Mark and Ouaknine, Jo\"{e}l and Rabinovich, Alexander and Worrell, James},
  title =	{{The Church Synthesis Problem with Metric}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{307--321},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.307},
  URN =		{urn:nbn:de:0030-drops-32390},
  doi =		{10.4230/LIPIcs.CSL.2011.307},
  annote =	{Keywords: Church's Problem, monadic logic, games, uniformization}
}

Search Results

Documents authored by Jenkins, Mark

The Church Synthesis Problem with Metric

Abstract

Cite as

Thanks for your feedback!

Could not send message