NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Using Model Checking to Validate AI Planner Domain ModelsThis 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.
Document ID
19990054671
Acquisition Source
Ames Research Center
Document Type
Conference Paper
Authors
Penix, John
(NASA Ames Research Center Moffett Field, CA United States)
Pecheur, Charles
(NASA Ames Research Center Moffett Field, CA United States)
Havelund, Klaus
(NASA Ames Research Center Moffett Field, CA United States)
Date Acquired
August 19, 2013
Publication Date
June 1, 1999
Publication Information
Publication: Proceedings of the Twenty-Third Annual Software Engineering Workshop
Subject Category
Computer Programming And Software
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
Document Inquiry

Available Downloads

There are no available downloads for this record.
No Preview Available