Note: This page is under construction. A complete description of this project will be available soon.
Runtime monitoring, as the name suggests, consists of building monitors that repeatedly collect data during a system’s operation in order to ensure that it is working as expected. Runtime monitoring is increasingly important part of runtime assurance, wherein we provide guarantees on the behavior of a complex cyber-physical system by monitoring its runtime behavior rather than seek to provide proofs of correctness at design time. As an aside, there is an active area of research that seeks to bridge the gap between simplifying assumptions in proofs of system properties at design time by monitoring these properties during system deployment. The key goals of a runtime monitor include:
- Active observation of a system’s execution by collecting sensor inputs, and observable events from the software systems.
- Evaluating the observations against detailed specifications, typically written in some form of temporal logic.
- Flagging potential violations as soon as possible so that mitigations (such as safely shutting down).
There has been a long history of formal verification techniques deployed during runtime in the area of runtime verification. Most runtime monitors evaluate properties on the state of the system at the current time instant. However, our goal is to predict the possible future states of the system at hand in order to check if these states will satisfy some given specifications.
Predictive runtime monitors are
Predictive Runtime Monitoring
The predictive runtime monitoring project focuses on two key aspects:
a. Predict the possible future states of the system and provide uncertainty estimates?
b. Compute the probability of a correctness property being violated?
In our project, we use Bayesian machine learning techniques that use observed data and dynamical model to compute forecasted future states of a system.
Prediction is a key aspect of predictive runtime monitoring. The goal is to rapidly forecast the future position of vehicles given a series of past observations. There are multiple approaches to prediction ranging from a extrapolation of the vehicle’s current trajectory to understanding the intent of the vehicle/agent in order to predict its future moves.
a. Our approach to extrapolation is described in detail in our Runtime Verification (RV) 2019 paper . Therein, we use an autoregressive + moving average (ARMAX) model to capture the deviation of the vehicle’s position from its current trajectory that would result if it moved on its current heading at a constant velocity. Another way of understanding this model is that it predicts the extraneous forces acting on the vehicle. This approach proves too simplistic, however since it insists on a linear model of the vehicle’s dynamics and the forces acting on it.
b. We refined this approach in our followup paper that appeared in IROS 2020 . In this paper, we use a nonlinear ``coordinated turn’’ model with disturbances. The control inputs to this model are the unknown turn rate of the vehicle and the acceleration. We use probabilistic inference for predicting the posterior distributions of the turn rate and acceleration given observations of the vehicle’s position and velocity. This approach improves upon our original ARMAX model since it is a nonlinear model.
c. In our recent work, we consider the effect of modeling the operator’s intent as a temporal logic formula . Here, we use a Bayesian inference framework that tries to predict the intent (what is the agent trying to achieve) based on their observed position. It uses a restricted class of temporal logic formulae to capture this intent along with the uncertainty in it. To facilitate this, we also need to make a ``noisy rationality’’ assumption that posits that the probability that the user takes a particular path to achieve a given intent decays exponentially as a function of the cost differential between that path and the most efficient path.
Another important aspect of our approach to predictive runtime monitoring involves rapid reachability analysis of nonlinear stochastic systems. Reachability analysis seeks to find out if a given target set of states is reachable starting from an initial set. For stochastic systems, we have external disturbances represented by probability distributions at each time step. Therefore, we ask for bounds on the probability of reaching a given target set. Key challenges for reachability analysis include:
- Our RV 2019 paper shows an approach for computing viability: a game-based reachability analysis that assumes that the system plays a game with a disturbance whose objective is to drive a system away from the desired target set of states.
- Most of the vehicle models we consider are nonlinear. However, we use invariance of these systems to the frame of reference to actually precompute reachable sets for all possible initial conditions one would see in practice .
- Our recent work has explored using polynomial expansions for stochastic systems that can compute probability bounds for nonlinear systems 
- Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVsIn International Conference on Runtime Verification (RV), Vol. 11757, pp. 349–367, 2019.
- Predictive Runtime Monitoring of Vehicle Models Using Bayesian Estimation and Reachability AnalysisIn Intl. Conference on Intelligent Robots and Systems (IROS), pp. 2111-2118, 2020.
- Predictive Runtime Monitoring for Mobile Robots using Logic-Based Bayesian Intent InferenceIn International Conference on Robotics and Automation (ICRA), pp. 8565-8571, 2021.Note: Cf. here for a video demo .
- Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial FormsIn Advances in Neural Information Processing System (NeurIPS), 2020.