Verifying Intervention Policies to Counter Infection Propagation over Networks: A Model Checking Approach

Abstract

Spread of infections (diseases, ideas, etc.) in a network
can be modeled as the evolution of states of nodes in
a graph as a function of the states of their neighbors.
Given an initial configuration of a network in which a
subset of the nodes have been infected, and an infection
propagation function that specifies how the states of
the nodes evolve over time, we show how to use model
checking to identify, verify, and evaluate the effectiveness
of intervention policies for containing the propagation
of infection over such networks.