Tuning Trains Speed in Railway Scheduling

TL;DR

This paper introduces a formal modeling and verification approach for railway scheduling that accounts for uncertain train speeds, enabling the synthesis of safe segment durations using parametric timed automata.

Contribution

It presents a novel formal translation of railway scheduling with uncertain speeds into parametric timed automata and demonstrates its application on benchmarks.

Findings

Successful synthesis of segment durations for benchmarks

Effective modeling of uncertain train speeds

Verification of safety constraints in scheduling

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.