Synthesizing Operationally Safe Controllers for Human-in-the-Loop Human-in-the-Plant Hybrid Close Loop Systems

Human inputs are considered external disturbances in traditional certified safe controller synthesis approaches and are modeled using non-causal random variables with an assumed parameterized distribution. However, (human) safety-critical autonomous systems such as medical devices and autonomous cars operate in hybrid closed loop (HCL) mode, where humans are required to either provide control inputs, perturb the physical system being controlled (called a plant in control theory), or completely override the autonomous system (e.g. in Level 3 autonomy). Hence, the system often is subjected to causal human actions in operational deployment, that cannot be accurately modeled using non-causal distributions - leading to “flawed” safety-certified designs susceptible to operational failures in presence of unmodeled human actions (e.g. Boeing 747 Max MCAS failure). We propose a human-in-the-loop (HIL)-human-in-the-plant (HIP) approach towards synthesizing controllers for safety-critical autonomous systems where the human mind (HIL), the human body (HIP) and the real world controller (RWC) are modeled as an unified system. A three-way interaction is considered: a) through personalized inputs and biological feedback processes between HIP and HIL, b) through sensors and actuators between RWC and HIP, and c) through personalized configuration changes and data feedback between HIL and RWC. We extend the control Lyapunov theory by generating barrier function (CLBF) under human action plans, model the HIL as a combination of a Markov Chain (MC) for spontaneous events and a Fuzzy inference system (FIS) for event responses, the RWC as a black box, and integrate the HIL-HIP model with neural architectures that can learn CLBF certificates. Our main result is Theorem 1, which shows that if human actions are in the p-domain of attraction of the MC-FIS model of HIL, the synthesized controller satisfies safety properties (specified in Symbol Temporal Logic (STL)) with probability at least p. We demonstrate the capability of safe controller synthesis of our approach on two HCL applications: a) autonomous vehicle braking system, and b) automate insulin delivery for Type 1 Diabetes.