结构平衡理论的时态模型:形式系统与程序实现

Dynamic Social Network Modeling——Axiomatizing and Implementing the Logic of Allies and Enemies

敌友逻辑(van der Hoek, et al., 2018)采用结构平衡理论的视角对社会网络的动态变化进行了刻画。在一个稳定的社会网络中,主体之间没有理由改变当下的关系,而不稳定网络则通常会向稳定网络演进。敌友逻辑基于分支时间逻辑CTL,其中每条时间线表示网络的一个演进过程。本文前半部分探讨敌友逻辑的可靠且完全的公理系统。敌友逻辑的模型检测、有效性和可满足性检测问题的计算复杂性已知都是PSPACE完全的。本文后半部分介绍敌友逻辑模型检测的程序实现。

The Logic of Allies and Enemies(LAE)(van der Hoek, et al., 2018) models the dynamics of social networks from the viewpoint of structural balance theory. A network is stable if all pairs of agents have no reason to change their relationship, and an unstable network evolves over time until eventually reaching a stable state. LAE is a CTL-based temporal logic with every timeline modeling evolution of networks. We axiomatize this logic in the first part of the paper. The model and validity checking problems for LAE is known to be PSPACE-complete. We introduce an LAE model checker in the second part.