---
abstract: 'Ever since the outbreak of the COVID-19 epidemic, various public health control strategies have been proposed and tested against SARS-CoV-2. In this paper, we study three specific COVID-19 epidemic control models: the susceptible, exposed, infectious, recovered (SEIR) model with vaccination control, the SEIR model with shield immunity control, and the susceptible, un-quarantined infected, quarantined infected, confirmed infected (SUQC) model with quarantine control. We express the control requirement in *metric temporal logic* (MTL) formulas and develop methods for synthesizing control inputs based on three specific COVID-19 epidemic models with MTL specifications. To the best of our knowledge, this is the first paper to provide automatically-synthesized and fine-tuned control synthesis for the COVID-19 epidemic models with formal specifications. We provide simulation results in three different case studies: vaccination control for the COVID-19 epidemic with model parameters estimated from data in Lombardy, Italy; shield immunity control for the COVID-19 epidemic with model parameters estimated from data in Lombardy, Italy; and quarantine control for the COVID-19 epidemic with model parameters estimated from data in Wuhan, China. The results show that the proposed synthesis approach can generate control inputs within a relatively short time (within 5 seconds) such that the time-varying numbers of individuals in each category (e.g., infectious, immune) satisfy the MTL specifications. The results are also consistent with the claim that control in the early phases of COVID-19 is the most effective in the mitigation.'
author:
- 'Zhe Xu[^1],  Bo Wu and Ufuk Topcu'
bibliography:
- 'ref.bib'
title: 'Control Strategies for COVID-19 Epidemic with Vaccination, Shield Immunity and Quarantine: A Metric Temporal Logic Approach'
---

Introduction
============

The COVID-19 pandemic [@Fauci2020] has caused over 15 million confirmed cases and over 0.6 million deaths globally as of July 23, 2020. Ever since the outbreak of COVID-19, various public health control strategies have been produced and tested against SARS-CoV-2 [@Stewart_magazine_2020].

Currently, over 90 vaccines are being developed against SARS-CoV-2 by research teams across the world [@vaccines_nature2020]. Besides vaccination, other strategies have also been proposed to control the spread of SARS-CoV-2. In [@Weitz_nature], the authors proposed *shielding immunity* to protect the susceptible people from getting infected with SARS-CoV-2. Specifically, shielding immunity works by first identifying and deploying recovered individuals who have protective antibodies to SARS-CoV-2, and then increasing the proportion of interactions with recovered individuals as opposed to other individuals. In [@Zhao2020], the authors analyzed how quarantine has mitigated the spread of SARS-CoV-2 based on a model that differentiates quarantined infected individuals and un-quarantined infected individuals.

Despite the fact that various promising control strategies have been proposed against SARS-CoV-2, such control strategies still suffer from several limitations. (a) The control strategies SARS-CoV-2 often treat the control inputs (e.g., the shield strength in shield immunity, the quarantine rate in quarantine control) as parameters which stay constant during one stage of time, while in reality such inputs could be changed on a daily basis for more fine-tuned control. (b) The control inputs in the literature are often tuned manually through trial-and-error, instead of being synthesized automatically. (c) There is a lack of specific and formal specifications for the expected effects and outcomes of the control strategies.

To address these limitations, we propose an automatically-synthesized fine-tuned control synthesis approach for three control strategies in mitigating SARS-CoV-2. We use *metric temporal logic* (MTL) formulas to specify the expected outcomes such as “the deaths from the infection should always not exceed one thousand per day within the next three months” or “the people immune from the disease should eventually exceed 200 thousand within the next 100 to 120 days”. Such temporal logic formulas have been used as high-level knowledge or specifications in many applications in artificial intelligence [@zhe_ijcai2019], robotic control [@Verginis2019Icra], power systems [@zhe_control], etc.

The proposed control synthesis approach is based on three specific COVID-19 epidemic mitigation models: the susceptible, exposed, infectious, recovered (SEIR) model with vaccination control, the SEIR model with shield immunity control, and the susceptible, un-quarantined infected, quarantined infected, confirmed infected (SUQC) model with quarantine control. We express the mitigation requirement in metric temporal logic formulas and develop methods for synthesizing controls based on the three specific COVID-19 epidemic models. Specifically, we convert the synthesis problem into mixed-integer bi-linear programming or mixed-integer fractional constrained programming problems, and solve the optimization problems using highly efficient solvers [@beal2018gekko].

We provide simulation results in three different case studies: vaccination control for COVID-19 epidemic with model parameters estimated from data in Lombardy, Italy; shield immunity control for COVID-19 epidemic with model parameters estimated from data in Lombardy, Italy; and quarantine control for COVID-19 epidemic with model parameters estimated from data in Wuhan, China. The proposed synthesis approach can generate control inputs within a relatively short time (within 5 seconds) such that the system behaviors satisfy the MTL specifications. The results also show that more control efforts are needed for more stringent requirements expressed in MTL specifications, and control in early phases of COVID-19 spread can generally mitigate the effects more efficiently.

Related Work
============

**COVID-19 epidemic modeling and control strategies**: Ever since the outbreak of COVID-19, there has been numerous research focusing on the modeling of COVID-19 epidemic based on data collected from both the epicenters and other places [@Bertozzi_Franco2020]. Among the various models, *compartmental models* such as SEIR and SUQC models have been used frequently for the analysis of COVID-19. There has also been work in analyzing or predicting COVID-19 using artificial intelligence models [@Zheng_AI2020], stochastic intensity models [@Chen2002], etc. The models we use in this paper are based on the SEIR (both the standard and with shield immunity) and SUQC models, but we have replaced some essential parameters (e.g., the shield strength in shield immunity, the quarantine rate in quarantine control) with control inputs which can be synthesized to vary on a daily basis.

**Optimal control of epidemic models**: There is a rich literature in designing vaccination control for the SEIR or SIR models of epidemics. However, such methods have not been applied in the setting of COVID-19 mitigation. Besides, there has been no work in optimal control of epidemic models with formal specifications (e.g., expressed in temporal logic formulas).

**Control synthesis with temporal logic specifications**: There are three main categories of approaches to design controllers that meet temporal logic specifications [@KHFP; @RVFK2012; @KKW2002; @MH2019IFAC; @STJC2010; @UASX2011; @liu2017distributed; @Djeumou2020; @liu2017communication; @liu2020distributed; @cubuktepe2020policy]. The first category of approaches abstract the system as a transition system and transform the controller syntheses problem into a series of constrained reachability problems [@Topcu; @Dimarogonas; @Coogan]. The second category of approaches mainly focus on linear dynamics and it converts the control synthesis problem into a mixed-integer linear programming (MILP) problem [@BluSTL; @sayan2016; @Allerton2019; @zheACC2019DF; @zhe_advisory; @zheACC2018wind] and the controller then consists in a pre-compiled MILP which can be solved efficiently by MILP solvers. The third category of approaches substitute the temporal logic constraint into the optimization problem and apply a functional gradient descent algorithm on the resulting unconstrained problem [@Andygradient; @Abbas2014; @zhe_control; @zheACCstorageControl]. The control synthesis approach in this paper is based on the second category of approaches, but we have extended the method to non-linear dynamics to fit the epidemic models for COVID-19.

Metric Temporal Logic (MTL) {#sec_MTL}
===========================

In this section, we briefly review metric temporal logic (MTL) [@FainekosMTL] interpreted over discrete-time trajectories. The state $x$ (e.g., representing the susceptible, exposed, infectious, recovered population of a certain region) belongs to the domain $\mathcal{X}\subset\mathbb{R}^n$. The time set is $\mathbb{T} = \mathbb{R}_{\ge0}$. The domain $\mathbb{B} = \{\textrm{True}, \textrm{False}\}$ is the Boolean domain, and the time index set is $\mathbb{I} = \{0,1,\dots\}$. We use $t[k]\in\mathbb{T}$ to denote the time instant at time index $k\in\mathbb{I}$ and $x[k]\triangleq x(t[k])$ to denote the value of $x$ at time $t[k]$. With slight abuse of notation, we use $\xi$ to denote a trajectory as a function from $\mathbb{T}$ to $\mathcal{X}$. A set $AP$ is a set of atomic propositions, each mapping $\mathcal{X}$ to $\mathbb{B}$. The syntax of MTL is defined recursively as follows: $$\varphi:=\top\mid \pi\mid\lnot\varphi\mid\varphi_{1}\wedge\varphi_{2}\mid\varphi_{1}\vee
\varphi_{2}\mid\varphi_{1}\mathcal{U}_{\mathcal{I}}\varphi_{2},$$ where $\top$ stands for the Boolean constant True, $\pi\in AP$ is an atomic proposition, $\lnot$ (negation), $\wedge$ (conjunction), $\vee$ (disjunction) are standard Boolean connectives, $\mathcal{U}$ is a temporal operator representing until, $\mathcal{I}$ is a time index interval of the form $\mathcal{I}=[i_{1},i_{2}]$ ($i_1\le i_2$, $i_1, i_2\in\mathbb{I}$). We can also derive two useful temporal operators from until ($\mathcal{U}$), which are eventually $\Diamond_{\mathcal{I}}\varphi=\top\mathcal{U}_{\mathcal{I}}\varphi$ and always $\Box_{\mathcal{I}}\varphi=\lnot\Diamond_{\mathcal{I}}\lnot\varphi$. For example, the MTL formula $\Box_{[0,100]} (DeathsPerDay\le 0.001)\wedge\Diamond_{[40, 60]}(Recovered\ge6)$ means “the deaths from infection should never exceed 0.001 million (one thousand) per day within the next 100 days, and the immune population should eventually exceed 6 million after 40 to 60 days” (we assume that the unit is million in this paper unless otherwise indicated).

We define the set of states that satisfy the atomic proposition $\pi$ as $\mathcal{O}(\pi)\subset \mathcal{X}$. We denote the distance from $x$ to a set $D\subseteq\mathcal{X}$ as **dist**$_d(x,D)\triangleq$inf$\{d(x, x')\mid x'\in cl(D)\}$, where $d$ is a metric on $\mathcal{X}$ and $cl(D)$ denotes the closure of the set $D$. In this paper, we use the metric $d(x,x')={\left\lVertx-x'\right\rVert}$, where $\left\Vert\cdot\right\Vert $ denotes the 2-norm. We denote the depth of $x$ in $D$ as **depth**$_d(x,D)\triangleq$ **dist**$_d(x,\mathcal{X}\setminus D)$. We define the signed distance from $x$ to $D$ as $\textbf{Dist}_d(x,D)\triangleq-\textbf{dist}_d(x,D)$, if $x$ $\not\in D$; and $\textbf{Dist}_d(x,D)\triangleq\textbf{depth}_d(x,D)$, if $x$ $\in D$. The Boolean semantics of MTL can be found in [@FAINEKOScontinous], with the slight variation that we only evaluate the satisfaction of a trajectory with respect to an MTL formula at discrete-time instants $t[k]~(k\in\mathcal{I})$. The robustness degree of a trajectory $\xi$ with respect to an MTL formula $\varphi$ at time index $k$, denoted as $\left[\left[\varphi\right]\right](\xi, k)$, is defined recursively as follows: $$\begin{split}
\left[\left[\top\right]\right](\xi, k) :=& +\infty,\\
\left[\left[ \pi\right]\right](\xi, k)  :=&\textbf{Dist$_d(x[k],\mathcal{O}(\pi))$},\\
\left[\left[ \neg\varphi\right]\right](\xi, k)  :=&-\left[\left[ \varphi\right]\right](\xi, k),\\
\left[\left[\varphi_1\vee\varphi_2\right]\right](\xi, k)  :=&\max\big(\left[\left[ \varphi_1\right]\right](\xi, k),\left[\left[ \varphi_2\right]\right](\xi, k)\big),\\
\left[\left[\varphi_1\mathcal{U}_{\mathcal{I}}\varphi_{2}\right]\right](\xi, k)  :=&\max_{k'\in (k+\mathcal{I})}\Big(\min\big(\left[\left[ \varphi_2\right]\right](\xi, k'),\\& \min_{k\leq k''<k'}\left[\left[\varphi_1\right]\right]
(\xi,k'')\big)\Big).  
\end{split}$$ As defined, $\left[\left[\varphi\right]\right](\xi, k)\ge0$ if $\xi$ satisfies $\varphi$ at time index $k$.

COVID-19 Models with Control Strategies {#sec_models}
=======================================

In this section, we study three models for COVID-19 epidemic [@Carcione_model; @Weitz_nature; @Zhao2020] and introduce the corresponding models with vaccination control, shield immunity control and quarantine control.

COVID-19 SEIR Model with Vaccination Control
--------------------------------------------

The susceptible, exposed, infectious, recovered (SEIR) model has been frequently used in epidemic analyses. As shown in Figure \[diagram1\], the total population is divided into five parts:

-   The susceptible population $S$: everyone is susceptible to the disease by birth since immunity is not hereditary;

-   The exposed population $E$: the individuals who have been exposed to the disease, but are still not infectious;

-   The infectious population $I$: the individuals who are infectious;

-   The immune (recovered) population $R$: the individuals who are vaccinated or recovered from the disease, i.e., the population who are immune to the disease;

-   The dead population $D$: the dead individuals from the disease.

For simplicity, we assume that the birth rate and the natural death rate are the same for the population we are investigating.

We consider an SEIR epidemic disease model [@Carcione_model; @Elie2020] with vaccination control [@Alonso2012] as follows. $$\begin{aligned}
\begin{cases}
\dot{I} = \epsilon E - (\gamma+\mu+\alpha)I;\\
\dot{E} = \beta SI/N - (\mu+\epsilon)E;\\
\dot{S} = \lambda N - \mu S - \beta SI/N - V;\\
\dot{R} = \gamma I - \mu R + V;\\
\dot{D} = - \dot{I}-\dot{E}-\dot{S}-\dot{R},
\end{cases}            
\label{vaccination_model}\end{aligned}$$ where the control input $V$ is the number of vaccinated individuals per day, $N = S + E + I + R\le N_0$ is the total population in the region ($N_0$ is the initial total population in the region), $S$, $E$, $I$, $R$ and $D$ are the number of susceptible, exposed, infectious and recovered population in the region, respectively, and $D$ is the number of deaths from SARS-CoV-2 in the region. For the parameters, $\lambda$ denotes the per-capita birth rate, $\mu$ is the per-capita natural death rate (death rate from causes unrelated to SARS-CoV-2), $\alpha$ is the SARS-CoV-2 virus-induced average fatality rate, $\beta$ is the probability of disease transmission per contact (dimensionless) times the number of contacts per unit time, $\epsilon$ is the rate of progression from exposed to infectious (the reciprocal is the incubation period), and $\gamma$ is the recovery rate of infectious individuals (the reciprocal is the infectious period).

Note that this model is slightly different from the model in [@Alonso2012] as we use $V$ as a separate term instead of $VS$. We found it more convenient for computational purposes in the optimization problems for control synthesis in later sections.

![Block diagram of the COVID-19 SEIR model with vaccination control.[]{data-label="diagram1"}](diagram_covid.pdf)

COVID-19 SEIR Model with Shield Immunity
----------------------------------------

*Shield immunity* is a strategy recently proposed in [@Weitz_nature] to limit the transmission of the disease. The basic idea of this strategy is to increase the proportion of interactions with recovered individuals as opposed to the other individuals in the population. The effectiveness of this strategy is based on the assumption that recovered individuals (virus-negative and antibody-positive) can safely interact with both susceptible and infectious individuals without getting infected with the disease. See Figure \[diagram2\] as an illustration.

As the model used in [@Weitz_nature] is modified from a SIR model, we consider a corresponding SEIR model with shield immunity and we use the shield strength as control inputs. Specifically, we consider the following model: $$\begin{aligned}
\begin{cases}
\dot{I} = \epsilon E - (\gamma+\mu+\alpha)I ;\\
\dot{E} = \beta SI/(N+\chi R) - (\mu+\epsilon)E;\\
\dot{S} = \lambda N - \mu S - \beta SI/(N+\chi R);\\
\dot{R} = \gamma I - \mu R + V;\\
\dot{D} = - \dot{I}-\dot{E}-\dot{S}-\dot{R},
\end{cases}                 \end{aligned}$$ where the states and parameters are the same as in (\[vaccination\_model\]), while $\chi(\cdot)$ is the shielding strength as time-varying input to be synthesized for the recovered population to substitute the contact for the susceptible population.

![Block diagram of the COVID-19 SEIR model with shield immunity control.[]{data-label="diagram2"}](diagram_covid_shield.pdf)

COVID-19 SUQC model with quarantine control
-------------------------------------------

The susceptible, un-quarantined infected, quarantined infected, confirmed infected (SUQC) model was recently proposed in [@Zhao2020] based on the COVID-19 data in Wuhan, China. As shown in Figure \[diagram3\], we consider four subgroups in the population:

-   The susceptible population $S$: everyone is susceptible to the disease by birth since immunity is not hereditary;

-   The un-quarantined infected population $U$: the individuals who are infected and un-quarantined, and they can be either asymptomatic or symptomatic;

-   The quarantined infected population $Q$: the individuals who are infectious and quarantined (the un-quarantined infected become quarantined infected by isolation or hospitalization, and the quarantined infected lose the ability of infecting the susceptible individuals);

-   The confirmed infected population $C$: the individuals who are confirmed to be infected with the disease (i.e., the positive cases).

We consider the SUQC model with quarantine control as follows. $$\begin{aligned}
\begin{cases}
\dot{S} = - \beta_0 US/N;\\
\dot{U} = \beta_0 US/N - q U;\\
\dot{Q} = q U - [\gamma_2 + (1-\gamma_2)\sigma]Q;\\
\dot{C} = [\gamma_2 + (1-\gamma_2)\sigma]Q,
\end{cases}                 \end{aligned}$$ where $q$ is the quarantine rate (for an un-quarantined infected to be quarantined) as control input to be synthesized, $\beta_0$ is the infection rate (i.e., the mean number of new infected caused by an un-quarantined infected per day), $\gamma_2$ is the confirmation rate of $Q$ (i.e., the probability that the quarantined infected are identified to be confirmed cases through conventional methods such as laboratory diagnosis), $\sigma$ is the subsequent confirmation rate of those infected that are not confirmed by the conventional methods, but confirmed with some additional tests.

![Block diagram of the COVID-19 SUQC model with quarantine control.[]{data-label="diagram3"}](diagram_covid_SUQC.pdf)

Control Synthesis of COVID-19 epidemic with Metric Temporal Logic Specifications
================================================================================

In this section, we present the control synthesis methods for the three COVID-19 epidemic models in Section \[sec\_models\] with vaccination control, shield immunity control and quarantine control, respectively.\
**Vaccination control**: For the COVID-19 SEIR model with vaccination control, we discretize the model in (\[vaccination\_model\]) as follows. $$\begin{aligned}
\begin{cases}
I[k+1] = I[k] + T_{\textrm{s}}\epsilon E[k] - T_{\textrm{s}}(\gamma+\mu+\alpha)I[k];\\
E[k+1] = E[k] + T_{\textrm{s}}\beta S[k]I[k]/N[k] - T_{\textrm{s}}(\mu+\epsilon)E[k];\\
S[k+1] = S[k] + T_{\textrm{s}}\lambda N[k] - T_{\textrm{s}}\mu S[k] - T_{\textrm{s}}\beta S[k]I[k]/N[k] - T_{\textrm{s}}V[k];\\
R[k+1] = R[k] + T_{\textrm{s}}\gamma I[k] - T_{\textrm{s}}\mu R[k] + T_{\textrm{s}}V[k];\\
D[k+1] = D[k] - T_{\textrm{s}}\dot{I}[k]-T_{\textrm{s}}\dot{E}[k]-T_{\textrm{s}}\dot{S}[k]-T_{\textrm{s}}\dot{R}[k],
\end{cases}     
\label{discrete_vaccination_model}\end{aligned}$$ where $T_{\textrm{s}}$ is the sampling period. We also use $\Delta D[k]=D[k+1]-D[k]$ to denote the number of deaths from the infection at day $k$.

Following the notations in Section \[sec\_MTL\], we use $x_{\textrm{V}}=[I, E, S, R, D]$ to denote the state of (\[discrete\_vaccination\_model\]) and $\xi_{\bm\cdot;x^{init}_{\textrm{V}},V}$ to denote the trajectory of (\[discrete\_vaccination\_model\]) starting from $x^{init}_{\textrm{V}}=[I[1], E[1], S[1], R[1], D[1]]$ and vaccination control input $V(\bm\cdot)$. We formulate the problem of vaccination control as follows.

\[Vaccination control\] Given the SEIR model in (\[discrete\_vaccination\_model\]) and an MTL specification $\varphi_{\textrm{V}}$, compute the input signal $V(\bm\cdot)$ that minimize the vaccination control efforts ${\left\lVertV(\bm\cdot)\right\rVert}$ while satisfying $\left[\left[\varphi_{\textrm{V}}\right]\right](\xi_{\bm\cdot;x^{init}_{\textrm{V}},V}, 0)\ge0$, i.e., the trajectory $\xi_{\bm\cdot;x^{init}_{\textrm{V}},V}$ satisfies the MTL specification $\varphi_{\textrm{V}}$. \[problem1\]

The vaccination control synthesis problem can be formulated as a constrained optimization problem as follows. $$\begin{aligned}
\begin{split}
\underset{V(\cdot)}{{\mathrm{arg}\min}} ~ & {\left\lVertV[\cdot]\right\rVert}   \\
\text{subject to:} ~ 
& I[k+1] = I[k] + T_{\textrm{s}}\epsilon E[k] - T_{\textrm{s}}(\gamma+\mu+\alpha)I, \forall k=1,\dots,T-1, \\
& E[k+1] = E[k] + T_{\textrm{s}}\beta S[k]I[k]/N[k] - T_{\textrm{s}}(\mu+\epsilon)E[k], \forall k=1,\dots,T-1,  \\
& S[k+1] = S[k] + T_{\textrm{s}}\lambda N[k] - T_{\textrm{s}}\mu S[k] - T_{\textrm{s}}\beta S[k]I[k]/N[k] - T_{\textrm{s}}V[k], \\ &~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\forall k=1,\dots,T-1, \\
& R[k+1] = R[k] + T_{\textrm{s}}\gamma I[k] - T_{\textrm{s}}\mu R[k] + T_{\textrm{s}}V[k], \forall k=1,\dots,T-1, \\
& D[k] = N_0 - I[k] - E[k] - S[k] -R[k], \forall k=1,\dots,T,  \\
& 0\le V[k]\le V_{\textrm{max}}, \forall k=1,\dots,T, \nonumber \\ 
& \left[\left[\varphi_{\textrm{V}}\right]\right](\xi_{\bm\cdot;x^{init}_{\textrm{V}},V}, 0)\ge 0. 
\end{split}\end{aligned}$$ The above optimization problem is generally a mixed-integer non-linear programming problem. As the change of total population is relatively small compared to the multiplication of the susceptible population and the infectious population, we approximate the term $T_{\textrm{s}}\beta S[k]I[k]/N[k]$ with $T_{\textrm{s}}\beta S[k]I[k]/N_0$. With such approximation, the optimization problem becomes a mixed-integer bi-linear programming problem, which can be more efficiently solved using techniques such as McCormick’s relaxation [@McCormick1976; @Gupte2013SolvingMI]. Furthermore, if the MTL specification $\phi$ consists of only conjunctions ($\wedge$) and the always operator ($\Box$), the integers in the optimization problem can be eliminated and the problem becomes a bi-linear programming problem.\
**Shield immunity control**: For the COVID-19 SEIR model with shield immunity control, we discretize the model in (\[vaccination\_model\]) as follows. $$\begin{aligned}
\begin{cases}
I[k+1] = I[k] + T_{\textrm{s}}\epsilon E[k] - T_{\textrm{s}}(\gamma+\mu+\alpha)I[k];\\
E[k+1] = E[k] + T_{\textrm{s}}\beta S[k]I[k]/(N[k]+\chi[k]R[k]) - T_{\textrm{s}}(\mu+\epsilon)E[k];\\
S[k+1] = S[k] + T_{\textrm{s}}\lambda N[k] - T_{\textrm{s}}\mu S[k] - T_{\textrm{s}}\beta S[k]I[k]/(N[k]+\chi[k]R[k]);\\
R[k+1] = R[k] + T_{\textrm{s}}\gamma I[k] - T_{\textrm{s}}\mu R[k];\\
D[k+1] = D[k] - T_{\textrm{s}}\dot{I}[k]-T_{\textrm{s}}\dot{E}[k]-T_{\textrm{s}}\dot{S}[k]-T_{\textrm{s}}\dot{R}[k],
\end{cases}     
\label{discrete_shield_model}\end{aligned}$$ where $T_{\textrm{s}}$ is the sampling period.\
Following the notations in Section \[sec\_MTL\], we use $x_{\textrm{S}}=[I, E, S, R, D]$ to denote the state of (\[discrete\_shield\_model\]) and $\xi_{\bm\cdot;x^{init}_{\textrm{S}},\chi}$ to denote the trajectory of (\[discrete\_shield\_model\]) starting from $x^{init}_{\textrm{S}}=[I[1], E[1], S[1], R[1], D[1]]$ and shield immunity control input $\chi(\bm\cdot)$. We formulate the problem of shield immunity control as follows.

\[Shield immunity control\] Given the SEIR model in (\[discrete\_shield\_model\]) and an MTL specification $\varphi_{\textrm{S}}$, compute the input signal $\chi(\bm\cdot)$ that minimize the shield immunity control efforts ${\left\lVert\chi(\bm\cdot)\right\rVert}$ while satisfying $\left[\left[\varphi_{\textrm{S}}\right]\right](\xi_{\bm\cdot;x^{init}_{\textrm{S}},\chi}, 0)\ge0$, i.e., the trajectory $\xi_{\bm\cdot;x^{init}_{\textrm{S}},\chi}$ satisfies the MTL specification $\varphi_{\textrm{S}}$. \[problem1\]

The control synthesis problem can be formulated as a constrained optimization problem as follows. $$\begin{aligned}
\begin{split}
\underset{\chi(\cdot)}{{\mathrm{arg}\min}} ~ & {\left\lVert\chi[\cdot]\right\rVert}   \\
\text{subject to:} ~ 
& I[k+1] = I[k] + T_{\textrm{s}}\epsilon E[k] - T_{\textrm{s}}(\gamma+\mu+\alpha)I, \forall k=1,\dots,T-1, \\
& E[k+1] = E[k] + T_{\textrm{s}}\beta S[k]I[k]/(N[k]+\chi[k]R[k]) - T_{\textrm{s}}(\mu+\epsilon)E[k], \\ &~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\forall k=1,\dots,T-1,  \\
& S[k+1] = S[k] + T_{\textrm{s}}\lambda N[k] - T_{\textrm{s}}\mu S[k] - T_{\textrm{s}}\beta S[k]I[k]/(N[k]+\chi[k]R[k]), \\ &~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\forall k=1,\dots,T-1, \\
& R[k+1] = R[k] + T_{\textrm{s}}\gamma I[k] - T_{\textrm{s}}\mu R[k], \forall k=1,\dots,T-1, \\
& D[k] = N_0 - I[k] - E[k] - S[k] -R[k], \forall k=1,\dots,T,  \\
& 0\le \chi[k]\le \chi_{\textrm{max}}, \forall k=1,\dots,T, \nonumber \\ 
& \left[\left[\varphi_{\textrm{S}}\right]\right](\xi_{\bm\cdot;x^{init}_{\textrm{S}},\chi}, 0)\ge 0. 
\end{split}\end{aligned}$$ The above optimization problem is generally a mixed-integer fractional constrained programming problem. If the MTL specification $\phi$ consists of only conjunctions ($\wedge$) and the always operator ($\Box$), the integers in the optimization problem can be eliminated and the problem becomes a fractional constrained programming problem.\
**Quarantine control**: For the COVID-19 SEIR model with shield immunity control, we discretize the model in (\[vaccination\_model\]) as follows. $$\begin{aligned}
\begin{cases}
S[k+1] = S[k] - T_{\textrm{s}}\beta_0 U[k]S[k]/N[k];\\
U[k+1] = U[k] + T_{\textrm{s}}\beta_0 U[k]S[k]/N[k] - \gamma_1U[k];\\
Q[k+1] = Q[k] + T_{\textrm{s}}\gamma_1U[k] - T_{\textrm{s}}[\gamma_2 + (1-\gamma_2)\sigma]Q[k];\\
C[k+1] = C[k] + T_{\textrm{s}}[\gamma_2 + (1-\gamma_2)\sigma]Q[k],\\
\end{cases}     
\label{discrete_quarantine_model}\end{aligned}$$ where $T_{\textrm{s}}$ is the sampling period. We also use $\Delta C[k]=C[k+1]-C[k]$ to denote the number of confirmed infected individuals at day $k$.

Following the notations in Section \[sec\_MTL\], we use $x_{\textrm{Q}}=[S, U, Q, C]$ to denote the state of (\[discrete\_quarantine\_model\]) and $\xi_{\bm\cdot;x^{init}_{\textrm{Q}},q}$ to denote the trajectory of (\[discrete\_shield\_model\]) starting from $x^{init}_{\textrm{Q}}=[S[1], U[1], Q[1], C[1]]$ and quarantine control input $q(\bm\cdot)$. We formulate the problem of quarantine control as follows.

\[Quarantine control\] Given the SUQC with quarantine control model in (\[discrete\_quarantine\_model\]) and an MTL specification $\varphi_{\textrm{Q}}$, compute the input signal $q(\bm\cdot)$ that minimize the quarantine control efforts ${\left\lVertq(\bm\cdot)\right\rVert}$ while satisfying $\left[\left[\varphi_{\textrm{Q}}\right]\right](\xi_{\bm\cdot;x^{init}_{\textrm{Q}},q}, 0)\ge0$, i.e., the trajectory $\xi_{\bm\cdot;x^{init}_{\textrm{Q}},q}$ satisfies the MTL specification $\varphi_{\textrm{Q}}$. \[problem1\]

The control synthesis problem can be formulated as a constrained optimization problem as follows. $$\begin{aligned}
\begin{split}
\underset{q(\cdot)}{{\mathrm{arg}\min}} ~ & {\left\lVertq[\cdot]\right\rVert}  \\
\text{subject to:} ~ 
& S[k+1] = S[k] - T_{\textrm{s}}\beta_0 U[k]S[k]/N[k], \forall k=1,\dots,T-1, \\
& U[k+1] = U[k] + T_{\textrm{s}}\beta_0 U[k]S[k]/N[k] - q[k]U[k], \forall k=1,\dots,T-1,  \\
& Q[k+1] = Q[k] + T_{\textrm{s}}q[k]U[k] - T_{\textrm{s}}[\gamma_2 + (1-\gamma_2)\sigma]Q[k], \forall k=1,\dots,T-1, \\
& C[k+1] = C[k] + T_{\textrm{s}}[\gamma_2 + (1-\gamma_2)\sigma]Q[k], \forall k=1,\dots,T-1,   \\
& 0\le q[k]\le q_{\textrm{max}}, \forall k=1,\dots,T, \nonumber \\ 
& \left[\left[\varphi_{\textrm{Q}}\right]\right](\xi_{\bm\cdot;x^{init}_{\textrm{Q}},q}, 0)\ge 0. 
\end{split}\end{aligned}$$

The above optimization problem is generally a mixed-integer non-linear programming problem. As the change of total population is relatively small compared to the multiplication of the susceptible population and the un-quarantined infectious population, we approximate the term $T_{\textrm{s}}\beta_0 U[k]S[k]/N[k]$ with $T_{\textrm{s}}\beta_0 U[k]S[k]/N_0$. With such approximation, the optimization problem becomes a mixed-integer bi-linear programming problem, which can be more efficiently solved using techniques such as McCormick’s relaxation [@McCormick1976; @Gupte2013SolvingMI]. Furthermore, if the MTL specification $\phi$ consists of only conjunctions ($\wedge$) and the always operator ($\Box$), the integers in the optimization problem can be eliminated and the problem becomes a bi-linear programming problem.\

Simulation Results
==================

In this section, we implement the control synthesis approach in the three different control models as introduced in Section \[sec\_models\].

COVID-19 SEIR Model with Vaccination Control
--------------------------------------------

The parameters of the COVID-19 SEIR model are shown in Table \[parameter\_SEIR\]. They were estimated in [@Carcione_model] from the data in Lombardy, Italy in early phase corresponding to no isolation conditions. We consider three MTL specifications as shown in Table \[result\_vaccination\]. For example, $\varphi_1=\Box_{[0,100]} (\Delta D\le 0.01)\wedge\Box_{[0,100]} (D\le0.2)\wedge\Diamond_{[40, 60]}(R\ge6)$, which means “the deaths from infection should never exceed 0.01 million (10 thousand) per day and 0.2 million (i.e., 200 thousand) in total within the next 100 days, and the immune population should eventually exceed 6 million after 40 to 60 days”. We choose the initial values of the states as $I[1]=1$ (person), $E[1]=0.02$ million, $S[1]=9.9$ million, $R[1]=0$ and $D[1]=0$. We set $V_{\textrm{max}}=0.5$. Figure \[fig\_results0\] shows the simulation results without any vaccination. It can be seen that the three MTL specifications $\varphi_{\textrm{V}}^1$, $\varphi_{\textrm{V}}^2$ and $\varphi_{\textrm{V}}^3$ are all violated in such a situation. Note that as isolation measures were taken after the early phase in Lombardy, Italy, the real situation was better than those shown in Figure \[fig\_results0\]. Now we investigate the hypothetical scenario where isolation measures are replaced by vaccination.

  parameter          value           
  ------------------ ------------ -- --
  $\lambda$          1/30295         
  $\mu$              1/30295         
  $\alpha$           0.006/day       
  $\beta$            0.75/day        
  $\epsilon$         (1/3)/day       
  $\gamma$           (1/8)/day       
  $N_0$              10 million      
  $T_{\textrm{s}}$   1 day           

  : Parameters of COVID-19 SEIR model estimated from data from Lombardy, Italy in early phase corresponding to no isolation conditions [@Carcione_model].[]{data-label="parameter_SEIR"}

[ll&gt;p[20mm]{}]{}      MTL specification & control effort & computation time\

  -----------------------------------------------------------
   $\varphi_{\textrm{V}}^1=\Box_{[0,100]} (\Delta D\le0.01)$
            $~~~~~~\wedge\Box_{[0,100]} (D\le0.2)$
             $~~~\wedge\Diamond_{[40, 60]}(R\ge6)$
  -----------------------------------------------------------

  : MTL specifications and simulation results for vaccination control.[]{data-label="result_vaccination"}

&      1.104 &      1.128 s\

  ------------------------------------------------------------
   $\varphi_{\textrm{V}}^2=\Box_{[0,100]} (\Delta D\le0.005)$
             $~~~~~\wedge\Box_{[0,100]} (D\le0.2)$
              $~~\wedge\Diamond_{[40, 60]}(R\ge6)$
  ------------------------------------------------------------

  : MTL specifications and simulation results for vaccination control.[]{data-label="result_vaccination"}

&      2.033 &      2.286 s\

  ------------------------------------------------------------
   $\varphi_{\textrm{V}}^3=\Box_{[0,100]} (\Delta D\le0.005)$
             $~~~~~\wedge\Box_{[0,100]} (D\le0.05)$
               $\wedge\Diamond_{[40, 60]}(R\ge6)$
  ------------------------------------------------------------

  : MTL specifications and simulation results for vaccination control.[]{data-label="result_vaccination"}

&      4.022 &      4.609 s\

We use the solver GEKKO [@beal2018gekko] to solve the optimization problems. Figures \[fig\_results1\], \[fig\_results2\] and \[fig\_results3\] show the simulation results for vaccination control of COVID-19 SEIR model with MTL specifications $\varphi_{\textrm{V}}^1$, $\varphi_{\textrm{V}}^2$ and $\varphi_{\textrm{V}}^3$, respectively. The results show that the MTL specifications $\varphi_{\textrm{V}}^1$, $\varphi_{\textrm{V}}^2$ and $\varphi_{\textrm{V}}^3$ are satisfied with the synthesized vaccination control inputs respectively. It can be seen that vaccination within the first 40 days after the outbreak can mitigate the spread of SARS-CoV-2 in the most efficient manner. The results also show that the control effort for satisfying $\varphi_{\textrm{V}}^1$ is less than that for satisfying $\varphi_{\textrm{V}}^2$, which is still less than that for satisfying $\varphi_{\textrm{V}}^3$. This is consistent with the fact that $\varphi_{\textrm{V}}^2$ implies $\varphi_{\textrm{V}}^1$, and $\varphi_{\textrm{V}}^3$ implies both $\varphi_{\textrm{V}}^1$ and $\varphi_{\textrm{V}}^2$. For all three specifications, the computations for control synthesis are finished within 5 seconds.

[0.46]{} ![Simulation results for COVID-19 SEIR model estimated from data from Lombardy, Italy in early phase corresponding to no isolation conditions.[]{data-label="fig_results0"}](case0_a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for COVID-19 SEIR model estimated from data from Lombardy, Italy in early phase corresponding to no isolation conditions.[]{data-label="fig_results0"}](case0_c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for COVID-19 SEIR model estimated from data from Lombardy, Italy in early phase corresponding to no isolation conditions.[]{data-label="fig_results0"}](case0_d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^1$.[]{data-label="fig_results1"}](case1_a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^1$.[]{data-label="fig_results1"}](case1_b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^1$.[]{data-label="fig_results1"}](case1_c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^1$.[]{data-label="fig_results1"}](case1_d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^2$.[]{data-label="fig_results2"}](case2_a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^2$.[]{data-label="fig_results2"}](case2_b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^2$.[]{data-label="fig_results2"}](case2_c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^2$.[]{data-label="fig_results2"}](case2_d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^3$.[]{data-label="fig_results3"}](case3_a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^3$.[]{data-label="fig_results3"}](case3_b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^3$.[]{data-label="fig_results3"}](case3_c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with vaccination control and MTL specification $\varphi_{\textrm{V}}^3$.[]{data-label="fig_results3"}](case3_d.png "fig:"){width="\textwidth"}

COVID-19 SEIR Model with Shield Immunity Control
------------------------------------------------

We use the same parameters of the COVID-19 SEIR model as shown in Table \[parameter\_SEIR\]. We also choose the same initial values of the states as $I[1]=1$ (person), $E[1]=0.02$ million, $S[1]=9.9$ million, $R[1]=0$ and $D[1]=0$. We set $\chi_{\textrm{max}}=100$. Referring back to Figure \[fig\_results0\], it can be seen that the three MTL specifications $\varphi_{\textrm{S}}^1$, $\varphi_{\textrm{S}}^2$ and $\varphi_{\textrm{S}}^3$ are all violated without any control strategies. Now we investigate the hypothetical scenario where isolation measures are replaced by shield immunity control.

Figures \[fig\_results\_shield1\], \[fig\_results\_shield2\] and \[fig\_results\_shield3\] show the simulation results for shield immunity control of the COVID-19 SEIR model with MTL specifications $\varphi_{\textrm{S}}^1$, $\varphi_{\textrm{S}}^2$ and $\varphi_{\textrm{S}}^3$, respectively. The results show that the MTL specifications $\varphi_{\textrm{S}}^1$, $\varphi_{\textrm{S}}^2$ and $\varphi_{\textrm{S}}^3$ are satisfied with the synthesized shield immunity control inputs respectively. We observe that with the three MTL specifications, the synthesized shield immunity control inputs all increase to a peak at approximated 20 days after the outbreak and then gradually decrease. These observations are consistent with the claim that shield immunity at early phases of the outbreak can mitigate the spread of SARS-CoV-2 in the most efficient manner. The results also show that the control effort for satisfying $\varphi_{\textrm{S}}^1$ is less than that for satisfying $\varphi_{\textrm{S}}^2$, which is still less than that for satisfying $\varphi_{\textrm{S}}^3$. This is consistent with the fact that $\varphi_{\textrm{S}}^2$ implies $\varphi_{\textrm{S}}^1$, and $\varphi_{\textrm{S}}^3$ implies both $\varphi_{\textrm{S}}^1$ and $\varphi_{\textrm{S}}^2$. For all three specifications, the computations for control synthesis are finished within 5 seconds.

[ll&gt;p[20mm]{}]{}      MTL specification & control effort & computation time\

  -----------------------------------------------------------
   $\varphi_{\textrm{S}}^1=\Box_{[0,100]} (\Delta D\le0.01)$
            $~~~~~~\wedge\Box_{[0,100]} (D\le0.2)$
             $~~~\wedge\Diamond_{[40, 60]}(R\ge6)$
  -----------------------------------------------------------

  : MTL specifications and simulation results for shield immunity control.

&      39660.76 &      4.402 s\

  ------------------------------------------------------------
   $\varphi_{\textrm{S}}^2=\Box_{[0,100]} (\Delta D\le0.005)$
             $~~~~~\wedge\Box_{[0,100]} (D\le0.2)$
              $~~\wedge\Diamond_{[40, 60]}(R\ge6)$
  ------------------------------------------------------------

  : MTL specifications and simulation results for shield immunity control.

&      49422.85 &      2.881 s\

  ------------------------------------------------------------
   $\varphi_{\textrm{S}}^3=\Box_{[0,100]} (\Delta D\le0.005)$
             $~~~~~\wedge\Box_{[0,100]} (D\le0.15)$
               $\wedge\Diamond_{[40, 60]}(R\ge6)$
  ------------------------------------------------------------

  : MTL specifications and simulation results for shield immunity control.

&      94526.45 &      3.387 s\

\[result\_shield\]

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^1$.[]{data-label="fig_results_shield1"}](case_shield_phi1a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^1$.[]{data-label="fig_results_shield1"}](case_shield_phi1b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^1$.[]{data-label="fig_results_shield1"}](case_shield_phi1c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^1$.[]{data-label="fig_results_shield1"}](case_shield_phi1d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^2$.[]{data-label="fig_results_shield2"}](case_shield_phi2a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^2$.[]{data-label="fig_results_shield2"}](case_shield_phi2b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^2$.[]{data-label="fig_results_shield2"}](case_shield_phi2c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^2$.[]{data-label="fig_results_shield2"}](case_shield_phi2d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^3$.[]{data-label="fig_results_shield3"}](case_shield_phi3a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^3$.[]{data-label="fig_results_shield3"}](case_shield_phi3b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^3$.[]{data-label="fig_results_shield3"}](case_shield_phi3c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SEIR model with shield immunity control and MTL specification $\varphi_{\textrm{S}}^3$.[]{data-label="fig_results_shield3"}](case_shield_phi3d.png "fig:"){width="\textwidth"}

COVID-19 SUQC model with quarantine control
-------------------------------------------

The parameters of the COVID-19 SUQC model are shown in Table \[parameter\_SUQC\]. They were estimated in [@Zhao2020] from the data in Wuhan, China. We choose the initial values of the states as $S[1]=8.9$ million, $U[1]=0.001$ million, $Q[1]=0$ and $C[1]=0$. We set $q_{\textrm{max}}=1$. Figure \[fig\_results\_quarantine0\] shows the simulation results for the COVID-19 SUQC model estimated from data in Stage I of Wuhan, China. It can be seen that the three MTL specifications $\varphi_{\textrm{Q}}^1$, $\varphi_{\textrm{Q}}^2$ and $\varphi_{\textrm{Q}}^3$ are all violated in such a situation (with quarantine rate being always 0.063). Now we investigate the scenario where the quarantine rate can be controlled to satisfy the MTL specifications.

  parameter          value            
  ------------------ ------------- -- --
  $\beta_0$          0.2967           
  $\gamma_2$         0.05             
  $N$                8.9 million      
  $\sigma$           0                
  $T_{\textrm{s}}$   1 day            

  : Parameters of the COVID-19 SUQC model estimated from data from Wuhan, China [@Zhao2020].[]{data-label="parameter_SUQC"}

Figures \[fig\_results\_quarantine1\], \[fig\_results\_quarantine2\] and \[fig\_results\_quarantine3\] show the simulation results for quarantine control of the COVID-19 SUQC model with MTL specifications $\varphi_{\textrm{Q}}^1$, $\varphi_{\textrm{Q}}^2$ and $\varphi_{\textrm{Q}}^3$, respectively. The results show that the MTL specifications $\varphi_{\textrm{Q}}^1$, $\varphi_{\textrm{Q}}^2$ and $\varphi_{\textrm{Q}}^3$ are satisfied with the synthesized quarantine control inputs respectively. The results also show that the control effort for satisfying $\varphi_{\textrm{Q}}^1$ is less than that for satisfying $\varphi_{\textrm{Q}}^2$, which is still less than that for satisfying $\varphi_{\textrm{Q}}^3$. This is consistent with the fact that $\varphi_{\textrm{Q}}^2$ implies $\varphi_{\textrm{Q}}^1$, and $\varphi_{\textrm{Q}}^3$ implies both $\varphi_{\textrm{Q}}^1$ and $\varphi_{\textrm{Q}}^2$. We observe that with $\varphi_{\textrm{Q}}^1$, the synthesized quarantine control inputs first increase to a peak at approximated 90 days after the outbreak and then gradually decrease; with $\varphi_{\textrm{Q}}^2$, the synthesized quarantine control inputs first increase to a peak at approximated 50 days after the outbreak and then gradually decrease; and with $\varphi_{\textrm{Q}}^3$, the synthesized quarantine control inputs are at a peak from the beginning of the outbreak and gradually decrease. These observations are consistent with the claim that quarantine at early phases of the outbreak of SARS-CoV-2 can reduce the number of confirmed infected cases in the most efficient manner, and more stringent control specification generally require stronger quarantine measures to be implemented in earlier phases after the outbreak. For all three specifications, the computations for control synthesis are finished within 5 seconds.

[ll&gt;p[20mm]{}]{}      MTL specification & control effort & computation time\

  ------------------------------------------------------------
   $\varphi_{\textrm{Q}}^1=\Box_{[0,200]} (\Delta C\le0.001)$
             $~~~~~~\wedge\Box_{[0,200]} (C\le0.1)$
  ------------------------------------------------------------

  : MTL specifications and simulation results for quarantine control.

&      19.5 &      4.296 s\

  -------------------------------------------------------------
   $\varphi_{\textrm{Q}}^2=\Box_{[0,200]} (\Delta C\le0.0005)$
             $~~~~~\wedge\Box_{[0,200]} (C\le0.05)$
  -------------------------------------------------------------

  : MTL specifications and simulation results for quarantine control.

&      20.021 &      1.753 s\

  -------------------------------------------------------------
   $\varphi_{\textrm{Q}}^3=\Box_{[0,200]} (\Delta C\le0.0005)$
             $~~~~~\wedge\Box_{[0,200]} (C\le0.02)$
  -------------------------------------------------------------

  : MTL specifications and simulation results for quarantine control.

&      20.54 &      4.578 s\

\[result\_quarantine\]

[0.46]{} ![Simulation results for the COVID-19 SUQC model estimated from data in Stage I of Wuhan, China.[]{data-label="fig_results_quarantine0"}](case_quarantine_phi0a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model estimated from data in Stage I of Wuhan, China.[]{data-label="fig_results_quarantine0"}](case_quarantine_phi0c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model estimated from data in Stage I of Wuhan, China.[]{data-label="fig_results_quarantine0"}](case_quarantine_phi0d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^1$.[]{data-label="fig_results_quarantine1"}](case_quarantine_phi1a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^1$.[]{data-label="fig_results_quarantine1"}](case_quarantine_phi1b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^1$.[]{data-label="fig_results_quarantine1"}](case_quarantine_phi1c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^1$.[]{data-label="fig_results_quarantine1"}](case_quarantine_phi1d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^2$.[]{data-label="fig_results_quarantine2"}](case_quarantine_phi2a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^2$.[]{data-label="fig_results_quarantine2"}](case_quarantine_phi2b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^2$.[]{data-label="fig_results_quarantine2"}](case_quarantine_phi2c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^2$.[]{data-label="fig_results_quarantine2"}](case_quarantine_phi2d.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^3$.[]{data-label="fig_results_quarantine3"}](case_quarantine_phi3a.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^3$.[]{data-label="fig_results_quarantine3"}](case_quarantine_phi3b.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^3$.[]{data-label="fig_results_quarantine3"}](case_quarantine_phi3c.png "fig:"){width="\textwidth"}

[0.46]{} ![Simulation results for the COVID-19 SUQC model with quarantine control and MTL specification $\varphi_{\textrm{Q}}^3$.[]{data-label="fig_results_quarantine3"}](case_quarantine_phi3d.png "fig:"){width="\textwidth"}

Conclusion
==========

In this paper, we proposed automatically-synthesized and fine-tuned control synthesis methods for mitigating the COVID-19 epidemic with three models with vaccination, shield immunity and quarantine, respectively. We used metric temporal logic (MTL) formulas to formally specify the required performance of the control strategies. The proposed approach can synthesize control inputs within a relatively short time (i.e., within 5 seconds) that can satisfy the MTL specifications.

The preliminary work in this paper opens the door to the formal synthesis of control strategies for epidemic models. We list several future work as follows. First, we will investigate the effects of model uncertainties and parameter uncertainties in the control synthesis, and explore robust control synthesis methods in the presence of such uncertainties. Second, we will extend this work to online control synthesis so that control inputs can be generated in real-time based on the latest information (e.g., using online parameter identification and receding horizon control). Finally, as we investigated the three control strategies separately in this paper, we will study the benefits and costs of joint control of different control strategies (vaccination, shield immunity and quarantine) so that the specifications can be satisfied with coordinated efforts.

[^1]: Zhe Xu and Bo Wu are with the Oden Institute for Computational Engineering and Sciences, University of Texas, Austin, Austin, TX 78712, Ufuk Topcu is with the Department of Aerospace Engineering and Engineering Mechanics, and the Oden Institute for Computational Engineering and Sciences, University of Texas, Austin, Austin, TX 78712, e-mail: zhexu@utexas.edu, bowu86@gmail.com, utopcu@utexas.edu.
