| EPSRC Reference: |
GR/L87491/01 |
| Title: |
DEVELOPING CLAUSAL RESOLUTION FOR THE TEMPORAL MU-CALCULUS |
| Principal Investigator: |
Fisher, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing and Mathematics |
| Organisation: |
Manchester Metropolitan University |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
15 June 1998 |
Ends: |
31 December 2000 |
Value (£): |
125,281
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Temporal mu-calculus was introduced as an extension of propositional temporal logic with fixed points representing maximal and minimal solutions to temporal equations. One of the crucial features of the mu-calculus is its use of a recursion operator as a basic connective, thus allowing the representation of recurrent properties in a natural way. These features of the mu-calculus allow it to be applied in both hardware and software verification.Resolution has been shown to be an effective method for theorem-proving across a range of different logics. We have developed a clausal resolution method for linear-time temporal logic and are currently extending it to both branching-time temporal logic and temporal logics of knowledge and belief. In addition to being relatively simple to understand, this approach admits practical implementation techniques.The aim of this project is to develop a clausal resolution method for the temporal mu-calculus. Initially, linear-time mu-calculus will be considered, and a prototype system will be produced. Then simple branching-time calculi will be considered before tackling the full branching-time mu-calculus.We believe that the success of this research will lead to improved practical verification techniques for complex reactive systems.
|
|
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.mmu.ac.uk |