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.

2015-09-01 to 2017-08-31
Award Amount: 
Award Number: