Autonomy Protocols- From Human Behavioral Modeling to Correct-by-Construction, Scalable Control Poster.pdf

Computer systems are increasingly coming to be relied upon to augment or replace human
operators in controlling mechanical devices in contexts such as transportation systems, chemical
plants, and medical devices, where safety and correctness are critical. A central problem is how
to verify that such partially automated or fully autonomous cyber-physical systems (CPS) are
worthy of our trust. One promising approach involves synthesis of the computer implementation
codes from formal specifications, by software tools. This project contributes to this "correct-byconstruction"
approach, by developing scalable, automated methods for the synthesis of control
protocols with provable correctness guarantees, based on insights from models of human
behavior. It targets: (i) the gap between the capabilities of today's hardly autonomous, unmanned
systems and the levels of capability at which they can make an impact on our use of monetary,
labor, and time resources; and (ii) the lack of computational, automated, scalable tools suitable
for the specification, synthesis and verification of such autonomous systems.
The research is based on study of modular reinforcement learning-based models of human
behavior derived through experiments designed to elicit information on how humans control
complex interactive systems in dynamic environments, including automobile driving.
Architectural insights and stochastic models from this study are incorporated with a specification
language based on linear temporal logic, to guide the synthesis of adaptive autonomous
controllers. Motion planning and other dynamic decision-making are by algorithms based on
computational engines that represent the underlying physics, with provision for run-time
adaptation to account for changing operational and environmental conditions. Tools
implementing this methodology are validated through experimentation in a virtual testing facility
in the context of autonomous driving in urban environments and multi-vehicle autonomous
navigation of micro-air vehicles in dynamic environments.