Robust Pandemic Control Synthesis with Formal Specifications: A Case Study on COVID-19 Pandemic

TL;DR

This paper presents a formal, logic-based approach to synthesizing robust COVID-19 control strategies using SEIR models with vaccination and shield immunity, ensuring compliance with specified temporal logic constraints.

Contribution

It introduces an iterative synthesis method for optimal pandemic control strategies expressed in metric temporal logic, validated through simulations on real-world data.

Findings

Control strategies satisfy MTL specifications robustly

Effective vaccination and shield immunity controls demonstrated

Model parameters estimated from Lombardy, Italy data

Abstract

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.