基于MSVL的社交网络概率性质的验证

发布时间：2020-08-06 09:51

【摘要】：近年来随着互联网的蓬勃发展,社交网络已成为各个领域的研究热点,尤其是计算机领域。研究社交网络中个体的社交活动可以充分地了解社交网络结构的变化规律及信息传播规律,这对于促进社交网络的进一步发展具有重要的理论指导意义。社交网络中的个体具有高度的能动性,个体的社交行为具有很强的随机性,如个体关系产生、消亡等。充分研究社交网络中这些随机的特性,可以更好地发掘其中隐藏的、不可直接观测的有用信息。目前,一些模型被用于研究社交网络中的随机性,如马尔可夫链、隐马尔可夫模型(Hidden Markov Model)、马尔可夫随机场和贝叶斯网络等。并且形式化方法已被应用于社交网络的隐私策略验证、安全性验证、事件检测等方面,但这些研究大都没有考虑到社交网络的随机性,特别是使用HMM来研究其中潜藏的随机性。本文提出一种基于时序逻辑程序设计语言(Modeling Simulation and Verification Language,MSVL)研究社交网络中概率性质的方法,将HMM与MSVL相结合来研究社交网络的随机性。该方法的具体流程是:首先,确定模型中的隐状态和观测状态并根据需求获取数据集,再对数据集进行离散化处理并采用监督学习或者非监督学习的算法对数据集进行训练,得出HMM;然后,用MSVL对该模型及相关算法如Viterbi、forward等进行实现并输入测试数据集,来得出与用户随机行为相关的概率信息;最后,用命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)对用户概率的性质进行描述,并采用统一模型检测方法在MC编译器中对性质进行验证和分析。另外,通过新浪微博和动物社交网络两个实例分析来说明方法的有效性。第一个实例将用户间的交互行为视为观测状态,将用户间的关系强度视为隐状态,使用隐马尔可夫模型进行建模并用MSVL对其进行实现;然后用PPTL描述用户交互行为和关系强度两类概率的性质;最后在MC编译器中进行验证、分析并与其它工具进行对比。第二个实例通过鱼群运动过程中的速度来研究鱼群中个体的社交行为,将鱼群中个体的游泳速度视为观测状态,将该个体周围鱼的平均游泳速度视为隐状态,使用隐马尔可夫模型进行建模并用MSVL对其进行实现;然后用PPTL公式描述鱼社交行为概率的性质;最后在MC编译器中进行验证、分析并与其它工具进行对比。
【学位授予单位】：西安电子科技大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP393.09
【图文】：

性质,社交,随机性

性质不满足

性质,编译器

出其中的一个模型，仿真结果被输出在 MC 编译器的结果输出框中，图 4.5 仿真结果上就是建模与仿真的结果。由于建模是考虑到程序中所有的路径，所状态数很多。仿真则只是找出程序中一条可满足的路径，所以可以方程序的执行情况。、性质验证小节通过 MC 编译器对 4.2 节中提出的 3 个性质进行验证。若性质满会给出相关的提示。若不满足，MC 编译器会给出一条反例路径。在入 MSVL 程序和待验证的性质，点击工具栏中的验证按钮即开始验例，在 MC 编译器中输入性质的界面如图 4.6 所示。

【相似文献】