The Church Synthesis Problem over Continuous Time
The Church Synthesis Problem over Continuous Time
The Church Problem asks for the construction of a procedure which, given a logical specification A(I,O) between input omega-strings I and output omega-strings O, determines whether there exists an operator F that implements the specification in the sense that A(I, F(I)) holds for all inputs I. Buchi and Landweber provided a procedure to solve the Church problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time domain of the non-negative reals. We show that in the continuous time domain there are phenomena which are very different from the canonical discrete time domain of the natural numbers.
Daniel Fattal、Alexander Rabinovich
自动化基础理论计算技术、计算机技术
Daniel Fattal,Alexander Rabinovich.The Church Synthesis Problem over Continuous Time[EB/OL].(2025-07-22)[2025-08-10].https://arxiv.org/abs/2404.04782.点此复制
评论