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

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.

open access publishing via