IEICE TRANSACTIONS on Fundamentals
Open Access
Automatic Generation of Train Timetables from Mesoscopic Railway Models by SMT-Solver
-
Full Text Views
59
- Cite this
- Free PDF (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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E102-A No.2 pp.325-335
- Publication Date
- 2019/02/01
- Publicized
- 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
Authors
Yoshinao ISOBE
National Institute of Advanced Industrial Science and Technology
Hisabumi HATSUGAI
National Institute of Advanced Industrial Science and Technology
Akira TANAKA
National Institute of Advanced Industrial Science and Technology
Yutaka OIWA
National Institute of Advanced Industrial Science and Technology
Takanori AMBE
East Japan Railway Company
Akimasa OKADA
East Japan Railway Company
Satoru KITAMURA
East Japan Railway Company
Yamato FUKUTA
East Japan Railway Company
Takashi KUNIFUJI
East Japan Railway Company
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Yoshinao ISOBE, Hisabumi HATSUGAI, Akira TANAKA, Yutaka OIWA, Takanori AMBE, Akimasa OKADA, Satoru KITAMURA, Yamato FUKUTA, Takashi KUNIFUJI, "Automatic Generation of Train Timetables from Mesoscopic Railway Models by SMT-Solver" in IEICE TRANSACTIONS on Fundamentals,
vol. E102-A, no. 2, pp. 325-335, February 2019, doi: 10.1587/transfun.E102.A.325.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E102.A.325/_p
Copy
@ARTICLE{e102-a_2_325,
author={Yoshinao ISOBE, Hisabumi HATSUGAI, Akira TANAKA, Yutaka OIWA, Takanori AMBE, Akimasa OKADA, Satoru KITAMURA, Yamato FUKUTA, Takashi KUNIFUJI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Automatic Generation of Train Timetables from Mesoscopic Railway Models by SMT-Solver},
year={2019},
volume={E102-A},
number={2},
pages={325-335},
abstract={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.},
keywords={},
doi={10.1587/transfun.E102.A.325},
ISSN={1745-1337},
month={February},}
Copy
TY - JOUR
TI - Automatic Generation of Train Timetables from Mesoscopic Railway Models by SMT-Solver
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 325
EP - 335
AU - Yoshinao ISOBE
AU - Hisabumi HATSUGAI
AU - Akira TANAKA
AU - Yutaka OIWA
AU - Takanori AMBE
AU - Akimasa OKADA
AU - Satoru KITAMURA
AU - Yamato FUKUTA
AU - Takashi KUNIFUJI
PY - 2019
DO - 10.1587/transfun.E102.A.325
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E102-A
IS - 2
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - February 2019
AB - 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.
ER -
English
