Model-Checking Algorithms for Timed Systems

As computer systems become ubiquitous, it becomes increasingly urgent todevelop analysis techniques and tools to guarantee that they operate asintended. Many safety-critical systems deployed today, from ABS brakingtechnology in cars to avionics control, can be viewed as timed systems, in thattheir correct behaviour depends crucially on their meeting various timingconstraints.There is by now healthy body of techniques and tools dedicated to the analysisof untimed systems. Formal analysis methods for timed systems, however, arestill in their infancy. The goal of this project is to investigate thetheoretical underpinnings and practical applicability of algorithms foranalysing timed systems. More specifically, we intend to study a well-knownformalism 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 agiven Metric Temporal Logic formula.The project is based on very recent algorithmic breakthroughs concerning theanalysis of Metric Temporal Logic. We intend to study the complexity of suchalgorithms, as well as various heuristics for accelerating them. The flavour ofthe project is mainly theoretical; however, we aim to implement our work andtest it on various case studies to evaluate how well our algorithms work inpractice.