IEICE TRANSACTIONS on Information
Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker
Summary :
In this paper, we propose and implement an automated route planning framework for milk-run transport logistics by applying model checking techniques. First, we develop a formal specification framework for milk-run transport logistics. The framework adopts LTL (Linear Temporal Logic), a language based on temporal logics, as a specification language for users to be able to flexibly and formally specify complex delivery requirements for trucks. Then by applying the bounded semantics of LTL, the framework then defines the notion of “optimal truck routes”, which mean truck routes on a given route map that satisfy given delivery requirements (specified by LTL) with the minimum cost. We implement the framework as an automated route planner using the NuSMV model checker, a state-of-the-art bounded model checker. The automated route planner, given route map and delivery requirements, automatically finds optimal trucks routes on the route map satisfying the given delivery requirements. The feasibility of the implementation design is investigated by analysing its computational complexity and by showing experimental results.
- Publication
- IEICE TRANSACTIONS on Information Vol.E96-D No.12 pp.2555-2564
- Publication Date
- 2013/12/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E96.D.2555
- Type of Manuscript
- Special Section PAPER (Special Section on Parallel and Distributed Computing and Networking)
- Category
Authors
Takashi KITAMURA
National Institute of Advanced Industrial Science and Technology (AIST)
Keishi OKAMOTO
Sendai National College of Technology
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
Takashi KITAMURA, Keishi OKAMOTO, "Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker" in IEICE TRANSACTIONS on Information,
vol. E96-D, no. 12, pp. 2555-2564, December 2013, doi: 10.1587/transinf.E96.D.2555.
Abstract: In this paper, we propose and implement an automated route planning framework for milk-run transport logistics by applying model checking techniques. First, we develop a formal specification framework for milk-run transport logistics. The framework adopts LTL (Linear Temporal Logic), a language based on temporal logics, as a specification language for users to be able to flexibly and formally specify complex delivery requirements for trucks. Then by applying the bounded semantics of LTL, the framework then defines the notion of “optimal truck routes”, which mean truck routes on a given route map that satisfy given delivery requirements (specified by LTL) with the minimum cost. We implement the framework as an automated route planner using the NuSMV model checker, a state-of-the-art bounded model checker. The automated route planner, given route map and delivery requirements, automatically finds optimal trucks routes on the route map satisfying the given delivery requirements. The feasibility of the implementation design is investigated by analysing its computational complexity and by showing experimental results.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E96.D.2555/_p
Copy
@ARTICLE{e96-d_12_2555,
author={Takashi KITAMURA, Keishi OKAMOTO, },
journal={IEICE TRANSACTIONS on Information},
title={Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker},
year={2013},
volume={E96-D},
number={12},
pages={2555-2564},
abstract={In this paper, we propose and implement an automated route planning framework for milk-run transport logistics by applying model checking techniques. First, we develop a formal specification framework for milk-run transport logistics. The framework adopts LTL (Linear Temporal Logic), a language based on temporal logics, as a specification language for users to be able to flexibly and formally specify complex delivery requirements for trucks. Then by applying the bounded semantics of LTL, the framework then defines the notion of “optimal truck routes”, which mean truck routes on a given route map that satisfy given delivery requirements (specified by LTL) with the minimum cost. We implement the framework as an automated route planner using the NuSMV model checker, a state-of-the-art bounded model checker. The automated route planner, given route map and delivery requirements, automatically finds optimal trucks routes on the route map satisfying the given delivery requirements. The feasibility of the implementation design is investigated by analysing its computational complexity and by showing experimental results.},
keywords={},
doi={10.1587/transinf.E96.D.2555},
ISSN={1745-1361},
month={December},}
Copy
TY - JOUR
TI - Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker
T2 - IEICE TRANSACTIONS on Information
SP - 2555
EP - 2564
AU - Takashi KITAMURA
AU - Keishi OKAMOTO
PY - 2013
DO - 10.1587/transinf.E96.D.2555
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E96-D
IS - 12
JA - IEICE TRANSACTIONS on Information
Y1 - December 2013
AB - In this paper, we propose and implement an automated route planning framework for milk-run transport logistics by applying model checking techniques. First, we develop a formal specification framework for milk-run transport logistics. The framework adopts LTL (Linear Temporal Logic), a language based on temporal logics, as a specification language for users to be able to flexibly and formally specify complex delivery requirements for trucks. Then by applying the bounded semantics of LTL, the framework then defines the notion of “optimal truck routes”, which mean truck routes on a given route map that satisfy given delivery requirements (specified by LTL) with the minimum cost. We implement the framework as an automated route planner using the NuSMV model checker, a state-of-the-art bounded model checker. The automated route planner, given route map and delivery requirements, automatically finds optimal trucks routes on the route map satisfying the given delivery requirements. The feasibility of the implementation design is investigated by analysing its computational complexity and by showing experimental results.
ER -
English
