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.

The proposed research concerns the problem of synthesizing system components from high-level input-output logical specifications. The motivation for the synthesis problem that we study originally came from the theory of sequential circuits, and we consider that the potential long-term beneficiaries are hardware and software companies. While propositional logic synthesis is already used in VLSI design to great effect, the version of the synthesis problem that we study is much more challenging from an algorithmic point of view since it involves temporal and predicate logics. Nevertheless, given the increasing complexity of modern software and hardware systems, and the need to optimize designs with respect to area, speed or power, there is a clear need to provide further automated support to designers. Thus, while automated synthesis for highly expressive specification languages, such as predicate and temporal logics, is an ambitious goal, and carries a significant element of risk, we feel that research in this area has the potential for great impact over the long term. This grant proposes to do foundational research. Given the current state of the art, it is unrealistic to expect direct or short-term industrial applications of this work. In particular, the field is not sufficiently well developed to consider industrial case studies. However we believe that foundational research will prove indispensable for unlocking the potential of automatic synthesis. By analogy with the closely related field of model checking, we believe the time period between foundational studies and industrial benefits being realized could be up to twenty years. The influence of this research will necessarily be mediated through subsequent application-oriented research. Thus our main strategy to maximize the impact of the research is through disseminating our results to other researchers working in automated verification.