The Church problem for expansions of (N,

Inf. Comput.(2012)

引用 1|浏览0
暂无评分
摘要
For a two-variable formula B(X,Y) of Monadic Logic of Order (MLO) the Church synthesis problem concerns the existence and construction of a finite-state operator Y=F(X) such that B(X,F(X)) is universally valid over Nat. Buchi and Landweber (1969) proved that the Church synthesis problem is decidable. We investigate a parameterized version of the Church synthesis problem. In this extended version a formula B and a finite-state operator F might contain as a parameter a unary predicate P. A large class of predicates P is exhibited such that the Church problem with the parameter P is decidable. Our proofs use composition method and game theoretical techniques.
更多
查看译文
关键词
finite-state operator Y,extended version,two-variable formula B,Church synthesis problem,parameterized version,Church synthesis problem concern,Church problem,formula B,parameter P,finite-state operator F
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要