Extensions of the Church Synthesis Problem

点击翻译按钮获取中文摘要

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.