### Skapa referens, olika format (klipp och klistra)

**Harvard**

Pardo Jimenez, R. och Schneider, G. (2017) *Model checking social network models*.

** BibTeX **

@conference{

Pardo Jimenez2017,

author={Pardo Jimenez, Raul and Schneider, Gerardo},

title={Model checking social network models},

booktitle={8th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20-22 September 2017},

pages={238-252},

abstract={A social network service is a platform to build social relations among people sharing similar interests and activities. The underlying structure of a social networks service is the social graph, where nodes represent users and the arcs represent the users' social links and other kind of connections. One important concern in social networks is privacy: what others are (not) allowed to know about us. The "logic of knowledge" (epistemic logic) is thus a good formalism to define, and reason about, privacy policies. In this paper we consider the problem of verifying knowledge properties over social network models (SNMs), that is social graphs enriched with knowledge bases containing the information that the users know. More concretely, our contributions are: i) We prove that the model checking problem for epistemic properties over SNMs is decidable; ii) We prove that a number of properties of knowledge that are sound w.r.t. Kripke models are also sound w.r.t. SNMs; iii) We give a satisfaction-preserving encoding of SNMs into canonical Kripke models, and we also characterise which Kripke models may be translated into SNMs; iv) We show that, for SNMs, the model checking problem is cheaper than the one based on standard Kripke models. Finally, we have developed a proof-of-concept implementation of the model-checking algorithm for SNMs.},

year={2017},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 252754

A1 Pardo Jimenez, Raul

A1 Schneider, Gerardo

T1 Model checking social network models

YR 2017

T2 8th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20-22 September 2017

SP 238

OP 252

AB A social network service is a platform to build social relations among people sharing similar interests and activities. The underlying structure of a social networks service is the social graph, where nodes represent users and the arcs represent the users' social links and other kind of connections. One important concern in social networks is privacy: what others are (not) allowed to know about us. The "logic of knowledge" (epistemic logic) is thus a good formalism to define, and reason about, privacy policies. In this paper we consider the problem of verifying knowledge properties over social network models (SNMs), that is social graphs enriched with knowledge bases containing the information that the users know. More concretely, our contributions are: i) We prove that the model checking problem for epistemic properties over SNMs is decidable; ii) We prove that a number of properties of knowledge that are sound w.r.t. Kripke models are also sound w.r.t. SNMs; iii) We give a satisfaction-preserving encoding of SNMs into canonical Kripke models, and we also characterise which Kripke models may be translated into SNMs; iv) We show that, for SNMs, the model checking problem is cheaper than the one based on standard Kripke models. Finally, we have developed a proof-of-concept implementation of the model-checking algorithm for SNMs.

LA eng

DO 10.4204/EPTCS.256.17

LK http://dx.doi.org/10.4204/EPTCS.256.17

LK http://publications.lib.chalmers.se/records/fulltext/252754/local_252754.pdf

OL 30