  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.
