| EPSRC Reference: |
EP/H018581/1 |
| Title: |
Extensions of the Church Synthesis Problem |
| Principal Investigator: |
Worrell, Professor JB |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research |
| Starts: |
08 December 2009 |
Ends: |
07 September 2010 |
Value (£): |
60,867
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
30 Sep 2009
|
ICT Prioritisation Panel (Oct 09)
|
Announced
|
|
|
Summary on Grant Application Form |
|
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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ox.ac.uk |