# Analyzing Disease Spread Models using a Theorem Prover

**DISCLAIMER**: This post is a

**pedagogical**tutorial on theorem proving for hybrid-time dynamical systems and is

**not**intended as a serious analysis of any actual disease.

During panedmics, public health professionals often suggest “social
distancing”.
The goal of social distancing is to slow down the spread of the
disease so that public health infrastructure is not overloaded.
Unfortunately, social distancing often incures a significant social and
economic cost.
Businesses must close, and people are isolated from their friends
and family.
This leads us to an interesting question: **how much social distancing is
enough?**

Answering that question in the context of a real pandemic requires an enormous amoung of effort. In this note, we’ll consider a very simple toy model of a pandemic and use a theorem prover to derive the minimum amount of social distancing necessary to avoid hospital overload.

## SIR Models

A Susceptible-Infected-Recovered model is a simplified dynamical system model of disease spread. The basic model is a set of three ordinary differential equations:

```
s' = -b*s*i,
r' = -k*i,
i' = b*s*i - k*i
```

where:

`s`

is the number of individuals in the population who are susceptible to the infection,`r`

is the number of individuals in the population who are recovered (we make the assumpption that once an individual is recovered they will not get the disease again; this assumption obviously doesn’t always hold), and`i`

is the number of currently infected individuals.

In addition to these variables, the system also has two parameters:

`b`

is the number of contacts individuals make each day, and`k`

is the recover rate (the number of individuals who change from infected (`i`

) to recovered (`r`

) each day.

Our goal is to allow as much contact between inviduals as possible
while keeping the infected rate (`i`

) below hospital’s capacity (`capacity`

).
In terms of the model, we would like to know: **how large we can let b get
before i goes above capcity?**

This is a *reachability property* of the SIR model: we would like to know,
given some initial conditions on `s`

, `i`

, and `r`

, whether the flow of
the SIR differential equations will reach point where `i < hospitalCapcity`

.
The KeYmaera X theorem prover was designed to explore exactly these types
of reachability properties.

## A Quick Introduction to Differential Dynamic Logic and KeYmaera X

In this note, we will use KeYmaera X to discover values of `b`

that keep the value of `i`

below `hospitalCapcity`

.
KeYmaera X is a theorem prover for differential dynamic logic.
This logic allows you to state and prove reachability
properties of differential equations by writing formulas such as:

```
init -> [{ODEs}]property
```

where,

`init`

is a formula of first order logic over real-valued variables (e.g.,`x>0 & y>0`

),`ODEs`

is a system of differential equations,`property`

is also a formula of first order logic over real-valued variables (e.g.,`i < capacity`

),

and the meaning of the formula `init -> [{ODEs}]property`

is:
*starting from a set described by the formula init, any
flow of the different equaltions ODEs will stay within the set described by
property*.

For example, we can state properties such as:
`x>0 & y>0 -> [{x'=y}]x>0`

; i.e., if `x`

starts positive and has a positive
derivative then the value of `x`

will remain positive throughout the flow of
the equation `x'=y`

.

## Finding a Safe Contact Rate using KeYmaera X

Here’s a simple SIR model written in KeYmaera X’s input language:

```
ProgramVariables
R s, r, i, s_0, r_0, i_0, b, k, capacity;
End.
Problem
(
i < capacity &
s=s_0 &
r=r_0 &
i=i_0 &
0 < k & k < 1
)
->
[
{
s' = -b*s*i,
r' = k*i,
i' = b*s*i-k*i
}
](i<capacity)
End.
```

Notice that this formula is not true! For example, if:

```
s_0 = 1,000,000
r_0 = 0
i_0 = 999
capacity = 1000
```

then obviously `i`

will quickly exceed `capcity`

.
However, we can use KeYmaera X to derive necessary and sufficient conditions
on the choice of `b`

in terms of any concrete choice of `s_0`

, `r_0`

, and
`i_0`

.

## Conclusion

Theorem provers are useful for more than just checking the truth of things we already know. They can also help us understand the world.