Expressive power & complexity of temporal logic for model-checking

Hardware verification based upon mathematical logic is now routinely used in industry to verify the correctness of large digital circuits using a technique called model-checking. Such discrete systems move from one state to another according to the regular ticks of a clock. The challenge now is to find tractable methods for reasoning about real-time systems and hybrid systems that move in a continuous manner with respect to time: examples include aeroplanes flying according to the laws of physics and a moving robot arm. We shall invent new logics which are specifically tailored for tractable reasoning about real-time and hybrid systems.