Formal Specification and Correct-by-Construction Synthesis of Control Protocols for Adaptable, Human-Embedded Autonomous Systems
Technical point of contact: Dr. Laura Humphrey, Air Force Research Lab (RQQA)
Period of activity: 2015-2018
Collaborators: Behcet Acikmese
Overview of the Project
- 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.