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 