Reasoning about Parameters in the Friedkin--Johnsen Model from Binary Observations

1. Problem Formulation

The paper addresses a parameter verification problem within the context of social opinion dynamics, specifically using the Friedkin–Johnsen (FJ) model. The core challenge arises from data limitations common in real-world scenarios (e.g., online social networks):

• Observation Constraints: Instead of observing continuous opinion values, the system only provides binary observations (e.g., "favor" vs. "against") at discrete time steps. These are generated by quantizing continuous opinions against a fixed threshold $\gamma$.
• Goal: Given a sequence of binary outputs $\{ \tilde{y}(t) \}_{t=0}^T$, a set of candidate stubbornness parameters, and an estimate of the influence matrix, determine if there exists an FJ model configuration (initial opinions and stubbornness parameters) that is consistent with the observed binary sequence up to a small error tolerance $\kappa$.
• Difficulty: The mapping from continuous states to binary outputs is discontinuous, making standard continuous control or estimation techniques difficult to apply directly. Furthermore, the inverse problem (inferring parameters from limited, discrete data) is ill-posed and computationally complex.

2. Methodology

The authors propose a formal verification framework based on finite abstractions and approximate simulation relations.

A. System Reformulation

The FJ model is reformulated as a discrete-time transition system $T = (X, X_0, \theta, \to, Y, H)$:

• State: Augmented to include both current opinions $x(t)$ and initial opinions $x(0)$ to handle the affine term in the FJ dynamics linearly.
• Dynamics: $x(t+1) = (I - \Lambda)W x(t) + \Lambda x(0)$, where $\Lambda$ is the stubbornness matrix and $W$ is the stochastic influence matrix.
• Output: $y(t) = Q(x(t))$, where $Q$ is a quantization function ($1$ if $x_i \ge \gamma$, else $0$).

B. Finite Abstraction Construction

To make the verification tractable, the authors construct a finite abstraction $T^{ab}$ of the original continuous system:

1. Discretization: The continuous space of initial opinions and stubbornness parameters is discretized into finite sets.
   • Initial opinions are sampled from a grid with resolution $d_x$.
   • Stubbornness parameters are sampled from a grid with resolution $d_\lambda$.
2. Influence Matrix Approximation: The true influence matrix $W$ is approximated by a discrete estimate $W^{ab}$ within a bounded error $\epsilon_w$.
3. Transition Relation: The abstraction uses the same linear dynamics but operates on the discretized state space.

C. Approximate Simulation Relation

A key theoretical contribution is the definition of a $\delta$-approximate simulation relation ($T \preceq_\delta T^{ab}$). Unlike standard simulation which only checks output proximity, this relation enforces:

1. State Proximity: The continuous states of the original system and the abstraction must remain close ($\|x - x^{ab}\| \le \delta\sqrt{n}$).
2. Output Proximity: The binary output sequences must be close in normalized Hamming distance ($\|y - y^{ab}\|_H \le \delta$).

Handling Discontinuity: The authors introduce Assumption 2, which posits that for the duration of observation, most agents' opinions remain sufficiently far from the quantization threshold $\gamma$. This ensures that small state errors do not lead to large output errors (bit flips), allowing the simulation relation to hold.

D. Verification Logic

The verification problem is encoded using Signal Temporal Logic (STL). The consistency requirement is formalized as a temporal formula $\phi_\kappa$, stating that the system's output sequence must remain within Hamming distance $\kappa$ of the observed sequence for all time steps $t \in [0, T]$.

3. Key Contributions

1. Formal Verification Framework for Binary Data: The paper bridges formal methods (model checking) with opinion dynamics, specifically addressing the challenge of inferring parameters from coarse, binary data.
2. Approximate Simulation for Quantized Systems: They define a novel simulation relation that simultaneously bounds state errors and output errors, overcoming the discontinuity of the quantization function.
3. Finite Abstraction Theorem (Theorem 1): They prove that if the discretization is sufficiently fine ($d_x, d_\lambda$ large) and the network estimation error is small, the finite abstraction $\delta$-approximately simulates the original continuous FJ model.
4. Soundness and Completeness Guarantees (Propositions 1 & 2):
   • Soundness (Necessary Condition): If the abstraction fails to satisfy the observation constraints (even with relaxed error $\kappa + \delta$), then the original continuous system cannot satisfy them. This allows for the rejection of inconsistent parameter sets.
   • Completeness (Sufficient Condition): If the abstraction satisfies the constraints (with tightened error $\kappa - \delta$), then there exists a corresponding concrete system that is consistent.
5. Complexity Reduction: The method allows the use of off-the-shelf SMT solvers (like Z3) on finite state spaces, transforming an infinite-dimensional parameter inference problem into a finite model-checking problem.

4. Results and Numerical Experiments

The authors validate the framework through four numerical experiments:

• Convergence of Abstraction: As the discretization resolutions ($d_x, d_\lambda$) increase, the trajectories and output errors of the abstraction converge to those of the original FJ model.
• Robustness to Network Estimation: The framework remains effective even when the influence matrix $W$ is replaced by its expected value (e.g., from a Stochastic Block Model), provided the error $\epsilon_w$ is bounded.
• Solution Space Reduction: The experiments demonstrate how adding constraints (e.g., bounding the distance between estimated and true stubbornness parameters) significantly reduces the number of valid solutions returned by the solver.
• Scalability via Structural Simplification: In a large-scale example ($n=200$), the authors showed that incorporating known structural information (e.g., identifying "stubborn" leaders and community structures) allows for dimensionality reduction. By grouping agents with similar properties, the execution time of the model checker was significantly reduced.

5. Significance

This work is significant for several reasons:

• Realism: It addresses the practical reality that social media data is often binary (likes, upvotes, binary stance) rather than continuous, a gap often ignored in traditional opinion dynamics literature.
• Rigorous Guarantees: Unlike heuristic learning methods, this approach provides mathematical guarantees regarding the consistency of parameters with observations. It avoids false positives by proving that if the abstraction fails, the real system must fail.
• Scalability: By reducing the problem to a finite state space, it makes the verification of complex multi-agent systems computationally feasible using existing formal verification tools.
• Generalizability: The methodology of using approximate simulation relations for systems with discontinuous outputs can be extended to other domains involving quantized observations in control and networked systems.

In summary, the paper provides a rigorous, computationally tractable method to verify whether a specific set of parameters in a social opinion model can explain observed binary behavior, offering a new tool for analyzing limited and discrete social data.