Formal Specification and Correct-by-Construction Synthesis of Control Protocols for Adaptable, Human-Embedded Autonomous Systems

Jump to: navigation, search

Technical point of contact: Dr. Laura Humphrey, Air Force Research Lab (RQQA)
Period of activity: 2015-2018
Collaborators: Behcet Acikmese

Overview of the Project

The objective of this project is to develop methods and computational tools for formal specification, analysis, and correct-by-construction (with respect to rich temporal logic specifications) synthesis of adaptable, hierarchical control protocols for human-embedded, multi-vehicle autonomous systems. Our work makes novel connections between controls, computer science formal methods, convex optimization, learning theory, and human factors. We closely collaborate with researchers from the Air Force Research Lab for domain specific insights.

The project is structured into four main research thrusts described by the main questions investigated in each thrust:


A schematic for human-embedded autonomous systems: Multiple unmanned vehicle with heterogenous capabilities for navigation and sensing deliver a joint mission with an operator.

  • Thrust (1) Efficient and reliable computation engines for high-fidelity dynamic modeling: How can we scalably incorporate high-fidelity dynamic models of the autonomous systems into autonomy protocol synthesis?
  • Thrust (2) Formally embedding the operators into the execution of autonomy protocols: How can we formally define human-embedded, flexibly adjustable autonomy and develop synthesis algorithms for the co-design of control protocols and the information content of operator interfaces?
  • Thrust (3) Automated feedback generation and inference of specifications: How can we render the automated synthesis procedure transparent and interpretable to human operators/designers by generating informative feedback and diverse design planning choices to them and inferring their preferences and requirements as mathematically-based specifications?
  • Thrust (4) Learning-based adaptation with provable correctness guarantees: How can we develop protocols that both react to anticipated environmental changes and adapt to unforeseen contextual changes with provable guarantees of correctness with respect to temporal logic specifications?

We demonstrate the progress on case studies motivated by the operation of multi-UAV teams along with adversaries, cooperating assets, and human operators.