Expressive power & complexity of temporal logic for model-checking

  • Gore, Rajeev (PI)
  • Davoren, Jennifer M. (CoI)
  • Demri, Stephane (CoI)
  • Goubault-Larrecq, J (CoI)

    Project: Research

    Project Details

    Description

    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.
    StatusFinished
    Effective start/end date1/05/0230/04/03

    Funding

    • Australian Research Council (ARC): A$11,000.00

    Fingerprint

    Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.