1:20 PM - 1:40 PM
[2E3-OS-13b-01] Bounded Model Checking with Boolean Formulas in Susceptible-Infected-Recovered Model
Keywords:COVID-19, infectious disease modelling, susceptible-infected-recovered model, bounded model checking, satisfiability problem
Since threats of the COVID-19 continues to have great impacts for human society, it is important to study the nature of infectious diseases.
A SIR (Susceptible-Infected-Recovered) model explains a nature of stochastic processes by using stochastic differential equations.
Although this model gives us important properties, it can lead to meaningless results if the probabilistic parameters deviate from reality.
In this paper, a non-stochastic formulation of the SIR model is investigated.
A satisfiability problem (SAT) based symbolical representation with Boolean formulas is proposed in order to describe all possible states of the SIR model, where it is irrelevant what kind of probability distribution the state transition depends on.
The bounded model checking which is a method of verifying whether a system can reach a desired (or undesired) state within a finite time is also proposed.
Numerical experiments with SMT (Satisfiability Modulo Theory) solver shows the effectiveness of this model.
A SIR (Susceptible-Infected-Recovered) model explains a nature of stochastic processes by using stochastic differential equations.
Although this model gives us important properties, it can lead to meaningless results if the probabilistic parameters deviate from reality.
In this paper, a non-stochastic formulation of the SIR model is investigated.
A satisfiability problem (SAT) based symbolical representation with Boolean formulas is proposed in order to describe all possible states of the SIR model, where it is irrelevant what kind of probability distribution the state transition depends on.
The bounded model checking which is a method of verifying whether a system can reach a desired (or undesired) state within a finite time is also proposed.
Numerical experiments with SMT (Satisfiability Modulo Theory) solver shows the effectiveness of this model.
Authentication for paper PDF access
A password is required to view paper PDFs. If you are a registered participant, please log on the site from Participant Log In.
You could view the PDF with entering the PDF viewing password bellow.