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  

Publication
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)
Category: 
Keyword: 
formal approach,  train timetable,  mesoscopic model,  periodic timetable,  SMT-Solver,  railway capacity,  

Full Text: FreePDF(5.2MB)


Summary: 
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.