@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 