Whenever a train is delayed, this may cause delays for further trains. For example, a further connection might have to wait for the given train, or the movement of the delayed train outside of the usual schedule might case a capacity problem on its track. Traditionally, such consequences of delays are analyzed using random (i.e., Monte-Carlo) simulations which may miss important corner cases. The formalism of timed automata avoids this problem by using a symbolic representation that allows for exhaustive simulation.
In the thesis, the student will take advantage of this by creating a model of train delays based on timed automata, and investigating the properties of simulations of the resulting model.