Using Model Checking to Validate AI Planner Domain Models
Using Model Checking to Validate AI Planner Domain Models
复制标题
使用模型检查来验证 AI Planner 域模型
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
K. Havelund
中科院分区：
文献类型：
--
作者：
J. Penix;C. Pecheur;K. Havelund
这份报告描述了一个调查使用模型检查，以协助验证域模型的HSTS计划。计划者模型指定使用定量持续时间约束的定性时间间隔逻辑。我们进行了几个实验，将领域建模语言转换为SMV，Spin和Murphi模型检查器。这样就可以直接比较不同系统如何支持特定类型的验证任务。初步结果表明，模型检测是有用的，发现故障的模型，可能不容易识别生成测试计划。
This report describes an investigation into using model checking to assist validation of domain models for the HSTS planner. The planner models are specified using a qualitative temporal interval logic with quantitative duration constraints. We conducted several experiments to translate the domain modeling language into the SMV, Spin and Murphi model checkers. This allowed a direct comparison of how the different systems would support specific types of validation tasks. The preliminary results indicate that model checking is useful for finding faults in models that may not be easily identified by generating test plans.