Project: NSF CAREER: Formal Methods for Human-Cyber-Physical Systems

Sponsor: This project is supported by National Science Foundation CCF-1942836 (June 2020 - present).

Objective

There is a growing trend toward human-cyber-physical systems (h-CPS), where systems collaborate or interact with human operators to harness complementary strengths of humans and autonomy. Examples include self- driving cars that need the occasional driver intervention, artificial pancreas systems that require patients to approve insulin boluses for meals, and industrial robots that work beside or cooperatively with people. The societal impact of h-CPS, however, is contingent on ensuring safety and reliability. Several high-profile incidents have shown that unsafe h-CPS can lead to catastrophic outcomes. Formal methods enable the model-based design of safety-critical systems with mathematically rigorous guarantees. While tremendous progress has been made in advancing formal methods for CPS, the research area of formal methods for h-CPS is still in its infancy. Human operators are not just part of the system’s environment, but agents with intentions, beliefs, and actions that mesh with the system autonomy. Therefore, formal methods for h-CPS need to take into account not only system models of CPS, but also the uncertainty due to human interactions. The proposed project targets this major gap to expand formal methods toward the joint modeling and formal analysis of CPS and human-autonomy interactions. Its objective is to develop theory, methods, and tools for the formal specification, verification and synthesis of h-CPS that account for the uncertainty and variability of human behaviors, intentions, and preferences.

Intellectual Merit

The proposed work has three research thrusts. Thrust I develops formal models and specifications for h-CPS, which is a first step in the model-based design of h-CPS. The key innovation includes new methods to build probabilistic models that can represent unobservable human cognitive states estimated from multi-modal sensing data, and to learn probabilistic specifications for h-CPS. Thrust II develops probabilistic verification and synthesis techniques to provide correctness guarantees for h-CPS, based on probabilistic models and specifications obtained in Thrust I. The key innovation includes new methods for compositional verification and synthesis of partially observable probabilistic models with respect to a rich set of specifications, new methods to verify parametric h-CPS models whose transition probabilities are specified as intervals or variables instead of point estimates (e.g., to capture learning inaccuracies), and new methods to generate explainable verification and synthesis results to help humans understand counterexamples and control strategies. Thrust III develops an evaluation plan for the proposed formal methods. The key innovation includes prototype tool implementation that expands PRISM and PRISM-games to support the proposed new formal methods for h-CPS, and human subjects studies to collect data for modeling and evaluation purposes.

Broader Impacts

The results of this project will improve the safety and user satisfaction of semi-autonomous driving, reduce the burden on drivers, and cut development costs. The proposed formal methods will enable the model-based design of a wide range of h-CPS applications (e.g., collaborative robots, assistive medical devices). The research outcomes of this project are integrated into the graduate course, and provide research and training opportunities for undergraduate and graduate students at the University of Virginia, with a particular focus on supporting underrepresented minorities and women students.

Research Progress & Publications

• Towards Transparent Robotic Planning via Contrastive Explanations [PDF] [DOI]
  Shenghui Chen, Kayla Boggess, and Lu Feng.
  IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2020
  

• STLnet: Signal Temporal Logic Enforced Multivariate Recurrent Neural Networks [PDF]
  Meiyi Ma, Ji Gao, Lu Feng, and John Stankovic.
  Thirty-fourth Conference on Neural Information Processing Systems (NeurlPS), 2020
  

• DeepTake: Prediction of Driver Takeover Behavior using Multimodal Data [PDF] [DOI]
  Erfan Pakdamanian, Shili Sheng, Sonia Baee, Seongkook Heo, Sarit Kraus, and Lu Feng.
  ACM Conference on Human Factors in Computing Systems (CHI), 2021
  

• Trust-Based Route Planning for Autonomous Driving [PDF] [DOI]
  Shili Sheng, Erfan Pakdamanian, Kyungtae Han, BaekGyu Kim, John Lenneman, Ziran Wang, and Lu Feng.
  ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 2021
  

• A Smart City Simulation Platform with Uncertainty [DOI]
  Shuyang Dong, Meiyi Ma, and Lu Feng.
  ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 2021
  

• A Novel Spatial-Temporal Specification-Based Monitoring System for Smart Cities [PDF] [DOI]
  Meiyi Ma, Ezio Bartocci, Eli Lifland, John Stankovic, and Lu Feng.
  IEEE Internet of Things Journal, 2021
  

• Towards Formal Methods for Smart Cities [DOI]
  Meiyi Ma, John Stankovic, and Lu Feng.
  IEEE Computer, 2021
  

• Predictive Monitoring with Logic-Calibrated Uncertainty for Cyber-Physical Systems [PDF] [DOI]
  Meiyi Ma, John Stankovic, Ezio Bartocci, and Lu Feng.
  ACM SIGBED International Conference on Embedded Software (EMSOFT), 2021
  

• MEDIRL: Predicting the Visual Attention of Drivers via Maximum Entropy Deep Inverse Reinforcement Learning [PDF]
  Sonia Baee, Erfan Pakdamanian, Inki Kim, Lu Feng, Vicente Ordonez, and Laura Barnes.
  IEEE/CVF International Conference on Computer Vision (ICCV), 2021
  

• Multi-Objective Controller Synthesis with Uncertain Human Preferences [PDF]
  Shenghui Chen, Kayla Boggess, David Parker, and Lu Feng.
  ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 2022
  

• Toward Policy Explanations for Multi-Agent Reinforcement Learning [PDF]
  Kayla Boggess, Sarit Kraus, and Lu Feng.
  International Joint Conference on Artificial Intelligence (IJCAI), 2022