一句话：将 Church 合成问题从离散时间推广到非负实数连续时间，并揭示其与离散情形的本质差异。
Church 合成问题研究：给定输入 ω-串 I 与输出 ω-串 O 之间的逻辑规格 A(I,O)，构造过程以判定是否存在算子 F，使得对所有输入 I 都有 A(I,F(I)) 成立。Büchi 和 Landweber 曾针对 MSO 规格与有限状态自动机可计算的算子给出求解过程。本文将该合成问题推广到非负实数的连续时间域，考察连续时间信号上的输入输出规格与可实现性。论文表明，连续时间域中会出现与自然数离散时间域非常不同的现象，从而说明经典有限状态自动机框架下的 Church 合成理论不能直接照搬。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2404-04782,
title = {The Church Synthesis Problem over Continuous Time},
author = {Alexander Rabinovich and Daniel Fattal},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:8)2025}
}