Rabinovich, Alexander - The Church Synthesis Problem with Parameters

lmcs:1233 - Logical Methods in Computer Science, November 14, 2007, Volume 3, Issue 4
The Church Synthesis Problem with Parameters

Authors: Rabinovich, Alexander

For a two-variable formula &psi;(X,Y) of Monadic Logic of Order (MLO) the Church Synthesis Problem concerns the existence and construction of an operator Y=F(X) such that &psi;(X,F(X)) is universally valid over Nat. Büchi and Landweber proved that the Church synthesis problem is decidable; moreover, they showed that if there is an operator F that solves the Church Synthesis Problem, then it can also be solved by an operator defined by a finite state automaton or equivalently by an MLO formula. We investigate a parameterized version of the Church synthesis problem. In this version &psi; might contain as a parameter a unary predicate P. We show that the Church synthesis problem for P is computable if and only if the monadic theory of <Nat,<,P> is decidable. We prove that the Büchi-Landweber theorem can be extended only to ultimately periodic parameters. However, the MLO-definability part of the Büchi-Landweber theorem holds for the parameterized version of the Church synthesis problem.


Source : oai:arXiv.org:0708.3477
DOI : 10.2168/LMCS-3(4:9)2007
Volume: Volume 3, Issue 4
Published on: November 14, 2007
Submitted on: January 3, 2007
Keywords: Computer Science - Logic in Computer Science,F.4.1,F.4.3


Share

Consultation statistics

This page has been seen 50 times.
This article's PDF has been downloaded 14 times.