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.