English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Ever since the outbreak of the COVID-19 epidemic, various public healthcontrol strategies have been proposed and tested against the coronavirusSARS-CoV-2. We study three specific COVID-19 epidemic control models: thesusceptible, exposed, infectious, recovered (SEIR) model with vaccinationcontrol; the SEIR model with shield immunity control; and the susceptible,un-quarantined infected, quarantined infected, confirmed infected (SUQC) modelwith quarantine control. We express the control requirement in metric temporallogic (MTL) formulas (a type of formal specification languages) which canspecify the expected control outcomes such as "the deaths from the infectionshould never exceed one thousand per day within the next three months" or "thepopulation immune from the disease should eventually exceed 200 thousand withinthe next 100 to 120 days". We then develop methods for synthesizing controlstrategies with MTL specifications. To the best of our knowledge, this is thefirst paper to systematically synthesize control strategies based on theCOVID-19 epidemic models with formal specifications. We provide simulationresults in three different case studies: vaccination control for the COVID-19epidemic with model parameters estimated from data in Lombardy, Italy; shieldimmunity control for the COVID-19 epidemic with model parameters estimated fromdata in Lombardy, Italy; and quarantine control for the COVID-19 epidemic withmodel parameters estimated from data in Wuhan, China. The results show that theproposed synthesis approach can generate control inputs such that thetime-varying numbers of individuals in each category (e.g., infectious, immune)satisfy the MTL specifications. The results also show that early interventionis essential in mitigating the spread of COVID-19, and more control effort isneeded for more stringent MTL specifications.

Control Strategies for COVID-19 Epidemic with Vaccination, Shield Immunity and Quarantine: A Metric Temporal Logic Approach