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 