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

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