control of epidemic models with formal specifications (e.g., expressed in temporal logic formulas).

**Control synthesis with temporal logic specifications**: There are three main categories of approaches to design controllers that meet temporal logic specifications [@KHFP; @RVFK2012; @KKW2002; @MH2019IFAC; @STJC2010; @UASX2011; @liu2017distributed; @Djeumou2020; @liu2017communication; @liu2020distributed; @cubuktepe2020policy]. The first category of approaches abstract the system as a transition system and transform the controller syntheses problem into a series of constrained reachability problems [@Topcu; @Dimarogonas; @Coogan]. The second category of approaches mainly focus on linear dynamics and it converts the control synthesis problem into a mixed-integer linear programming (MILP) problem [@BluSTL; @sayan2016; @Allerton2019; @zheACC2019DF; @zhe_advisory; @zheACC2018wind] and the controller then consists in a pre-compiled MILP which can be solved efficiently by MILP solvers. The third category of approaches substitute the temporal logic constraint into the optimization problem and apply a functional gradient descent algorithm on the resulting unconstrained problem [@Andygradient; @Abbas2014; @zhe_control; @zheACCstorageControl]. The control synthesis approach in this paper is based on the second category of approaches, but we have extended the method to non-linear dynamics to fit the epidemic models for COVID-19.

Metric Temporal Logic (MTL) {#sec_MTL}
===========================

In this section, we briefly review metric temporal logic (MTL) [@FainekosMTL] interpreted over 