| タイトル | Model Checking the Remote Agent Planner |
| 本文（外部サイト） | http://hdl.handle.net/2060/20010097311 |
| 著者（英） | Havelund, Klaus; Norvig, Peter; Muscettola, Nicola; Khatib, Lina |
| 著者所属（英） | NASA Ames Research Center |
| 発行日 | 2001-01-15 |
| 言語 | eng |
| 内容記述 | This work tackles the problem of using Model Checking for the purpose of verifying the HSTS (Scheduling Testbed System) planning system. HSTS is the planner and scheduler of the remote agent autonomous control system deployed in Deep Space One (DS1). Model Checking allows for the verification of domain models as well as planning entries. We have chosen the real-time model checker UPPAAL for this work. We start by motivating our work in the introduction. Then we give a brief description of HSTS and UPPAAL. After that, we give a sketch for the mapping of HSTS models into UPPAAL and we present samples of plan model properties one may want to verify. |
| NASA分類 | Cybernetics, Artificial Intelligence and Robotics |
| 権利 | No Copyright |
| URI | https://repository.exst.jaxa.jp/dspace/handle/a-is/225789 |
