  Pandemics can bring a range of devastating consequences to public health and
the world economy. Identifying the most effective control strategies has been
the imperative task all around the world. Various public health control
strategies have been proposed and tested against pandemic diseases (e.g.,
COVID-19). We study two specific pandemic control models: the susceptible,
exposed, infectious, recovered (SEIR) model with vaccination control; and the
SEIR model with shield immunity control. We express the pandemic control
requirement in metric temporal logic (MTL) formulas. We then develop an
iterative approach for synthesizing the optimal control strategies with MTL
specifications. We provide simulation results in two different scenarios for
robust control of the COVID-19 pandemic: one for vaccination control, and
another for shield immunity control, with the model parameters estimated from
data in Lombardy, Italy. The results show that the proposed synthesis approach
can generate control inputs such that the time-varying numbers of individuals
in each category (e.g., infectious, immune) satisfy the MTL specifications with
robustness against initial state and parameter uncertainties.
