Automated planning systems (APS) are gaining acceptance for use on NASA missions as evidenced by APS flown On missions such as Orbiter and Deep Space 1 both of which were commanded by onboard planning systems. The planning system takes high level goals and expands them onboard into a detailed of action fiat the spacecraft executes. The system must be verified to ensure that the automatically generated plans achieve the goals as expected and do not generate actions that would harm the spacecraft or mission. These systems are typically tested using empirical methods. Formal methods, such as model checking, offer exhaustive or measurable test coverage which leads to much greater confidence in correctness. This paper describes a formal method based on the SPIN model checker. This method guarantees that possible plans meet certain desirable properties. We express the input model in Promela, the language of SPIN and express the properties of desirable plans formally.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Model Checking Artificial Intelligence Based Planners: Even the Best Laid Plans Must Be Verified


    Beteiligte:

    Kongress:

    IEEE Aerospace Conference ; 2005 ; Big Sky, MT, United States


    Erscheinungsdatum :

    2005-03-05


    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Keine Angabe


    Sprache :

    Englisch




    Model Checking Autonomous Planners: Even the Best Laid Plans Must be Verified

    Smith, M. H. / Cucullu, G. C. / Smith, B. D. et al. | British Library Conference Proceedings | 2005


    Verifying AI Plan Models: Even the Best Laid Plans Need to be Verified

    Smith, Margaret / Cucullu, Gordon / Holzmann, Gerard et al. | NTRS | 2004


    The Best Laid Plans of Mice and Men

    Roess, Roger P. / Sansone, Gene | Springer Verlag | 2013


    Performance Metric for Plans, Projects, and Planners

    Strader, Brad | Online Contents | 2012


    Model Checking UAV Mission Plans

    Humphrey, L. / American Institute of Aeronautics and Astronautics | British Library Conference Proceedings | 2012