on a model that differentiates quarantined infected individuals and un-quarantined infected individuals.

Despite the fact that various promising control strategies have been proposed against SARS-CoV-2, such control strategies still suffer from several limitations. (a) The control strategies SARS-CoV-2 often treat the control inputs (e.g., the shield strength in shield immunity, the quarantine rate in quarantine control) as parameters which stay constant during one stage of time, while in reality such inputs could be changed on a daily basis for more fine-tuned control. (b) The control inputs in the literature are often tuned manually through trial-and-error, instead of being synthesized automatically. (c) There is a lack of specific and formal specifications for the expected effects and outcomes of the control strategies.

To address these limitations, we propose an automatically-synthesized fine-tuned control synthesis approach for three control strategies in mitigating SARS-CoV-2. We use *metric temporal logic* (MTL) formulas to specify the expected outcomes such as “the deaths from the infection should always not exceed one thousand per day within the next three months” or “the people immune from the disease should eventually exceed 200 thousand within the next 100 to 120 days”. Such temporal logic formulas have been used as high-level knowledge 