Mathematical guarantees for systems that must act at the right time

A railway barrier has one job: to be down before the train arrives, every time. It is one of many systems that must act within strict time limits, from air-traffic control to pacemakers, where a moment's delay can be dangerous.

During his PhD studies, Mikael Bisgaard Dahlsen-Jensen built a tool that works out how to keep such systems acting safely and on time. The right timing values are hard to pin down: some, like how long the barrier takes to lower, are unknown when the system is being designed, and others can never be known exactly, such as when a train reaches the crossing after a sensor trips. On top of that, no designer controls the environment. A driver may weave around a half-lowered barrier, and the system must cope regardless.

Instead of just guessing values and then testing them, his tool computes the answer, automatically working out all the values that are guaranteed safe. It treats the problem as a game, with that uncontrolled environment as a worst-case opponent, and finds a strategy that wins no matter what it does. All of this is built into established verification software, and the underlying method is mathematically proven correct, not just tested, so an engineer can trust its answers before a design is ever built.

The PhD study was completed at the Department of Computer Science, Faculty of Natural Sciences, Aarhus University.

This summary was prepared by the PhD student.

Time: Monday, 26 October 2026 at 13:10
Place: Building 5342, room 333, Ada, Department of Computer Science, Aarhus University, Åbogade 34, 8200 Aarhus N
Title of PhD thesis: Practical Controller Synthesis for Real-Time Systems under Uncertainty
Contact information: Mikael Bisgaard Dahlsen-Jensen, e-mail: mikaelbdj@gmail.com, tel.: +45 31902069
Members of the assessment committee:
Professor Didier Lime, LS2N, École Centrale de Nantes, France
Professor Jiri Srba, Department of Computer Science, Aalborg University, Denmark
Associate Professor Amin Timany (chair), Department of Computer Science, Aarhus University, Denmark
Main supervisor: Professor Jaco van de Pol, Department of Computer Science, Aarhus University, Denmark
Language: The PhD dissertation will be defended in English

The defence is public.
The PhD thesis is available for reading at the Graduate School of Natural Sciences/GSNS, Ny Munkegade 120, building 1521, 8000 Aarhus C