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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The event that two or more trains reach the end of their sections simultaneously has measure zero and may be ignored.
- 2.
Our experiment files can be found online at http://people.cs.aau.dk/~florber/TrainGames/ExperimentFiles.rar.
References
Danish railway station plans. https://www.sporskiftet.dk/wiki/danske-spor-og-stationer-sporplaner-og-link/. Accessed 14 Jan 2019
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Aristyo, B., Pradityo, K., Tamba, T.A., Nazaruddin, Y.Y., Widyotriatmo, A.: Model checking-based safety verification of a Petri net representation of train interlocking systems. In: 2018 57th Annual Conference of the Society of Instrument and Control Engineers of Japan (SICE), pp. 392–397, September 2018
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7
Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Formal verification of a railway interlocking system using model checking. Formal Aspects Comput. 10(4), 361–380 (1998)
David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206–211. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_16
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer 17(4), 397–415 (2015)
Eriksen, A.B., et al.: Uppaal stratego for intelligent traffic lights. In: 12th ITS European Congress (2017)
Giua, A., Seatzu, C.: Modeling and supervisory control of railway networks using Petri nets. IEEE Trans. Autom. Sci. Eng. 5(3), 431–445 (2008)
Hansen, M.R.: On-the-Fly Solving of Railway Games (work in progress). Waldén, M. (ed.), p. 34 (2017)
Haxthausen, A.E.: Automated generation of formal safety conditions from railway interlocking tables. STTT 16(6), 713–726 (2014)
Kasting, P., Hansen, M.R., Vester, S.: Synthesis of railway-signaling plans using reachability games. In: Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2016, pp. 9:1–9:13. ACM, New York (2016)
Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Safe and optimal adaptive cruise control. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 260–277. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23506-6_17
Petersen, J.L.: Automatic verification of railway interlocking systems: a case study. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, FMSP 1998, pp. 1–6. ACM, New York (1998)
Watkins, C.J.C.H., Dayan, P.: Q-learning. Mach. Learn. 8(3), 279–292 (1992)
Winter, K.: Model checking railway interlocking systems. In: Proceedings of the Twenty-fifth Australasian Conference on Computer Science, ACSC 2002, vol. 4, pp. 303–310. Australian Computer Society Inc., Darlinghurst (2002)
Acknowledgments
We would like to thank to Peter G. Jensen for his support with the experiments and advice on Uppaal Stratego. We also thank the anonymous reviewers for their detailed comments and in particular for pointing out a problem in our original formal model that could have made the constructed controller potentially unsafe. The research leading to these results has received funding from the project DiCyPS funded by the Innovation Fund Denmark, the Sino Danish Research Center IDEA4CPS and the ERC Advanced Grant LASSO. The fourth author is partially affiliated with FI MU, Brno, Czech Republic.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Karra, S.L., Larsen, K.G., Lorber, F., Srba, J. (2019). Safe and Time-Optimal Control for Railway Games. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2019. Lecture Notes in Computer Science(), vol 11495. Springer, Cham. https://doi.org/10.1007/978-3-030-18744-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-18744-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-18743-9
Online ISBN: 978-3-030-18744-6
eBook Packages: Computer ScienceComputer Science (R0)