Using Model Checking to Validate AI Planner Domain Models
John Penix, Charles Pecheur, Klaus Havelund · 1999
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. 1 Introduction In the classical approach to analyzing the correctness of a piece of software is broken into two tasks: verification and validation. Verification is the task of making sure that the software implementation complies with a stated set of requirements. Validation is making sure that the stated requirements correctly reflect the needs of the end user. In the ...