Church Synthesis Problem with Parameters

DOI10.1007/11874683_36MaRDI QIDQ3613362zbMATH OpenOpenAlexFDO

Authors Alexander Rabinovich

Publication date 12 March 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0708.3477

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Automata and formal grammars in connection with logical questions (03D05)

Abstract: For a two-variable formula ψ(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 ψ(X,F(X)) is universally valid over Nat. B"{u}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 ψ 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"{u}chi-Landweber theorem can be extended only to ultimately periodic parameters. However, the MLO-definability part of the B"{u}chi-Landweber theorem holds for the parameterized version of the Church synthesis problem.

Recommendations

• The Church Synthesis Problem with Parameters
• Decidable Extensions of Church’s Problem
• The Church problem for expansions of \((\mathbb{N},<)\) by unary predicates
• Logical Refinements of Church’s Problem
• The Church synthesis problem with metric

Cited in

(4)

• The Church synthesis problem with metric
• Decidable Extensions of Church’s Problem
• The Church Synthesis Problem with Parameters
• The Church problem for expansions of \((\mathbb{N},<)\) by unary predicates

This page was built for publication: Church Synthesis Problem with Parameters

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3613362)