Skip to main content

2018 | OriginalPaper | Buchkapitel

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

verfasst von : Xiaobing Wang, Liyuan Ren, Liang Zhao, Xinfeng Shu

Erschienen in: Structured Object-Oriented Formal Language and Method

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In 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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat Zhang, J., Liu, B., Tang, J., et al.: Social influence locality for modeling retweeting behaviors. In: International Joint Conference on Artificial Intelligence, pp. 2761–2767. AAAI Press (2013) Zhang, J., Liu, B., Tang, J., et al.: Social influence locality for modeling retweeting behaviors. In: International Joint Conference on Artificial Intelligence, pp. 2761–2767. AAAI Press (2013)
2.
Zurück zum Zitat Caviglione, L., Coccoli, M., Merlo, A.: Social Network Engineering for Secure Web Data and Services. IGI Global, Hershey (2013)CrossRef Caviglione, L., Coccoli, M., Merlo, A.: Social Network Engineering for Secure Web Data and Services. IGI Global, Hershey (2013)CrossRef
3.
Zurück zum Zitat Ding, J., Cruz, I., Li, C.: A formal model for building a social network. In: IEEE International Conference on Service Operations, Logistics, and Informatics, pp. 237–242. IEEE Press, New York (2011) Ding, J., Cruz, I., Li, C.: A formal model for building a social network. In: IEEE International Conference on Service Operations, Logistics, and Informatics, pp. 237–242. IEEE Press, New York (2011)
5.
Zurück zum Zitat Rabiner, L., Juang, B.: An introduction to hidden Markov models. IEEE ASSP Mag. 3, 4–16 (1986)CrossRef Rabiner, L., Juang, B.: An introduction to hidden Markov models. IEEE ASSP Mag. 3, 4–16 (1986)CrossRef
6.
Zurück zum Zitat Wang, X., Tian, C., Duan, Z., Zhao, L.: MSVL: a typed language for temporal logic programming. Front. Comput. Sci. 11, 762–785 (2017)CrossRef Wang, X., Tian, C., Duan, Z., Zhao, L.: MSVL: a typed language for temporal logic programming. Front. Comput. Sci. 11, 762–785 (2017)CrossRef
7.
Zurück zum Zitat Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inform. 45, 43–78 (2008)MathSciNetCrossRef Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inform. 45, 43–78 (2008)MathSciNetCrossRef
8.
Zurück zum Zitat Tang, J., Chang, Y., Liu, H.: Mining social media with social theories: a survey. In: Applied Computing, Second Asian Applied Computing Conference, pp. 29–31. AACC, Nepal (2004) Tang, J., Chang, Y., Liu, H.: Mining social media with social theories: a survey. In: Applied Computing, Second Asian Applied Computing Conference, pp. 29–31. AACC, Nepal (2004)
9.
Zurück zum Zitat Granovetter, M.: The strength of weak ties. Am. J. Sociol. 78, 1360–1380 (1973)CrossRef Granovetter, M.: The strength of weak ties. Am. J. Sociol. 78, 1360–1380 (1973)CrossRef
10.
Zurück zum Zitat Baier, C., Haverkort, B., Hermanns, H., et al.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29, 524–541 (2003)CrossRef Baier, C., Haverkort, B., Hermanns, H., et al.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29, 524–541 (2003)CrossRef
12.
Zurück zum Zitat Forejt, V., Kwiatkowska, M., Norman, G., et al.: Automated verification techniques for probabilistic systems. In: International School on Formal Methods for the Design of Computer, Communication and Software Systems, pp. 53–113. Advanced Lectures, Bertinoro (2011)CrossRef Forejt, V., Kwiatkowska, M., Norman, G., et al.: Automated verification techniques for probabilistic systems. In: International School on Formal Methods for the Design of Computer, Communication and Software Systems, pp. 53–113. Advanced Lectures, Bertinoro (2011)CrossRef
15.
Zurück zum Zitat Yang, X.: Probabilistic model checking on propositional projection temporal logic. In: IMECS 2011. LNECS, vol. 2188, pp. 242–248 (2011) Yang, X.: Probabilistic model checking on propositional projection temporal logic. In: IMECS 2011. LNECS, vol. 2188, pp. 242–248 (2011)
Metadaten
Titel
A Framework Based on MSVL for Verifying Probabilistic Properties in Social Networks
verfasst von
Xiaobing Wang
Liyuan Ren
Liang Zhao
Xinfeng Shu
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-319-90104-6_9