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-by-construction" 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. Education and outreach activities include involvement of undergraduate and graduate students in the research, integration of the research into courses, demonstrations for K-12 students, and recruitment of research participants from under-represented demographic groups. Data, code, and teaching materials developed by the project are disseminated publicly on the Web.

This research investigates a cyber-physical framework for scalable, long-term monitoring and maintenance of civil infrastructures. With growth of the world economy and its population, there has been an ever increasing dependency on larger and more complex networks of civil infrastructure as evident in the billions of dollars spent by the federal, state and local governments to either upgrade or repair transportation systems or utilities. Despite these large expenditures, the nation continues to suffer staggering consequences from infrastructural decay. Therefore, paramount to the concept of a smart city of the future is the concept of smart civil infrastructure that can self-monitor itself to predict any impending failures and in the cases of extreme events (e.g. earthquakes) identify portions that would require immediate repair, and prioritize areas for emergency response. A goal of this research project is to make significant progress towards this grand vision by investigating a framework of infrastructural Internet-of-Things (i-IoT) using a network of self-powered, embedded health monitoring sensors. The collaborative and interdisciplinary nature of this research would provide opportunities for unique outreach programs involving undergraduate and graduate students in technical areas, e.g., sensors, IoTs and structural health monitoring. The project would also provide avenues for disseminating the results of this research to stakeholders in the state governments and for translating the results of the research into field deployable prototypes. This research addresses different elements of the proposed i-IoT framework by bringing together expertise from three universities in the area of self-powered sensors, energy scavenging processors, structural health monitoring and earthquake engineering. At the fundamental level, the project involves investigating self-powered sensors that will require zero maintenance and can continuously operate over the useful lifespan of the structure without experiencing any downtime. The challenge in this regard is that sensors need to occupy a small enough volume such that an array of these devices could be easily embedded and can provide accurate spatial resolution in structural imaging. This research is also investigates techniques that would enable real time wireless collection of data from an array of self-powered sensors embedded inside a structure, without taking the structure out-of-service. The methods to be explored involve combining the physics of energy scavenging, transduction, rectification and logic computation to improve the system's energy-efficiency and reduce the system latency. At the algorithmic level the project explores novel structural failure prediction and structural forensic algorithms based on historical data collected from self-powered sensors embedded at different spatial locations. This includes kernel algorithms that can exploit the data to quickly identify the most vulnerable part of a structure after a man-made or a natural crisis (for example an earthquake). Finally, the technology translation plan for this research is to validate the proposed i-IoT framework in real-world deployment, which includes buildings, multi-span bridges and highways.