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

基于模型检查的网络信息传播分析框架

• 批准号: 1555780
• 负责人: Samik Basu
• 金额: $ 12.47万
• 依托单位: Iowa State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1555780&HistoricalAwards=false
• 关键词: Model; Checking; based; Framework; Analyzing

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.

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