Formal analysis of DeGroot Influence Problems using probabilistic model checking

DeGroot learning is a model of opinion diffusion and formation in a social network. We examine the behaviour of the DeGroot learning model when external strategic players that aim to influence the opinion formation process are introduced. More specifically, we consider the case of a single decision maker and that of two competing players, with a fixed number of possible influence actions for each of them. In the former case, the DeGroot model takes the form of a Markov Decision Process (MDP), while in the latter case it takes the form of a Stochastic Game (SG). These models are solved using probabilistic model checking techniques, as well as other solution techniques beyond model checking. The viability of our analysis is attested on a well-known social network, the Zachary's karate club. Finally, the evaluation of influence in a social network simultaneously with the decision maker's cost is supported, which is encoded as a multi-objective model checking problem.