Extensions of the Church Synthesis Problem

在理论计算机科学中，综合是指采用逻辑规范，确定其是否可实现，如果可实现，则生成符合规范的实现的过程。因此，综合涉及到从系统的高级描述性视图到更面向实现的视图的过渡。理想情况下，综合问题的解决方案包括一个从规范自动生成实现的决策过程。一般来说，自动合成实现是不可能的。然而，通过仔细限制规范和实现形式，可以实现可决定性。综合问题的起源可以追溯到逻辑学家Alonzo Church在20世纪60年代发表的一篇有影响力的论文，该论文提出了在自然数上用二阶一元逻辑编写的规范的有限状态机实现的综合问题。这正是我们在这个项目中寻求发展的方法。我们计划研究的一个方向是，不仅要求规范，而且要求实现以逻辑形式给出。与直接细化到状态机实现相比，这是一个更小的步骤，并且为以抽象的方式理解规范和实现形式化的相对表达性和复杂性之间的关系开辟了道路。在另一个方向上，我们计划考虑从实时规范中合成实时系统的挑战性问题。实时系统包括物理硬件、实时控制器、通信协议和嵌入式系统。为了准确地模拟这样的系统，必须考虑实时行为，例如，硬件的延迟，协议的超时或来自环境的刺激频率。这里的主要挑战是实现一个重要的实时规范要求我们超越有限状态实现。最后，我们打算考虑合成与神谕的关系。可以在规范和实现中使用的oracle模型背景知识。即使这样一个神谕可以指的信息只是半可计算的，我们仍然希望能够说，相对于这样一个神谕的合成是可决定的。

In theoretical computer science, synthesis refers to the process of taking a logical specification, determining whether it is realizable, and, if so, generating an implementation that meets the specification. Thus synthesis involves the passage from a high-level descriptive view of a system to a more implementation-oriented view. Ideally a solution to the synthesis problem involves a decision procedure that generates the implementation automatically from the specification. In full generality it is not possible to automatically synthesize implementations. However, by carefully restricting the specification and implementation formalisms one can achieve decidability. One can trace the origins of the synthesis problem to an influential paper by the logician Alonzo Church in the 1960s, which posed the problem of synthesizing finite-state machine implementations of specifications written in second-order monadic logic over the natural numbers. It is this approach that we seek to develop in this project.One direction we plan to investigate asks that not only the specification, but also the implementation be given in a logical formalism. This is a smaller step than refining directly to a state machine implementation and opens the way to understand in an abstract way the relationship between the relative expressiveness and complexity of the specification and implementation formalisms.In another direction we plan to consider the challenging problem of synthesizing real-time systems from real-time specifications. Real-time systems include physical hardware, real-time controllers, communication protocols and embedded systems. To accurately model such systems one must take account of real-time behaviour, e.g., latency in hardware, timeouts in protocols or the frequency of stimuli from the environment. The major challenge here is that implementing a non-trivial real-time specification requires that we go beyond finite-state implementations.Finally we plan to consider synthesis relative to oracles. Oracles model background knowledge that can be used both in the specification and implementation. Even though such an oracle could refer to information that is only semi-computable, we still want to be able to say that synthesis relative to such an oracle is decidable.