Verification Of Probabilistic Properties In Social Networks Based On MSVL

In recent years,with the vigorous development of Internet,social networks have become the research hotspot in various fields,especially in the field of computer science.Researching the social activities of users can effectively reveal the evolution rules of the social networks structure and the rules of information dissemination.It has important theoretical significance for promoting the further development of social networks.Individuals of social networks are highly motivated,and their social behavior are highly random,such as the generation and disappearance of individual relationships.Fully studying the random characteristics of social networks can better explore the hidden and indirectly observable useful information.At present,some models are used to study the randomness of social networks such as Markov chains,HMM(hidden Markov models),Markov Random Fields,and Bayesian Networks.And formal methods have been applied to social networks,such as privacy policy verification,security verification,event detection,but most have not considered the randomness of social networks,especially using the hidden Markov models to study the underlying randomness of social networks.This thesis proposes a method based on MSVL(Modeling,Simulation and Verification Language)to study the probabilistic properties of social networks.It combines the HMM with formal methods to study the randomness in social networks.The specific process of this method consists of four steps.Firstly,the hidden state and the observation state are determined,and the corresponding data set is obtained and discretized,then the HMM is trained with the dataset and the supervised or non-supervised algorithm.Then,the HMM and related algorithms such as Viterbi,forward are implemented with MSVL,and dataset is input,then the information of user random behavior is obtained.Finally,we specify the probability property with PPTL and verify the properties in MC compiler with the unified model checking,and analyze the verification result.In addition,the examples of the Sina Weibo and the animal social network are provided to illustrate how the method works.The Hidden Markov Model based on Sina Weibo considers the interaction behavior of users as the observation state and the tie strength of users as the hidden state.Then the HMM is implemented with MSVL.Next the probabilistic properties of user interaction and user tie strength are specified with PPTL.Finally,verify and analysis these property in the MC compiler,and compare with other tools.The second example studies the social behavior of fish through the speed of the shoal of fish.In the HMM,the speed of fish is taken as the observation state and the average speed of the surrounding fish is taken as the hidden state.Then the HMM is implemented with MSVL.Next the probabilistic properties of fish social behavior are specified with PPTL.Finally,verify and analysis these property in the MC compiler,and compare with other tools.