GRAVITAS: A Model Checking Based Planning and Goal Reasoning Framework
  for Autonomous Systems
  While AI techniques have found many successful applications in autonomous
systems, many of them permit behaviours that are difficult to interpret and may
lead to uncertain results. We follow the "verification as planning" paradigm
and propose to use model checking techniques to solve planning and goal
reasoning problems for autonomous systems. We give a new formulation of Goal
Task Network (GTN) that is tailored for our model checking based framework. We
then provide a systematic method that models GTNs in the model checker Process
Analysis Toolkit (PAT). We present our planning and goal reasoning system as a
framework called Goal Reasoning And Verification for Independent Trusted
Autonomous Systems (GRAVITAS) and discuss how it helps provide trustworthy
plans in an uncertain environment. Finally, we demonstrate the proposed ideas
in an experiment that simulates a survey mission performed by the REMUS-100
autonomous underwater vehicle.
