论文标题
疫苗接种，屏蔽免疫力和隔离的共同-19流行病的控制策略：公制的时间逻辑方法
Control Strategies for COVID-19 Epidemic with Vaccination, Shield Immunity and Quarantine: A Metric Temporal Logic Approach
论文作者
论文摘要
自从Covid-19流行病爆发以来，已经提出了各种公共卫生控制策略，并针对冠状病毒SARS-COV-2进行了测试。我们研究了三个特定的COVID-199流行病控制模型：具有疫苗接种控制的易感，暴露，传染性，回收（SEIR）模型；具有盾牌免疫控制的SEIR模型；以及具有隔离控制的易感性，不受保证的感染，被隔离的感染，被确认的感染（SUQC）模型。我们表达了公制时间逻辑（MTL）公式（一种形式规范语言）的控制要求，该公式可以指定预期的控制结果，例如“感染的死亡在接下来的三个月内绝不应每天不超过1000个”或“在未来100至120天内，疾病的人口最终应超过疾病的人口免疫。然后，我们开发使用MTL规范合成控制策略的方法。据我们所知，这是基于与正式规格的Covid-19流行病模型系统合成控制策略的第一篇论文。我们在三个不同的案例研究中提供了仿真结果：COVID-19的疫苗接种控制，其模型参数是根据意大利伦巴第数据估算的模型参数； Covid-19流行病的屏蔽免疫控制与意大利伦巴第数据估算的模型参数；与中国武汉数据估算的模型参数对COVID-19的流行病进行了隔离控制。结果表明，所提出的合成方法可以生成控制输入，从而使每个类别中的时间变化数量（例如传染性，免疫）满足MTL规格。结果还表明，早期干预对于减轻COVID-19的传播至关重要，并且需要更多的控制努力才能进行更严格的MTL规格。
Ever since the outbreak of the COVID-19 epidemic, various public health control strategies have been proposed and tested against the coronavirus SARS-CoV-2. We study three specific COVID-19 epidemic control models: the susceptible, exposed, infectious, recovered (SEIR) model with vaccination control; the SEIR model with shield immunity control; and the susceptible, un-quarantined infected, quarantined infected, confirmed infected (SUQC) model with quarantine control. 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 strategies with MTL specifications. To the best of our knowledge, this is the first paper to systematically synthesize control strategies based on the COVID-19 epidemic models with formal specifications. We provide simulation results in three different case studies: vaccination control for the COVID-19 epidemic with model parameters estimated from data in Lombardy, Italy; shield immunity control for the COVID-19 epidemic with model parameters estimated from data in Lombardy, Italy; and quarantine control for the COVID-19 epidemic with model parameters estimated from data in Wuhan, China. 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. The results also show that early intervention is essential in mitigating the spread of COVID-19, and more control effort is needed for more stringent MTL specifications.
