Model Checking Human-Automation UAV Mission Plans

Abstract

The USAF is interested both in techniques for verifying the behavior of autonomous, multi-agent systems and in technologies that improve human-automation collaboration. Model checking – a mathematically based formal method used in system specification, design, and verification – has the potential to address these challenges simultaneously. In particular, the integration of model checking techniques into human-automation mission planning systems could result in several useful features lacking in current systems. For instance, it could allow a human operator to explicitly specify mission goals and constraints, thus enabling the autonomy to make decisions based on a clearer understanding of the human’s intent and to provide better feedback to the human when problems arise. Here, we explore how model checking can be used to assist a human operator in specifying and planning a UAV ISR mission.