Railway Scheduling Using Boolean Satisfiability Modulo Simulations

Autoři: doc. Dipl. Ing. Stefan Ratschan, Dr. tech.
Rok vydání: 2023
Typ publikace: Konferenční příspěvek (mezinárodní konf.)
Periodikum: Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings
Projekty: Kvazirozhodovací procedury pro logické teorie reálných funkcí
Bibliografická citace: KOLÁRIK, T., RATSCHAN, Stefan. Railway Scheduling Using Boolean Satisfiability Modulo Simulations. In: CHECHIK, M., KATOEN, J.-P., LEUCKER, M., eds. Formal Methods: 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings. Cham: Springer, 2023, S. 56-73. Lecture Notes in Computer Science, 14000. ISBN 978-3-031-27480-0. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-031-27481-7_5.
DOI: 10.1007/978-3-031-27481-7_5
ID: 570721
Online záznam: Zobrazit online záznam

Abstrakt

Railway scheduling is a problem that exhibits both non-trivial discrete and continuous behavior. In this paper, we model this problem using a combination of SAT and ordinary differential equations (SAT modulo ODE). In addition, we adapt our existing method for solving such problems in such a way that the resulting solver is competitive with methods based on dedicated railway simulators while being more general and extensible.