Expressive power and complexity of temporal logics for model-checking

点击翻译按钮获取中文摘要

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.