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 