Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantitative Predictive Monitoring and Control for Safe Human-Machine Interaction

Shuyang Dong, Meiyi Ma, Josephine Lamp, Sebastian Elbaum, Matthew B. Dwyer, Lu Feng

TL;DR

This work tackles safe human–machine interaction under uncertainty by combining Bayesian sequential predictions with a new STL-U quantitative monitor that yields robustness degree intervals indicating how far predicted trajectories satisfy safety requirements. It introduces a loss L_qt to calibrate uncertainty estimates by selecting optimal stochastic regularization and dropout, and an adaptive controller that adjusts actions based on STL-U robustness, yielding safer, more effective closed-loop performance. Demonstrations in Type 1 Diabetes management and semi-autonomous driving show earlier hazard detection, higher validation accuracy for safety satisfaction, and improved time-in-range with reduced safety hazards. The approach provides a general, formal framework for runtime predictive monitoring and control under uncertainty, with potential impact across healthcare, transportation, and other safety-critical HMI domains.

Abstract

There is a growing trend toward AI systems interacting with humans to revolutionize a range of application domains such as healthcare and transportation. However, unsafe human-machine interaction can lead to catastrophic failures. We propose a novel approach that predicts future states by accounting for the uncertainty of human interaction, monitors whether predictions satisfy or violate safety requirements, and adapts control actions based on the predictive monitoring results. Specifically, we develop a new quantitative predictive monitor based on Signal Temporal Logic with Uncertainty (STL-U) to compute a robustness degree interval, which indicates the extent to which a sequence of uncertain predictions satisfies or violates an STL-U requirement. We also develop a new loss function to guide the uncertainty calibration of Bayesian deep learning and a new adaptive control method, both of which leverage STL-U quantitative predictive monitoring results. We apply the proposed approach to two case studies: Type 1 Diabetes management and semi-autonomous driving. Experiments show that the proposed approach improves safety and effectiveness in both case studies.

Quantitative Predictive Monitoring and Control for Safe Human-Machine Interaction

TL;DR

This work tackles safe human–machine interaction under uncertainty by combining Bayesian sequential predictions with a new STL-U quantitative monitor that yields robustness degree intervals indicating how far predicted trajectories satisfy safety requirements. It introduces a loss L_qt to calibrate uncertainty estimates by selecting optimal stochastic regularization and dropout, and an adaptive controller that adjusts actions based on STL-U robustness, yielding safer, more effective closed-loop performance. Demonstrations in Type 1 Diabetes management and semi-autonomous driving show earlier hazard detection, higher validation accuracy for safety satisfaction, and improved time-in-range with reduced safety hazards. The approach provides a general, formal framework for runtime predictive monitoring and control under uncertainty, with potential impact across healthcare, transportation, and other safety-critical HMI domains.

Abstract

There is a growing trend toward AI systems interacting with humans to revolutionize a range of application domains such as healthcare and transportation. However, unsafe human-machine interaction can lead to catastrophic failures. We propose a novel approach that predicts future states by accounting for the uncertainty of human interaction, monitors whether predictions satisfy or violate safety requirements, and adapts control actions based on the predictive monitoring results. Specifically, we develop a new quantitative predictive monitor based on Signal Temporal Logic with Uncertainty (STL-U) to compute a robustness degree interval, which indicates the extent to which a sequence of uncertain predictions satisfies or violates an STL-U requirement. We also develop a new loss function to guide the uncertainty calibration of Bayesian deep learning and a new adaptive control method, both of which leverage STL-U quantitative predictive monitoring results. We apply the proposed approach to two case studies: Type 1 Diabetes management and semi-autonomous driving. Experiments show that the proposed approach improves safety and effectiveness in both case studies.

Paper Structure

This paper contains 22 sections, 2 theorems, 5 equations, 5 figures, 5 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Uncertain Sequential Prediction
  4. Signal Temporal Logic with Uncertainty
  5. Approach
  6. STL-U Quantitative Monitor
  7. Uncertainty Calibration
  8. Adaptive Controller
  9. Experiments
  10. Datasets and experimental setup.
  11. RQ1: Evaluation of Uncertainty Calibration
  12. RQ2: Evaluation of Predictive Monitors
  13. RQ3: Closed-Loop Simulation
  14. Related Work
  15. Safe human-machine interaction via formal methods.
  16. ...and 7 more sections

Key Result

Theorem 3.1

Given an STL-U formula $\varphi$ and a flowpipe $\omega$, the following properties hold. where $\underline{\rho}$ and $\overline{\rho}$ are the lower and upper bounds of the robustness degree interval $\rho(\varphi, \omega, t)$, and $\models_s$ (resp.$\models_w$) denotes the strong (resp. weak) satisfaction relations.

Figures (5)

  • Figure 1: Proposed approach applied to T1D management.
  • Figure 2: An example flowpipe of predicted BG levels under a confidence level $\varepsilon$.
  • Figure 3: Adapting control actions based on STL-U quantitative monitoring results.
  • Figure 4: Loss values of using different SRTs and dropout rates in the Bayesian LSTM model for adults.
  • Figure 5: Comparing the number of hazards that occurred during the simulated 7-day period (mean and standard deviation over each patient population).

Theorems & Definitions (3)

  • Definition 1: STL-U quantitative semantics
  • Theorem 3.1
  • Theorem A.1