Extensions of the Church Synthesis Problem

在理论计算机科学中，综合是指采用逻辑规范，确定它是否可实现，如果是，则生成满足规范的实现的过程。因此，综合涉及到从系统的高级描述性视图到更面向实现的视图的通道。理想情况下，综合问题的解决方案涉及一个决策过程，该过程根据规范自动生成实现。一般来说，不可能自动合成实现。然而，通过仔细限制规范和实现形式主义，可以实现可判定性。综合问题的起源可以追溯到20世纪60年代逻辑学家阿朗佐·丘奇（Alonzo Church）的一篇有影响力的论文，该论文提出了在自然数上综合用二阶一元逻辑编写的规范的有限状态机实现的问题。我们在这个项目中寻求的就是这种方法，我们计划研究的一个方向是不仅要求规范，而且要求实现以逻辑形式给出。这是一个更小的步骤，比直接提炼到一个状态机的实现，并打开了一个抽象的方式来理解之间的关系的相对表现力和复杂性的规范和实现formalism.In另一个方向，我们计划考虑的挑战性问题，从实时规范合成实时系统。实时系统包括物理硬件、实时控制器、通信协议和嵌入式系统。为了准确地模拟这样的系统，必须考虑实时行为，例如，硬件中的延迟、协议中的超时或来自环境的刺激的频率。这里的主要挑战是，实现一个非平凡的实时规范要求我们超越有限状态实现。最后，我们计划考虑相对于甲骨文的合成。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.