COVID Infection Prediction using CPS Formal Verification Methods

Formal verification of cyber-physical systems (CPS) requires reasoning methods for not just software, but also analyzing how the physical side of the system will behave. As the laws of nature are written in differential equations, CPS formal verification researchers have inevitably needed to create analysis methods that can analyze systems with differential equations. For example, the behavior of an autonomous race car or an F-16 aircraft is more readily and accurately described in terms of how continuous variables such as the speed and position change over time.

In time-bounded reachability analysis—one formal analysis technique for CPS—given a set of initial states and uncertainty on external inputs and disturbances, the method computes what future states the system can enter while obeying the differential equations. These states are then checked to see if they all meet a formal specification. 

Beyond traditional CPS applications, the generality of this setup allows us to analyze many other classes of systems. My SIGBED Blog post last year showed one such domain, verification of neural networks, where reachability methods were used to formally prove properties over complex network structures. Another potential application area, especially relevant over the last year, is the possibility to predict how COVID propagates through a population. 

Disease propagation can be modeled using differential equations of various complexity. The COVID supermodel is one recent modeling approach that captures the effects of asymptotic patients, various degrees of lockdown, as well as herd immunity. One difficulty of using such models is parameter selection, which in our case involves determining things like the probability of infection, removal rate, and mortality rate. Although estimates can be obtained from data, small changes in parameters can have an outsized impact on the resulting predictions. As the COVID supermodel uses a seven-dimensional nonlinear differential equation, analyzing the extreme points may not capture the worst-case scenarios. When models are complex with uncertain parameters, sampling the parameter space and running lots of simulations may not adequately capture the space of possibilities.

With reachability methods, we can analyze all possible behaviors under a set of uncertainty. A plot of the set propagation of confirmed COVID cases in India, along with the real-world case measurement for three different date ranges is shown below.

While the predicted set of possibilities (blue) contains the real-world case count (red), we are able to see how much small changes in infection parameters could affect case count. Parameter estimation is still a difficult problem, as the model requires adjusting parameters over time, due to new COVID variants with different infection rates spreading through a population. Accurate prediction beyond a few weeks is probably infeasible with these models, unless changes in parameters can be accurately estimated. Further, actual infection rates are unknown if people do not get tested, adding uncertainty to the result validation. Nonetheless, such analysis could be useful for decision making, where policy decisions can affect some of the parameters, such as the degree of lockdown affecting probability of infection. 

The reachability method used for the plots has a parallelotope bundle set representation with automatic and dynamic parallelotope direction selection, in order to soundly predict possible ranges of infection rates over time. The parameters and details of the reachability method are available in an online report.

Author bio: Stanley Bak (@StanleyBak) is an assistant professor at Stony Brook University in the Department of Computer Science investigating formal methods for CPS. Parasara Sridhar Duggirala (@psduggirala) is an assistant professor and Edward Kim is a graduate student at the University of North Carolina at Chapel Hill in the Department of Computer Science investigating CPS and formal methods.

Disclaimer: Any views or opinions represented in this blog are personal, belong solely to the blog post authors and do not represent those of ACM SIGBED or its parent organization, ACM.