Expressive power and complexity of temporal logics for model-checking [ 2002-05-01 - 2003-04-30 ]

Research Grant

Researchers: Dr Rajeev Gore (Chief Investigator) ,  Dr Stéphane Demri (Chief Investigator) ,  Prof Jean Goubault-Larrecq (Chief Investigator) ,  Dr Jennifer Davoren (Partner Investigator) ,  The Australian National University (Managed by)

Brief description Expressive power and complexity of temporal logics for model-checking. Hardware verification based upon mathematical logic is now routinely\r\nused in industry to verify the correctness of large digital circuits\r\nusing a technique called model-checking. Such discrete systems move\r\nfrom one state to another according to the regular ticks of a clock.\r\nThe challenge now is to find tractable methods for reasoning about\r\nreal-time systems and hybrid systems that move in a continuous manner\r\nwith respect to time: examples include aeroplanes flying according to\r\nthe laws of physics and a moving robot arm. We shall invent new logics\r\nwhich are specifically tailored for tractable reasoning about\r\nreal-time and hybrid systems.

Funding Amount $11,000

Funding Scheme Linkage - International

View this grant in the ARC Data Portal