Skip past navigation NASA Langley Formal Methods


home

welcome

quick page

philosophy

team

research

quote

links

new?
  home > research

Spacecraft Autonomy and AI Planning

One of the main obstacles hindering the adoption of autonomous software for man-rated critical applications is the lack of a rigorous means of establishing the safety of these systems. Although AI-based autonomous software can provide enormous capability and flexibility, this power comes at a price: the verification and validation problem is greatly exacerbated. Traditional simulation based testing methods fall short of providing the needed level of confidence level. In other application domains, formal methods have been developed which explore the entire state space of the application providing rigorous guarantees about critical safety properties of the application. Unfortunately little progress has been made to date in applying formal methods to AI-based autonomous software systems. Some ground breaking work has been made by Charles Pecheur of NASA Ames [1,2,3] , but there are huge challenges in making techniques such as these practical for the system being developed under the Spacecraft Autonomy for Vehicles and Habitats Project. In [2] Menzies and Pecheur write
    The main challenge in verifying AI software (or, for that matter, any kind of complex system) comes from the number of different possible executions that have to be taken into account. We refer broadly to this uncertainty on a system's future behavior as non-determinism. Non-deterministic choices come from incoming external events, scheduling of concurrent tasks, or even intentional random choices in the program, to name a few. Every choice point in the execution results in as many possible subsequent execution branches. Typically, those choices compound into exponentially many possible executions. This is known as the state space explosion phenomenon.
Note: The link to external site tag identifies links that are outside of the NASA domain.

Publications

  • Plan Verification

    A Plan Preparation Language, Ricky Butler and César Muñoz, NASA/TM-2006-214518, Nov 2006.

    The ANMLite Language and Logic for Specifying Planning Problems, Ricky Butler, Radu Siminiceanu and César Muñoz, NASA/TM-2007-215088, Nov 2007.

    Solving the AI Planning Plus Scheduling Problem Using Model Checking via Automatic Translation from the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL) , Ricky Butler, César Muñoz, and Radu Siminiceanu NASA/TM-2007-215089 , Nov 2007.

  • Formal Semantics of Plexil

    Model Checking Abstract PLEXIL Programs with SMART, Radu Siminiceanu NASA/CR-2007-214542,NIA Report No. 2007-02, April 2007.

 

  Skip past navigation  
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 26 September 2003 (10:10:40)