Abstract
Railway scheduling is a complex and safety critical problem that has recently attracted attention in the formal verification community. We provide a formal model of railway scheduling as a stochastic timed game and using the tool Uppaal Stratego, we synthesise the most permissive control strategy for operating the lights and points at the railway scenario such that we guarantee system's safety (avoidance of train collisions). Among all such safe strategies, we then select (with the help of reinforcement learning) a concrete strategy that minimizes the time needed to move all trains to their target locations. This optimizes the speed and capacity of a railway system and advances the current state-of-the-art where the optimality criteria were not considered yet. We successfully demonstrate our approach on the models of two Danish railway stations, and discuss the applicability and scalability of our approach.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings of International Conference on Reliability, Safety and Security of Railway Systems: Modelling, Analysis, Verification and Certification (RSSRail'19) |
Redaktører | Simon Collart-Dutilleul, Alexander Romanovsky, Thierry Lecomte |
Antal sider | 17 |
Forlag | Springer |
Publikationsdato | 2019 |
Sider | 106-122 |
ISBN (Trykt) | 978-3-030-18743-9 |
ISBN (Elektronisk) | 978-3-030-18744-6 |
DOI | |
Status | Udgivet - 2019 |
Begivenhed | Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. - Lille, Lille, Frankrig Varighed: 4 jun. 2019 → 6 jun. 2019 https://conferences.ncl.ac.uk/rssrail2019/ |
Konference
Konference | Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. |
---|---|
Lokation | Lille |
Land/Område | Frankrig |
By | Lille |
Periode | 04/06/2019 → 06/06/2019 |
Internetadresse |
Navn | Lecture Notes in Computer Science |
---|---|
Vol/bind | 11495 |
ISSN | 0302-9743 |