For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 2019/02/01
Online ISSN: 1745-1337
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(5.2MB)
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.