Approximate Simulation-Based Verification of Compatibility of the Friedkin-Johnsen Model with Binary Observations

TL;DR

This paper presents an approximate simulation-based method for verifying if Friedkin-Johnsen opinion models can produce observed binary outputs, using finite abstractions to handle continuous parameters.

Contribution

It introduces a novel abstraction approach that simplifies the influence matrix and parameters, enabling verification of opinion models against binary observations.

Findings

Finite abstractions approximately simulate continuous FJ models.

Verification over abstractions can confirm model consistency with observations.

Numerical experiments demonstrate the effectiveness of the proposed framework.

Abstract

We consider a verification problem for opinion dynamics based on binary observations. The opinion dynamics is governed by a Friedkin-Johnsen (FJ) model, where only a sequence of binary outputs is available instead of the agents' continuous opinions. At every time-step we observe a binarized output for each agent depending on whether the opinion exceeds a fixed threshold. The objective is to verify whether an FJ model with a given set of stubbornness parameters and initial opinions can generate the observed binary outputs up to a small error. The FJ model is formulated as a transition system, and an approximate simulation relation of two transition systems is defined in terms of the proximity of their opinion trajectories and output sequences. We then construct a finite set of abstract FJ models by simplifying the influence matrix and discretizing the stubbornness parameters and the initial opinions. It is shown that the abstraction approximately simulates any concrete FJ model with continuous parameters and initial opinions, and is itself approximately simulated by some concrete FJ model. These results ensure that consistency verification can be performed over the finite abstraction. Specifically, by checking whether an abstract model satisfies the observation constraints, we can conclude whether the corresponding family of concrete FJ models is consistent with the binary observations. Finally, numerical experiments are presented to illustrate the proposed verification framework.