Before revision:  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.
After revision:  We express the control requirement in metric temporal logic (MTL) formulas (a type of formal specification languages) which can specify the expected control outcomes such as "the deaths from the infection should never exceed one thousand per day within the next three months" or "the population immune from the disease should eventually exceed 200 thousand within the next 100 to 120 days". We then develop methods for synthesizing control inputs based on three specific COVID-19 epidemic models with MTL specifications.