社交网络模型的模型检查

社交网络服务是一个在具有相似兴趣和活动的人们之间建立社会关系的平台。社交网络服务的底层结构是社交图，其中节点表示用户，弧表示用户的社会链接和其他类型的连接。社交网络中的一个重要关切是隐私：他人被（不）允许知道关于我们的哪些信息。因此，“知识逻辑”（认知逻辑）是定义和推理隐私策略的良好形式化工具。在本文中，我们考虑在社交网络模型（SNMs）上验证知识性质的问题，即增强了包含用户所知信息的知识库的社交图。更具体地，我们的贡献如下：i) 我们证明 SNMs 上认知性质的模型检查问题是可判定的；ii) 我们证明若干相对于 Kripke 模型可靠的知识性质相对于 SNMs 也是可靠的；iii) 我们给出 SNMs 到标准 Kripke 模型的满足保持编码，并且刻画了哪些 Kripke 模型可翻译为 SNMs；iv) 我们展示对于 SNMs，模型检查问题比基于标准 Kripke 模型的代价更低。最后，我们开发了 SNMs 模型检查算法的概念验证实现。