A Process Algebraic Approach to Modeling Collective Behaviors in Social Networks

The properties of social networks, such as concurrency, mobility and distribution, play a negative affect on the modeling and simulation of collective behaviors. This paper presents a process algebraic approach to formal specification and verification of collective behaviors in complex social networks. The social network mainly consists of many collectives, each of which is composed of many agents (or nodes). The agents are described in pi-calculus processes owing to the similarity in attributes between them. The specification of a collective is focused on the internal communication and cooperation among its all agents. Each collective has only one core agent, either a "doer" responsible for bringing behaviors, or "getter" responsible for responding behaviors, which represents the interests of the collective. The interactive behavior between two collectives is simplified into that of a pair of core agents. Finally, we reason and verify the formal systems by the Mobility Workbench (MWB), a model checker of pi-calculus.