Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2402.09121 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911776990298112 |
|---|---|
| author | Leys, Tim Perez, Guillermo A. |
| author_facet | Leys, Tim Perez, Guillermo A. |
| contents | Compartmental models are used in epidemiology to capture the evolution of infectious diseases such as COVID-19 in a population by assigning members of it to compartments with labels such as susceptible, infected, and recovered. In a stochastic compartmental model the flow of individuals between compartments is determined probabilistically. We establish that certain stochastic compartment models can be encoded as probabilistic counter machines where the configurations are bounded. Based on the latter, we obtain simple descriptions of the models in the PRISM language. This enables the analysis of such compartmental models via probabilistic model checkers. Finally, we report on experimental results where we analyze results from a Belgian COVID-19 model using a probabilistic model checkers. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_09121 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Inform: From Compartmental Models to Stochastic Bounded Counter Machines Leys, Tim Perez, Guillermo A. Formal Languages and Automata Theory Compartmental models are used in epidemiology to capture the evolution of infectious diseases such as COVID-19 in a population by assigning members of it to compartments with labels such as susceptible, infected, and recovered. In a stochastic compartmental model the flow of individuals between compartments is determined probabilistically. We establish that certain stochastic compartment models can be encoded as probabilistic counter machines where the configurations are bounded. Based on the latter, we obtain simple descriptions of the models in the PRISM language. This enables the analysis of such compartmental models via probabilistic model checkers. Finally, we report on experimental results where we analyze results from a Belgian COVID-19 model using a probabilistic model checkers. |
| title | Inform: From Compartmental Models to Stochastic Bounded Counter Machines |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2402.09121 |