Model-Checking Algorithms for Timed Systems

As computer systems become ubiquitous, it becomes increasingly urgent to develop analysis techniques and tools to guarantee that they operate as intended. Many safety-critical systems deployed today, from ABS braking technology in cars to avionics control, can be viewed as timed systems, in that their correct behaviour depends crucially on their meeting various timing constraints. There is by now healthy body of techniques and tools dedicated to the analysis of untimed systems. Formal analysis methods for timed systems, however, are still in their infancy. The goal of this project is to investigate the theoretical underpinnings and practical applicability of algorithms for analysing timed systems. More specifically, we intend to study a well-known formalism for expressing timed specifications, called Metric Temporal Logic, and develop efficient algorithms for verifying that a given timed system (suitably represented mathematically as a so-called timed automaton) meets a given Metric Temporal Logic formula. The project is based on very recent algorithmic breakthroughs concerning the analysis of Metric Temporal Logic. We intend to study the complexity of such algorithms, as well as various heuristics for accelerating them. The flavour of the project is mainly theoretical; however, we aim to implement our work and test it on various case studies to evaluate how well our algorithms work in practice.