Tuning Trains Speed in Railway Scheduling
Étienne André
TL;DR
The paper addresses railway scheduling under uncertain speeds by modeling segment traversal times as parametric durations and encoding trajectory constraints with parametric timed automata. It proposes a modular translation where each train and constraint becomes a separate PTA, and the overall system is the parallel composition synchronized on arrival/departure actions. Using the IMITATOR tool, the authors synthesize admissible parameter valuations for durations and constraints, demonstrating results on constrained railway systems, including bounds such as arrival constraints and segment-duration relations. The work shows that this PTA-based framework can automatically compute feasible schedules under uncertainty and suggests future enhancements for acceleration/deceleration modeling and scalability via reductions.
Abstract
Railway scheduling consists in ensuring that a set of trains evolve in a shared rail network without collisions, while meeting schedule constraints. This problem is notoriously difficult, even more in the case of uncertain or even unknown train speeds. We propose here a modeling and verification approach for railway scheduling in the presence of uncertain speeds, encoded here as uncertain segment durations. We formalize the system and propose a formal translation to parametric timed automata. As a proof of concept, we apply our approach to benchmarks, for which we synthesize using IMITATOR suitable valuations for the segment durations.