A Framework Based on MSVL for Verifying Probabilistic Properties in Social Networks

social networks, there are many phenomena related to randomness, such as interaction behaviors of users and dynamic changes of network structure. In this work, a framework based on MSVL (Modeling, Simulation and Verification Language) for verifying probabilistic properties in social networks is proposed. First, a hidden Markov model (HMM) is trained with the real social network dataset and implemented by MSVL. Then, an observed sequence is input into the trained HMM to obtain relevant information of the network, according to specialized algorithms. Next, a probabilistic property is specified with a formula of Propositional Projection Temporal Logic (PPTL). Finally, it is verified whether the MSVL model satisfies the PPTL property by model checking. An example of Sina Weibo is provided to illustrate how the framework works.