Autonomy Protocols: From Human Behavioral Modeling to Correct-By-Construction, Scalable Control
Technical point of contact: David Corman, NSF
Period of activity: 2014-2018
Collaborators: Mary Hayhoe and Dana Ballard (Texas). Behcet Acikmese (Univ of Washington)
NSF grant page
Poster from the PI meeting
Overview of the Project
The objective of this project is to develop scalable, automated methods for the synthesis of autonomy control protocols with provable correctness guarantees, incorporating insights from models of human behavior. Specifically, we formalize correctness by merging rich temporal logic specifications and potentially hybrid system models. We utilize architectural decompositions of the underlying decision-making problems toward improved scalability. Novel empirical and mathematical insights to be generated in-house on how humans manage complexity and diverse sensing in relevant contexts as they, for example, move through dynamic environments will (i) guide architectural exploration for suitable hierarchical decompositions and (ii) help manageably couple control and sensing/perception. We then instantiate those of the decision-making hierarchies identified as "promising" by developing correct-by-synthesis protocols from formal temporal logic specifications and customized algorithms for robust, constrained optimal control suitable for verifiably reliable real-time implementations.
We partition the proposed activities into three main research thrusts:
- Modeling of human sensory-motor decisions and empirical assessment of the candidate modular decision-making architectures: How do humans decompose a complex decision-making problem into tractable subproblems? How can we mathematically represent the underlying decompositions and systematically guide architectural exploration in autonomy protocol synthesis?
- Integrating the architectural insights into hierarchical, autonomous decision-making: How can we develop synthesis problems, i.e., formal models, constraints, specifications, and information flow patterns, for each of the layers in the candidate hierarchy? How can we ensure the consistency between the layers?
- Reliable, run-time computation engines for motion planning and abstractions of system dynamics: How can we efficiently incorporate uncertainty and constraints into run-time motion planning over continuous state spaces and represent continuous physics for high-level decision-making? How can we provably reliably perform the underlying computations?