EPSRC logo

Details of Grant 

EPSRC Reference: GR/L87491/02
Title: DEVELOPING CLAUSAL RESOLUTION FOR THE TEMPORAL MU-CALCULUS
Principal Investigator: Fisher, Professor M
Other Investigators:
Bolotov, Dr A Dixon, Dr C
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Liverpool
Scheme: Standard Research (Pre-FEC)
Starts: 10 September 2001 Ends: 09 March 2002 Value (£): 21,235
EPSRC Research Topic Classifications:
Artificial Intelligence
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.liv.ac.uk