A Model Checking based Framework for Analyzing Information-Propagation over Networks

在全球化和信息化的时代，信息在网络中的传播研究在理解和分析安全和安全问题方面起着重要的作用。网络中的实体可以是人、组或计算设备，而网络是描述一个实体如何影响其他实体或如何被其他实体影响的关系。在流行病学中，实体网络可以对应于人口群体及其空间/邻近关系。在社会科学或市场科学中，网络捕捉思想和信息（或同行之间的错误信息，或领导者和追随者）的交流，研究重点是确定足以影响整个网络的关键实体群体。 在所有上述应用中，中心主题是分析信息/感染的传播，并使用外部影响/刺激来将其传播控制在所需水平内或最大化其影响。这种影响传播的外部影响/刺激可以被称为疫苗。本项目研究如何确定部署疫苗的方式，以及部署疫苗的顺序，以实现预期目标。该项目的核心是开发和应用形式化方法技术，特别是模型检查，以捕获网络中信息传播的动态并对其进行分析。长期的目标是开发一个强大的和应用领域不可知的框架，这将允许简洁和精确的表示网络和传播模型的信息作为一个有限状态图，和所需的目标，在图的时间属性。该项目在应用领域和解决方案方法之间建立了一种自然的联系，进一步促进了形式化方法的研究，特别是在开发新型规范语言和有效技术来分析和探索用这种语言表达的模型方面。教育和研究活动的跨学科性质以及研究成果的传播将有助于开辟新的研究途径，不仅在正式方法方面，而且在信息传播和分析方面。该项目涉及本科生和代表性不足的学生。

In the age of globalization and informatization, the study of information propagation in the network of connected entities plays an important role in understanding and analyzing security and safety concerns. Entities in the network can be people, groups or computing devices, while the network is the relationship describing how one entity can influence or can be influenced by others. In epidemiology, the network of entities may correspond to the population groups and their spatial/proximity relationships. In social or market sciences, the network captures the exchange of ideas and information (or misinformation among peers, or leaders and followers), and the studies focus on identifying the critical groups of entities that are sufficient to influence the entire network. In all the above applications, the central theme is to analyze the spread of information/infection and use external influences/stimuli to either contain its spread within desired level or maximize its impact. Such external influences/stimuli that impact the spread can be referred to as vaccines. This project investigates ways to identify the way to deploy the vaccines, and the order in which to do so to realize the desired objective. At its core, the project develops and applies formal method techniques, particularly model checking, to capture the dynamics of information spread in a network and analyze them. The long term objective is to develop a robust and application-domain agnostic framework which will allow succinct and precise representation of network and spread-model of information as a finite-state graph, and desired objectives as temporal properties over the graph. The project establishes a natural connection between the application domains and solution methodology, which furthers research in formal methods, particularly in terms of developing new types of specification language and efficient techniques to analyze and explore models expressed in this language. The cross-disciplinary nature of the educational and research activities, and the dissemination of research results will help to open new avenues of research not only in formal methods but also in information propagation and analysis. The project involves undergraduate and under-represented students.