The goal of my research is to enable safe and reliable integration of human-robot systems in our society by providing a unified framework for modeling and design of these systems. Today's society is rapidly advancing towards autonomous systems that interact and collaborate with humans, e.g., semiautonomous vehicles interacting with drivers and pedestrians, medical robots used in collaboration with doctors, or service robots interacting with their users in smart homes. The safety-critical nature of these systems require us to provide provably correct guarantees about their performance. In this dissertation, we develop a formalism for the design of algorithms and mathematical models that enable correct-by-construction control and verification of human-robot systems.

We focus on two natural instances of this agenda. In the first part, we study interaction-aware control, where we use algorithmic HRI to be mindful of the effects of autonomous systems on humans' actions, and further leverage these effects for better safety, efficiency, coordination, and estimation. We further use active learning techniques to update and better learn human models, and study the accuracy and robustness of these models. In the second part, we address the problem of providing correctness guarantees, while taking into account the uncertainty arising from the environment or human models. Through this effort, we introduce Probabilistic Signal Temporal Logic (PrSTL), an expressive specification language that allows representing Bayesian graphical models as part of its predicates. Further, we provide a solution for synthesizing controllers that satisfy temporal logic specifications in probabilistic and reactive settings, and discuss a diagnosis and repair algorithm for systematic transfer of control to the human in unrealizable settings. While the algorithms and techniques introduced can be applied to many human-robot systems, in this dissertation, we will mainly focus on the implications of my work for semiautonomous driving.