近年来随着互联网的蓬勃发展,社交网络已成为各个领域的研究热点,尤其是计算机领域。研究社交网络中个体的社交活动可以充分地了解社交网络结构的变化规律及信息传播规律,这对于促进社交网络的进一步发展具有重要的理论指导意义。社交网络中的个体具有高度的能动性,个体的社交行为具有很强的随机性,如个体关系产生、消亡等。充分研究社交网络中这些随机的特性,可以更好地发掘其中隐藏的、不可直接观测的有用信息。目前,一些模型被用于研究社交网络中的随机性,如马尔可夫链、隐马尔可夫模型(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编译器中进行验证、分析并与其它工具进行对比。