In this section we show how a well-established logic for formal verification can be readily used to specify and reason about properties of BDPs, and in particular their convergence. The logic is the so-called \(\mu\)-calculus. This points to a so-far unexplored interface between fixpoint logics and models of opinion dynamics—like the DeGroot model and propositional opinion diffusion. The section moves some first steps in that direction along the lines of another recent work \cite{JvBoscillations}, where the \(mu\)-calculus, and extensions thereof, have been applied to the study of dynamical systems.
We treat influence graphs as Kripke (multi-relational) models \cite{Seligmanetal:synthese,Christoff_2015}.
We call an influence model a tuple \(\mathcal{M}=\left\langle N,{\bf G},{\bf O}\right\rangle\) where \({\bf G}=(G_{p_{1}},\dots,G_{p_{m}})\) is an influence profile, and \({\bf O}:{\bf P}\longrightarrow 2^{N}\) is an opinion profile over \({\bf P}\), that is, a valuation function.
One can therefore easily interpret a modal language over influence models, where modalities are interpreted on the accessibility relations in \({\bf G}\). That is, to each graph \(G_{p}\) we associate modalities \(\left[p\right]\) and \(\left\langle p\right\rangle\). We will give the details below, but let us immediately note that the class of (possibly infinite) influence graphs would then be characterized by the following properties, for any \(p\in{\bf P}\):
\begin{align} \left[p\right]\varphi\rightarrow\left\langle p\right\rangle\varphi & \\ \left\langle p\right\rangle\varphi\rightarrow\left[p\right]\varphi & \\ \end{align}More precisely, for any influence profile \({\bf G}=(G_{p_{1}},\dots,G_{p_{m}})\), formula \(\left[p_{i}\right]\varphi\rightarrow\left\langle p_{i}\right\rangle\varphi\) (respectively, \(\left\langle p_{i}\right\rangle\varphi\rightarrow\left[p_{i}\right]\varphi\)) is valid in such graph—that is, true in any pointed influence model built on such graph—if and only if each \(G_{p_{i}}\) consists of a serial (respectively, functional) relation.11These are known results from modal correspondence theory (cf. —\cite{Blackburn_2001}—). Put otherwise, on serial and functional graphs the modal box and diamond are equivalent.
The language of the \(\mu\)-calculus expands the basic modal language with a least fixpoint operator \(\mu\). Here is the BNF of the language:
\begin{equation} \mathcal{L}^{\mu}:\varphi::=p\mid\bot\mid\neg\varphi\mid\varphi\land\varphi\mid\left\langle p\right\rangle\varphi\mid\mu p.\varphi(p)\nonumber \\ \end{equation}where \(p\) ranges over \({\bf P}\) and \(\varphi(p)\) indicates that \(p\) occurs free in \(\varphi\) (i.e., it is not bounded by fixpoint operators) and under an even number of negations.22This syntactic restriction guarantees that every formula \(\varphi(p)\) defines a set transformation which preserves \(\subseteq\), which in turn guarantees the existence of least and greatest fixpoints by the Knaster-Tarski fixpoint theorem (cf. —\cite{Stirling_2001}—). In general, the notation \(\varphi(\psi)\) stands for \(\psi\) occurs in \(\varphi\). The usual definitions for Boolean and modal operators apply. Intuitively, \(\mu p.\varphi(p)\) denotes the smallest formula \(p\) such that \(p\leftrightarrow\varphi(p)\). The greatest fixpoint operator \(\nu\) can be defined from \(\mu\) as follows: \(\nu p.\varphi(p):=\neg\mu p.\neg\varphi(\neg p)\).
We interpret \(\mathcal{L}^{\mu}\) on influence models as follows:
Let \(\varphi\in\mathcal{L}^{\mu}\). The satisfaction of \(\varphi\) by a pointed influence model \((\mathcal{M},i)\) is inductively defined as follows:
\begin{align} \mathcal{M},i\not\models\bot & \notag \\ \mathcal{M},i\models p & \Longleftrightarrow i\in{\bf O}(p),\mbox{ for }p\in{\bf P}\notag \\ \mathcal{M},i\models\neg\varphi & \Longleftrightarrow i\not\in\lVert\varphi\rVert_{\mathcal{M}}\notag \\ \mathcal{M},i\models\varphi_{1}\wedge\varphi_{2} & \Longleftrightarrow i\in\lVert\varphi_{1}\rVert_{\mathcal{M}}\cap\lVert\varphi_{2}\rVert_{\mathcal{M}}\notag \\ \mathcal{M},i\models\left\langle p\right\rangle\varphi & \Longleftrightarrow i\in\{j\mid\exists k:jG_{p}k\ \&\ k\in\lVert\varphi\rVert_{\mathcal{M}}\}\notag \\ \mathcal{M},i\models\mu p.\varphi(p) & \Longleftrightarrow i\in\bigcap\{X\in 2^{N}\mid\lVert\varphi\rVert_{\mathcal{M}[p:=X]}\subseteq X\}\notag \\ \end{align}where \(\lVert\varphi\rVert_{\mathcal{M}[p:=X]}\) denotes the truth-set of \(\varphi\) once \({\bf O}(p)\) is set to be \(X\). As usual, we say that: \(\varphi\) is valid in a model \(\mathcal{M}\) iff it is satisfied in all points of \(\mathcal{M}\), i.e., \(\mathcal{M}\models\varphi\); \(\varphi\) is valid in a class of models iff it is valid in all the models in the class.
We list some relevant known results about \(\mathsf{K}^{\mu}\). The logic has a sound and (weakly) complete axiom system \cite{Walukiewicz_2000}. The satisfiability problem of \(\mathsf{K}^{\mu}\) is decidable \cite{Streett_1984}. The complexity of the model-checking problem for \(\mathsf{K}^{\mu}\) is known to be in NP \(\cap\) co-NP \cite{Gr_del_1999}. It is known that the model-checking problem for a formula of size \(m\) and alternation depth \(d\) on a system of size \(n\) can be solved by the natural fixpoint-approximation algorithm with (time) complexity of \(O((m\cdot n)^{d+1})\) \cite{Emerson96}, where the alternation depth of a formula of \(\mathcal{L}^{\mu}\) is the maximum number of \(\mu/\nu\) alternations in a chain of nested fixpoint subformulas.33The reader is referred to, e.g. —\cite{Emerson_2001}—, for the precise definition. Finally, the \(\mu\)-calculus is known to be invariant for bisimulation (cf. \cite{Blackburn_2001}). It actually corresponds to the bisimulation-invariant fragment of monadic second-order logic \cite{Janin_1996}.
Each stream of opinion profiles \({\bf O}^{0},{\bf O}^{1},\ldots,{\bf O}^{n},\ldots\) corresponds to a stream of influence models \(\mathcal{M}^{0},\mathcal{M}^{1},\ldots,\mathcal{M}^{n},\ldots\).
From the point of view of an influence model \(\mathcal{M}=\left\langle N,{\bf G},{\bf O}\right\rangle\) the BDP dynamics of Definition \ref{def:BDP} can therefore be recast in terms of updates of the valuation function \({\bf O}\) as follows:
Base: \({\bf O}^{0}:={\bf O}\)
Step: \({\bf O}^{n+1}(p):=\lVert\left[p\right]p\rVert_{\mathcal{M}^{n}}\).
That is, the interpretation of \(p\) at step \(n+1\) is the interpretation of \(\left[p\right]p\) at step \(n\). Equivalently, the interpretation of \(\neg p\) at step \(n+1\) is the interpretation of \(\left[p\right]\neg p\) at step \(n\).
Let \(\mathcal{M}=\left\langle N,{\bf G},{\bf O}\right\rangle\) be an influence model. The two following statements are equivalent:
\(i\in N\) is stable for \(p\);
The pointed model \((\mathcal{M},i)\) satisfies:44Notice that \(\pm p\) is used as a variable ranging over \(\left\{p,\neg p\right\}\). Technically the above formula is to be read as a scheme for \(\nu x.p\land\left[p\right]x\) and \(\nu x.\pm\neg p\land\left[p\right]x\).
\begin{align} \mathsf{stb}(p):=\nu x.\pm p\land\left[p\right]x\\ \end{align}First of all observe that, by the semantics of the \(\mu\)-calculus, formula \(\mathsf{stb}(p)\) denotes the largest fixpoint of function \(\pm p\land\left[p\right](\cdot)\), that is, formula \(\left[p^{*}\right]\pm p\) where \(\left[p^{*}\right]\) is the modal box interpreted over the reflexive and transitive closure of \(G_{p}\). \(1)\Rightarrow 2)\) Assume that \(i\) is stable for \(p\) and suppose towards a contradiction that \(\mathcal{M},i\not\models\mathsf{stb}(p)\). By what said above, it follows that there exists a \(j\) such that \({\bf O}_{i}(p)\neq{\bf O}_{j}(p)\) which is connected by a finite \(G_{p}\) path to \(i\). By the functionality of influence models and the dynamics of Definition \ref{def:BDP} then at some stage \(n\) in the stream of opinion profiles it should hold that \({\bf O}^{n}_{i}(p)={\bf O}_{j}(p)\), against the assumption that \(i\) be stable for \(p\). \(2)\Rightarrow 1)\) Assume \(\mathcal{M},i\models\mathsf{stb}(p)\). By what said above, this implies that there exists no \(j\) such that \({\bf O}_{i}(p)\neq{\bf O}_{j}(p)\) which is connected by a finite \(G_{p}\) path to \(i\). It follows that in the stream generated by the BDP dynamics \(i\) cannot change its opinion, and hence it is stable. ∎
Let \(\mathcal{M}=\left\langle N,{\bf G},{\bf O}\right\rangle\) be an influence model. The two following statements are equivalent:
\(i\in N\) stabilizes for issue \(p\in{\bf P}\);
The pointed model \((\mathcal{M},i)\) satisfies:
\begin{align} \mu x.\mathsf{stb}(p)\vee\left[p\right]x\\ \end{align}First of all observe that, by the semantics of the \(\mu\)-calculus \(\mu x.\mathsf{stb}(p)\vee\left[p\right]x\) denotes the smallest fixpoint of equation \(x\leftrightarrow\mathsf{stb}(p)\vee\left[p\right]x\). By the Knaster-Tarski theorem and the fact that influence models are finite, we can compute such fixpoint as \(\bigcup_{0\leq n<\omega}\lVert\mathsf{stb}(p)^{n}\rVert\) where \(\lVert\mathsf{stb}(p)^{0}\rVert=\lVert\mathsf{stb}(p)\vee\left[p\right]\bot\rVert\) (notice that \(\left[p\right]\bot\leftrightarrow\bot\) on influence models) and \(\lVert\mathsf{stb}(p)^{n+1}\rVert=\lVert\mathsf{stb}(p)\vee\left[p\right]\mathsf{stb}(p)^{n}\rVert\). So, by Lemma \ref{lemma:stable} \(i\) belongs to \(\lVert\mu x.\mathsf{stb}(p)\vee\left[p\right]x\rVert\) either \(i\) is stable for issue \(p\) or has access in a finite number of steps to a an agent who is stable for \(p\). \(1)\Rightarrow 2)\) Assume that \(i\) stabilizes for issue \(p\in{\bf P}\). So there exists a stage \(n\) in the stream of profiles generated through Definition \ref{def:BDP} at which \({\bf O}_{i}^{n}(p)={\bf O}_{i}^{m}(p)\) for all \(m>n\). By Lemma \ref{lemma:stable}, \(\left\langle N,{\bf G},{\bf O}^{n}\right\rangle,i\models\mathsf{stb}(p)\). It follows that \(i\) is connected through a finite \(G_{p}\)-path to an agent \(j\) such that \(\mathcal{M},j\models\mathsf{stb}(p)\). By what established above we thus have that \(\mathcal{M},i\models\mu x.\mathsf{stb}(p)\vee\left[p\right]x\). \(2)\Rightarrow 1)\) Assume \(\mathcal{M},i\models\mu x.\mathsf{stb}(p)\vee\left[p\right]x\). It follows that \(i\) is connected through a finite \(G_{p}\)-path to an agent \(j\) such that \(\mathcal{M},j\models\mathsf{stb}(p)\). By Lemma \ref{lemma:stable} \(j\) is therefore stable and therefore \(i\) will stabilize for \(p\). ∎
So the formula that expresses the stabilization of the agents’ opinions on one issue is \(\mu x.\left(\nu y.\pm p\land\left[p\right]y\right)\vee\left[p\right]x\). Informally, the theorem states that in a BDP an agent reaches a stable opinion if and only if it has an indirect influencer (linked by an influence path) whose all direct and indirect influencer have the same opinion. Notice that such formula has alternation depth \(0\). So an off-the-shelf model-checking algorithm for the \(\mu\)-calculus can check stabilization in time \(O(m\cdot n)\) with \(n\) being the size of the model and \(m\) the size of the formula.
Now confront this with the earlier Theorem \ref{theorem:mu}. Since the convergence of the BDP is equivalent to the stabilization of all agents on all issues \(p\) (either on \(p\) or \(\neg p\)), we have the following corollary:
The BDP for an opinion profile \({\bf O}\) based on influence graph \({\bf G}\) converges if and only if
\begin{align} \left\langle N,{\bf G},{\bf O}\right\rangle,i\models U\left(\bigwedge_{p\in{\bf P}}\mu x.\mathsf{stb}(p)\vee\left[p\right]x\right)\\ \end{align}for any agent \(i\in N\), where \(U\) denotes the universal modality (cf. \cite{Blackburn_2001}).
So we end up with a natural formalization of the property of convergence for a BDP.