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.