Automatic Generation of Train Timetables from Mesoscopic Railway Models by SMT-Solver

Yoshinao ISOBE  Hisabumi HATSUGAI  Akira TANAKA  Yutaka OIWA  Takanori AMBE  Akimasa OKADA  Satoru KITAMURA  Yamato FUKUTA  Takashi KUNIFUJI  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E102-A   No.2   pp.325-335
Publication Date: 2019/02/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E102.A.325
Type of Manuscript: Special Section PAPER (Special Section on Mathematical Systems Science and its Applications)
formal approach,  train timetable,  mesoscopic model,  periodic timetable,  SMT-Solver,  railway capacity,  

Full Text: FreePDF

This paper presents a formal approach for generating train timetables in a mesoscopic level that is more concrete than the macroscopic level, where each station is simply expressed in a black-box, and more abstract than the microscopic level, where the infrastructure in each station-area is expressed in detail. The accuracy of generated timetable and the computational effort for the generation is a trade-off. In this paper, we design a formal mesoscopic modeling language by analyzing real railways, for example Tazawako-line as the first step of this work. Then, we define the constraint formulae for generating train timetables with the help of SMT (Satisfiability Module Theories)-Solver, and explain our tool RW-Solver that is an implementation of the constraint formulae. Finally, we demonstrate how RW-Solver with the help of SMT-Solver can be used for generating timetables in a case study of Tazawako-line.