Runtime Monitoring of AI-enabled Systems

How can symbolic reasoning and formal logic provide runtime insight into model behavior, performance, and anomalies under real-world variability?

To provide insight into specification satisfaction under uncertainty, we developed a logic-based monitoring framework for traffic safety that analyzes dashboard camera streams using temporal specifications. This framework detects dangerous driving behaviors and accidents beyond traditional accuracy metrics.

In smart health applications, we introduced a formal specification logic for medical image segmentation to qualitatively and quantitatively assess model outputs against anatomical and topological constraints. This approach enables structured reasoning about anatomical consistency rather than relying solely on pixel-level accuracy.

Building upon these contributions, my ongoing research aims to extend formal specifications into richer temporal domains. Specifically, I seek to monitor data-driven segmentation models over time, enabling reasoning about temporal consistency and structural integrity in continuous data streams. For example, the framework will be able to detect violations where a segment in one frame shifts significantly in the next frame, indicating instability or potential model failure. By incorporating temporal logic into segmentation and perception monitoring, this work advances reasoning about deep learning models in dynamic cyber-physical system environments, such as driving and smart health systems.

Related Publications

  • ISL: Monitoring Image Segmentation Logic in Medical Imaging Analysis
    Ziyan An, Daniel Moyer, Ipek Oguz, Taylor T. Johnson, and Meiyi Ma
    International Conference on Runtime Verification, 2025
  • Formal Logic-Guided Harnessing Heterogeneous Fairness Rules in Smart Cities
    Ziyan An, Yiqi Zhao, Xuqing Gao, Ayan Mukhopadhyay, and Meiyi Ma
    ACM Transactions on Cyber-Physical Systems, 2025
  • Runtime Monitoring of Accidents in Driving Recordings with Multi-Type Logic in Empirical Models
    Ziyan An, Xia Wang, Taylor T. Johnson, Jonathan Sprinkle, and Meiyi Ma
    International Conference on Runtime Verification, 2023
Runtime accident monitoring pipeline
Figure 1: The runtime monitoring pipeline processes dashboard camera streams and evaluates them against multi-type logic specifications (FOL, HOL, STL) to detect dangerous driving behaviors and accidents on the fly.
Image Segmentation Logic (ISL) monitoring overview
Figure 2: Image Segmentation Logic (ISL) augments a U-Net segmentation model's outputs into a structured representation, then monitors them against pixel- and region-level logic formulas that encode anatomical and topological constraints.