A model checking approach to countering the dynamics of infection propagation over network

Open Access
Zhang, Can
Graduate Program:
Information Sciences and Technology
Master of Science
Document Type:
Master Thesis
Date of Defense:
March 31, 2016
Committee Members:
  • Dinghao Wu, Thesis Advisor
  • Model checking
With the outbreak of Ebola over the past year, attention has been paid on predicting and resolving the propagation of infectious disease over network of people and animals. Model checking is a commonly used method in the field of software analysis and verification. In this thesis, we propose to use model checking to counteract the spread of foot-and-mouth disease (FMD) in networks. We abstract the FMD spread model and properties, and encode the system using a well-known model checker Spin. Our program is capable of finding intervention policies and evaluating the effectiveness of different policies. Moreover, previous works generally use simulation models to study the disease control problem which cannot provide certainty as to predict whether certain future states of the outbreak are possible under a particular control policy. Model checking, on the other hand, is guaranteed to find a path that leads to the future states as long as they are possible from a given current configuration of the contagion network under a given control policy. It is worth mentioning that the method proposed in this thesis is not limited to infectious diseases, but can also be applied to counter the spread of, for example, computer virus, forest fire, and public opinions.