Abstract: Network exists widely in nature and human society. The spread of infections, such as computer viruses, diseases and rumors, poses great challenges to economic and societal system. It is an important issue in the network transmission control to protect individuals by finding effective intervention policies. This paper focuses on the network transmission model affected by time and adjacent nodes. Based on existing static protection work, a further study on dynamic protection cases is conducted, and four kinds of analyses of intervention policies are summarized. The intervention goals are expressed as logical properties and an effective approach of searching for intervention policies via model checking is proposed. Furthermore, experiments on random and small-world networks are conducted, demonstrating the advantages and disadvantages of model checkers NuSMV and SPIN on solving intervention problems. The results indicate that NuSMV needs less memory, but more time to complete searching, for example three times are unfinished in total six trails because of time exceeding in the dynamic recoverable problem; SPIN needs less time, but more memory, for example one time is unfinished in total six trails because of memory exceeding in the static unrecoverable problem.

Key words: model checking, network propagation, intervention policies

摘要： 网络广泛存在于自然界和人类生活中，计算机病毒、传染疾病、森林火灾和社会流言等在网络中的传播给经济、社会带来巨大挑战，寻找有效的干预策略实现对网络传播的控制是一个重要的研究问题。对受时间和邻接点影响的网络传播模型进行了重点关注，在已有静态保护工作的基础上，进一步研究了动态保护情况，总结了4类相关的干预策略分析问题；通过将干预目标描述为相应的时序逻辑属性，给出了通过模型检测找出有效的干预策略以抑制传播的方法。针对随机和小世界两种网络，比较分析了NuSMV和SPIN两种模型检测工具在解决具体网络传播干预策略问题中的优缺点。实验结果表明，NuSMV的内存使用量较少，但运行时间较多，对于动态可恢复问题的6次实验中有3次超时；SPIN运行时间较少，但内存使用量较大，对于静态不可恢复问题的6次实验中有1次内存超出。

关键词: 模型检测, 网络传播, 干预策略