capbtabboxtable[][]

# Knowledge distillation for fast and accurate DNA sequence correction

Anastasiya Belyaeva
Google Research
Joel Shor∗
Verily Life Sciences
Daniel E. Cook
Google Research
Kishwar Shafin
Google Research
Daniel Liu
Google Research
Armin Töpfer
Pacific Biosciences
Aaron M. Wenger
Pacific Biosciences
William J. Rowell
Pacific Biosciences
Howard Yang
Google Research
Alexey Kolesnikov
Google Research
Cory Y. McLean
Google Research
Maria Nattestad
Google Research
Andrew Carroll
Google Research
Pi-Chuan Chang
Google Research
These authors contributed equally.

###### Abstract

Accurate genome sequencing can improve our understanding of biology and the
genetic basis of disease. The standard approach for generating DNA sequences
from PacBio instruments relies on HMM-based models. Here, we introduce
Distilled DeepConsensus - a distilled transformer–encoder model for sequence
correction, which improves upon the HMM-based methods with runtime constraints
in mind. Distilled DeepConsensus is 1.3x faster and 1.5x smaller than its
larger counterpart while improving the yield of high quality reads (Q30) over
the HMM-based method by 1.69x (vs. 1.73x for larger model). With improved
accuracy of genomic sequences, Distilled DeepConsensus improves downstream
applications of genomic sequence analysis such as reducing variant calling
errors by 39% (34% for larger model) and improving genome assembly quality by
3.8% (4.2% for larger model). We show that the representations learned by
Distilled DeepConsensus are similar between faster and slower models.

##  1 Introduction

Genome sequencing is widely used to advance our understanding of biological
processes, the genetic basis of diseases, and is increasingly used for
personalized medicine directly in the clinic [1]. Thus, obtaining accurate
genome sequences is of paramount importance. Over the years, sequencing
platforms have been developed by Illumina, Pacific Biosciences (PacBio), and
Oxford Nanopore, that have had either short and accurate reads or long and
noisy reads. Recently, PacBio developed a novel long read HiFi sequencing
technology [2] that has led to new state-of-the-art performance in variant
calling [3] and the first telomere-to-telomere human assembly [4]. While
highly accurate, some errors still exist and here we focus on whether we can
use machine learning, and in particular transformers, to further improve the
accuracy of the genomic sequences with on-device runtime constraints in mind.

PacBio HiFi sequencing works by circularizing DNA, allowing for multiple
sequencing passes over the same molecule. This produces a set of noisy
sequences/subreads of the same region. The subreads are then combined into a
consensus sequence/read using a hidden Markov model (HMM) [2]. In order to
further improve upon the accuracy of the HMM-based method for correct DNA
sequence generation, DeepConsensus - an encoder-only transformer model has
been developed [5]. However, the accuracy and yield improvements of
DeepConsensus come with latency and model-size costs. For example, unlike
HMMs, transformer models are too large to be run on sequencing platforms with
resource constraints. As sequencing throughput increases, the problem
compounds.

In this work, we use Knowledge Distillation (KD) [6] to improve the runtime of
the transformer-based DeepConsensus model, using techniques similar to [7, 8,
9]. Our model is much smaller and faster than the original model, with slight
performance degradation. Importantly, these runtime boosts are critical for
enabling real time on-sequencing-device inference. In other domains of
biology, as the amount of data increases, such as sequencing millions of
single cells, and model size increases [10], the runtime considerations may
become increasingly important. This work explores initial steps in this
direction and our contributions are as follows:

  1. 1.

We show that knowledge distillation can improve model accuracy, resulting in a
faster model without a significant degradation in performance as compared to a
large model.

  2. 2.

We demonstrate relative performance parity between larger and smaller models
on downstream tasks like variant calling and de novo assembly generation.

  3. 3.

We show that the representations learned by larger and smaller models are
similar.

(a)

(b)

(c)

Figure 1: (a) Overview of the Distilled DeepConsensus model. To train
Distilled DeepConsensus, in addition to the alignment-based loss function we
compute the distillation loss between teacher and student probabilities per
position. (b) Performance versus runtime curve for Distilled DeepConsensus
student models and undistilled models. The performance is calculated relative
to pbccs (HMM-based model). (c) Error profiles of the teacher and distilled
student models.

##  2 Model

DeepConsensus [5] takes as input a tensor of length 100bp containing
information about the subreads such as the noisy subread sequences, strand
direction, pulse width, interpulse duration as well as general information
such as signal-to-noise ratio of each nucleotide and the consensus sequence
given by pbccs HMM-based algorithm (Fig. 1a). The goal is to predict the
correct consensus sequence from the noisy subread sequences and the other
auxiliary information. Since this problem is similar to sequence-to-sequence
tasks, Transformers [11] are leveraged for this problem.

Both the teacher and student models are encoder-only transformers. The teacher
has six encoder stacks. We vary the number of encoder stacks from 3 to 5 to
obtain smaller (student) Distilled DeepConsensus models of different sizes.
Each encoder stack is composed of a self-attention layer with hidden dimension
of 280 and 2 attention heads and a feedforward network with a filter size of
2048. The output of the entire encoder block, which represents the contextual
embedding of each base, is decoded with the feedforward layer followed by a
softmax function, that for each base outputs the probability of A, C, T, G or
a gap. We use this simpler decoder to save computational resources.

For our labels, we leverage a high quality assembly of the human genome
(T2T-CHM13), recently published by the Telomere-to-Telomere consortium [4], as
part of the effort to obtain the complete sequence of the human genome and use
data (2 SMRT Cells) from a CHM13 sample with 24-kb insert sizes from [5].

We use an alignment-based loss function, which is based on differentiable
dynamic programming [12], $L(y,p)$ to train the teacher model as in [5], where
$y=(y_{1},...,y_{m})$ is the true sequence and $p=(p_{1},...,p_{n})$ are the
predicted probabilities with $p_{i}$ representing the probability over A, C,
T, G or a gap classes.

In order to train smaller student models from the teacher, in addition to the
alignment-based loss function, we use a typical knowledge distillation loss
[6], to update the model weights of the student:

$L_{total}=L(y,p^{student})+\alpha L_{KD}(p^{student},p^{teacher}),$ (1)

where $p^{student}$ and $p^{teacher}$ are the probabilities output by the
student and the teacher models, respectively, and $\alpha$ is determined using
a hyper-parameter search. We explore both the Kullback–Leibler (KL) divergence
and the mean squared error (computed per base and averaged across positions)
for $L_{KD}$. In addition, we initialize the student layers from the teacher
layers, since this was found to be beneficial in [7].

##  3 Results

###  3.1 Performance vs. runtime trade-off

We measure the model performance by comparing the yield at empirical Q30
(number of bases in reads with Q30 or higher quality score, i.e. identity of
0.999 or higher) produced by DeepConsensus models versus pbccs. This metric
(yield at empirical Q30 over CCS) indicates how many more high quality bases
we obtain with a particular model as compared to pbccs. The models are trained
on the data collected from CHM13 cell line (chromosomes 1-18, 2 SMRT Cells),
hyper-parameters are optimized using CHM13 cell line (chromosomes 21-22, 2
SMRT Cells), and the models are tested on a completely held-out genome HG002
(chromosome 20, 1 SMRT Cell). Here, we use the KL loss for matching teacher
and student probabilities and initialize the student model from top layers of
the teacher. Model runtime is measured using number of seconds on a Google
Cloud VM with Intel 32 CPU cores (n1-standard-32).

In order to assess whether distillation is useful, we also train student
models of the same size but without the distillation loss, only with
$L(y,p_{student})$. We show that distillation consistently results in improved
yield at empirical Q30 over CCS across different student architectures (3, 4,
5 layers) and replicates (Fig. 1b).

Some student models, for example the 5 layer student model, achieve a similar
yield at empirical Q30 over CCS as the teacher while taking 90% of teacher’s
runtime. For the remaining analysis, we focus on the student model with 4
layers, 1.3x faster and 1.5x smaller (in terms of # parameters) than the
teacher, and slight performance degradation (1.69 vs 1.73) compared to the
teacher.

Figure 2: Distilled DeepConsensus improves variant calling: HG002 (chromosome
20) variant-calling performance of DeepVariant with pbccs, DeepConsensus and
Distilled DeepConsensus reads from 2 SMRT Cells.

Model | Mean QV ($\uparrow$) | Complete (%, $\uparrow$) | Duplicated (%, $\downarrow$)
---|---|---|---
pbccs | 49.8625 | 96.893 | 0.572
Teacher | 51.999 | 97.094 | 0.502
Student | 51.782 | 97.063 | 0.516

Figure 3: Mean quality, gene completeness, and false duplication rates of the
genome assemblies generated with pbccs, DeepConsensus and Distilled
DeepConsensus reads from 2 SMRT Cells.

###  3.2 Teacher versus student error profiles

We analyze whether the teacher and the student make similar kinds of errors.
We quantify the number of base pairs with mismatches, insertions and deletions
per read and additionally subdivide errors by their sequence context. It has
been shown that PacBio HiFi sequencing has higher error rates within
homopolymer (HP) regions [2], which are regions with consecutive repeating
bases (e. g. AAAA), and thus we split indel errors by HP and non-HP context.
Fig. 1c shows that the error types made by the teacher and the student are
similar with HP indels and in particular HP insertions for the student being
the major error type.

###  3.3 Performance on downstream tasks: variant calling and assembly

Variant calling We perform variant calling analysis using a custom DeepVariant
[13] model (warm-started from DeepVariant 1.4) trained on sequences from 2
SMRT Cells generated by DeepConsensus teacher and student models respectively
and evaluated on held-out chromosome 20. For sequences output by pbccs, we use
DeepVariant 1.4 (trained on pbccs output). Fig. 2 shows that the student model
has 39% error reduction in variant calling in comparison to pbccs with the
student being slightly better than the teacher on this task (34% reduction for
larger model).

Assembly analysis Given increased yield and higher quality reads generated by
the DeepConsensus student model and the larger teacher model, we compare the
student and the teacher models in terms of de novo assembly generation. Phased
assemblies were generated with hifiasm assembler using reads (from 2 SMRT
Cells) output by pbccs, and DeepConsensus student and teacher models, similar
to [5]. In Table 1, we report the estimated qualities, using YAK [14], of the
assemblies and show that the mean quality value (across haplotypes) is similar
between the teacher and the student models with both being better than pbccs
(3.8% and 4.2% for student and teacher, respectively). Additionally, both the
teacher and the student models increase assembly gene completeness and
decrease false gene duplication rate.

(a)

(b)

(c)

(d)

Figure 4:  a) Effect of loss choice on distillation. b) Effect of
initialization on distillation. c) Per-example agreement between the teacher,
students with the same hyperparameters but different replicates, and students
with different less optimal hyperparameters (we take the lowest performing
student from Fig. 4b. We measure the probability that model Y is strictly
better (>, equality is omitted and thus probabilities do not add up to 100%)
than model X (in terms of alignment identity) given that model X and Y
disagree on the prediction (edit distance > 0). d) CKA analysis between
student and a replicate (left), showing representations are stable and CKA
between student and teacher (right), showing representations are similar.

##  4 Analysis

We performed a study of distillation training options to evaluate which
factors contributed the most to good performance in the student models. We
experimented with three distillation losses: alignment to ground truth and
Kullback Leibler (KL) divergence with the teacher probabilities, alignment to
ground truth and MSE with the teacher probabilities, and just KL with the
teacher probabilities. Additionally, we experimented with four types of
initialization schemes. The relative benefits of each can be seen in Fig. 4a
and b. We found that MSE outperformed KL divergence, and that initializing the
student network to "alternating" layers (1, 2, 4, 6 of the teacher) performed
best among layer initialization schemes.

Fig. 4c shows a per-example agreement analysis [15] to better understand
whether models with better overall performances are just correctly predicting
more examples, or if they’re correctly predicting different examples. The
results show that the better models are more accurate only slightly more than
the worse models when there is a disagreement. This means that the set of
examples correctly predicted by the better models is a larger and different
set than the set of examples correctly predicted by the worse models, but
neither is as a superset of the other.

To test whether teachers and students learn the same representations, we apply
linear Centered Kernel Alignment (CKA) between pairs of layers across
networks, following the methodology of [16]. CKA computes a [0, 1]-valued
similarity between two Gram matrices computed from two representations over
the same sample of input examples [17]. We see from the student vs. student
plot (Fig. 4d, left) that the internal representations of the student model
are very stable across different replicates. In the teacher vs. student plot
(Fig. 4d, right), we find that layers in the student network correspond well
with particular layers in the teacher. Interestingly, we find that despite
initializing with top layers from the teacher ($1\rightarrow 1,2\rightarrow
2,4\rightarrow 3,6\rightarrow 4$), the student layers after training have a
different correspondence ($1\rightarrow 1,2$ or $4\rightarrow 2,4\rightarrow
3,6\rightarrow 4$). This representational difference might also explain why
the multiheaded attention of the student is different than the teacher: for
example for layer 3, the student attention head looks an average of 1.8 base
pairs different than the teacher for layer 4.

## References

  * [1] J. E. Gorzynski, S. D. Goenka, K. Shafin, T. D. Jensen, D. G. Fisk, M. E. Grove, E. Spiteri, T. Pesout, J. Monlong, G. Baid _et al._ , “Ultrarapid nanopore genome sequencing in a critical care setting,” _New England Journal of Medicine_ , vol. 386, no. 7, pp. 700–702, 2022.
  * [2] A. M. Wenger, P. Peluso, W. J. Rowell, P.-C. Chang, R. J. Hall, G. T. Concepcion, J. Ebler, A. Fungtammasan, A. Kolesnikov, N. D. Olson _et al._ , “Accurate circular consensus long-read sequencing improves variant detection and assembly of a human genome,” _Nature biotechnology_ , vol. 37, no. 10, pp. 1155–1162, 2019.
  * [3] N. D. Olson, J. Wagner, J. McDaniel, S. H. Stephens, S. T. Westreich, A. G. Prasanna, E. Johanson, E. Boja, E. J. Maier, O. Serang _et al._ , “Precisionfda truth challenge v2: Calling variants from short and long reads in difficult-to-map regions,” _Cell Genomics_ , vol. 2, no. 5, p. 100129, 2022.
  * [4] S. Nurk, S. Koren, A. Rhie, M. Rautiainen, A. V. Bzikadze, A. Mikheenko, M. R. Vollger, N. Altemose, L. Uralsky, A. Gershman _et al._ , “The complete sequence of a human genome,” _Science_ , vol. 376, no. 6588, pp. 44–53, 2022\.
  * [5] G. Baid, D. E. Cook, K. Shafin, T. Yun, F. Llinares-López, Q. Berthet, A. Belyaeva, A. Töpfer, A. M. Wenger, W. J. Rowell _et al._ , “Deepconsensus improves the accuracy of sequences with a gap-aware sequence transformer,” _Nature Biotechnology_ , pp. 1–7, 2022.
  * [6] G. Hinton, O. Vinyals, J. Dean _et al._ , “Distilling the knowledge in a neural network,” _arXiv preprint arXiv:1503.02531_ , vol. 2, no. 7, 2015\.
  * [7] V. Sanh, L. Debut, J. Chaumond, and T. Wolf, “Distilbert, a distilled version of bert: smaller, faster, cheaper and lighter,” _arXiv preprint arXiv:1910.01108_ , 2019.
  * [8] X. Jiao, Y. Yin, L. Shang, X. Jiang, X. Chen, L. Li, F. Wang, and Q. Liu, “Tinybert: Distilling bert for natural language understanding,” _arXiv preprint arXiv:1909.10351_ , 2019.
  * [9] Z. Sun, H. Yu, X. Song, R. Liu, Y. Yang, and D. Zhou, “Mobilebert: a compact task-agnostic bert for resource-limited devices,” _arXiv preprint arXiv:2004.02984_ , 2020.
  * [10] Ž. Avsec, V. Agarwal, D. Visentin, J. R. Ledsam, A. Grabska-Barwinska, K. R. Taylor, Y. Assael, J. Jumper, P. Kohli, and D. R. Kelley, “Effective gene expression prediction from sequence by integrating long-range interactions,” _Nature methods_ , vol. 18, no. 10, pp. 1196–1203, 2021.
  * [11] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin, “Attention is all you need,” _Advances in neural information processing systems_ , vol. 30, 2017.
  * [12] A. Mensch and M. Blondel, “Differentiable dynamic programming for structured prediction and attention,” in _International Conference on Machine Learning_. PMLR, 2018, pp. 3462–3471.
  * [13] R. Poplin, P.-C. Chang, D. Alexander, S. Schwartz, T. Colthurst, A. Ku, D. Newburger, J. Dijamco, N. Nguyen, P. T. Afshar _et al._ , “A universal snp and small-indel variant caller using deep neural networks,” _Nature biotechnology_ , vol. 36, no. 10, pp. 983–987, 2018.
  * [14] H. Cheng, G. T. Concepcion, X. Feng, H. Zhang, and H. Li, “Haplotype-resolved de novo assembly using phased assembly graphs with hifiasm,” _Nature methods_ , vol. 18, no. 2, pp. 170–175, 2021.
  * [15] J. Shor, A. Jansen, W. Han, D. S. Park, and Y. Zhang, “Universal paralinguistic speech representations using self-supervised conformers,” _ICASSP 2022 - 2022 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_ , pp. 3169–3173, 2022.
  * [16] M. Raghu, T. Unterthiner, S. Kornblith, C. Zhang, and A. Dosovitskiy, “Do vision transformers see like convolutional neural networks?” _Advances in Neural Information Processing Systems_ , vol. 34, pp. 12 116–12 128, 2021\.
  * [17] S. Kornblith, M. Norouzi, H. Lee, and G. Hinton, “Similarity of neural network representations revisited,” in _International Conference on Machine Learning_. PMLR, 2019, pp. 3519–3529.


# Comparing Social Network Dynamic Operators

Edoardo Baccini  University of Groningen
<EMAIL_ADDRESS>University of Groningen
Zoé Christoff  University of Groningen
<EMAIL_ADDRESS>
###### Abstract

Numerous logics have been developed to reason either about threshold-induced
opinion diffusion in a network, or about similarity-driven network structure
evolution, or about both. In this paper, we first introduce a logic containing
different dynamic operators to capture changes that are ‘asynchronous’
(opinion change only, network-link change only) and changes that are
‘synchronous’ (both at the same time). Second, we show that synchronous
operators cannot, in general, be replaced by asynchronous operators and vice
versa. Third, we characterise the class of models on which the synchronous
operator _can_ be reduced to sequences of asynchronous operators.

##  1 Introduction

There are two main types of change affecting agents connected through a social
network. First, the features of an agent, e.g., their opinions or behavior,
can be influenced by its neighbors in the network: for instance, if one’s
entire social circle has adopted an opinion in favor of (or against) vaccines,
one is unlikely to disagree with this opinion. Under this type of social
influence, or social conformity pressure, network-neighbors tend to align
their opinions (or any other feature that can change) and therefore become
more similar. Second, in addition to changing their own state (opinion, or
other feature), agents can also reshape their social environment by connecting
with others. What generally drives the formation of new links between two
agents is their similarity. Both types of changes relate to how similar agents
are: social influence makes network neighbors become more similar while new
links make similar agents become more connected [10, Ch. 4].

In social network analysis, a common way of representing both types of
dynamics is to assume that certain _thresholds_ drive the dynamics. On the one
hand, a typical way of representing social influence is via threshold models
[13, 18, 9, 10]: agents adopt a feature when a large enough proportion of
their network neighbors has already adopted it. On the other hand, the
formation of new links has been modelled in a similar way. In probabilistic
models, it is usual to assume that agents who are more similar are more likely
to connect than those who are less similar [24, 5]. In deterministic models,
this has been translated by a similarity threshold: two agents get connected
as soon as they are similar enough [19, 21, 20, 22].

Both types of changes have been addressed in logic. Indeed, a number of
logical frameworks has flourished to reason about threshold-based social
influence [3, 7, 6, 17, 15], and about threshold-based link formation [19, 21,
20, 22]. Yet, to the exception of [12, 16, 2], either the two aspects have
been treated separately [23, 19, 21, 20, 22, 11], or the two types of changes
have been taken to happen one after the other [20]. To our knowledge, only [2]
provides a logic capturing specifically _simultaneous_ changes of the network
structure and the state of the agents.

In this paper, we introduce a closely related framework that, similarly to [2]
combines three dynamic operators: one corresponding to the change of the
network structure only, one corresponding to the change of the agents feature
(opinion/behavior/state) only, and one corresponding to _both changes at the
same time_ , but restricting ourselves to monotonic changes. We then tackle
for this monotonic setting an open question by [20, 2] in the literature: Can
different sequences of dynamic operators be reduced to one another?

We first introduce the framework in Section 2. We then discuss the
(ir)replaceability of the three dynamic operators in Section 3. We show in
particular that our ‘synchronous’ operator cannot always be replaced by any
sequences of other operators (Theorem 2). We also show that, when it can be
replaced, the sequence of operators replacing it can only be of four specific
types (Theorem 3). Finally, we characterize the class of models on which the
synchronous operator can be replaced (Theorem 4).

##  2 Logic of asynchronous and synchronous network changes

We introduce a logic to reason about asynchronous and synchronous changes in
social networks. We use a propositional language (where atoms are parametrized
by our sets of agents and features) extended with three dynamic operators
$\triangle,\square,\bigcirc$, to capture, respectively, diffusion update,
network update, and both updates happening simultaneously.

######  Definition 1 (Syntax $\mathcal{L}$).

Let $\mathcal{A}$ be a non-empty finite set of agents, $\mathcal{F}$ be a non-
empty finite set of features. Let
$\Phi_{at}:=\\{N_{ab}:a,b\in{\mathcal{A}}\\}\cup\\{f_{a}:f\in{\mathcal{F}},a\in{\mathcal{A}}\\}$
be the set of atomic formulas. The syntax $\mathcal{L}$ is the following:

$\varphi:=\ N_{ab}\ |\ f_{a}\ |\ \neg{\varphi}\ |\ \varphi\wedge{\varphi}\ |\
\triangle{\varphi}|\ \square{\varphi}\ |\ \bigcirc{\varphi}$

where $f\in{\mathcal{F}}$ and $a,b\in\mathcal{A}$.

The connectors $\lor$, $\rightarrow$ and $\leftrightarrow$ are defined as
usual. $N_{ab}$ is read as ‘agent $a$ is an influencer of agent $b$’; $f_{a}$
as ‘agent $a$ has feature $f$’; $\triangle\varphi$ as ‘after a diffusion
update, $\varphi$ holds’; $\square\varphi$ as ‘after a network update,
$\varphi$ holds’; $\bigcirc\varphi$ as ‘after a synchronous update, $\varphi$
holds’.

We now introduce the models representing who is influencing whom and who has
which features, and our three different types of updates.

######  Definition 2 (Model $M$).

Let $\mathcal{A}$ be a non-empty finite set of agents, $\mathcal{F}$ be a non-
empty finite set of features. A model $M$ over $\mathcal{A}$ and $\mathcal{F}$
is a tuple $\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle$, where:

  * •

$\mathcal{N}\subseteq{\mathcal{A}\times{\mathcal{A}}}$ is a social influence
relation;

  * •

$\mathcal{V}:\mathcal{A}\longrightarrow{\mathcal{P}(\mathcal{F})}$ is a
valuation function, assigning to each agent a set of adopted features;

  * •

${\omega,\tau\in\mathbb{Q}}$ are two rational numbers such that
${0\leq{\omega}\leq{1}}$ and ${0<{\tau}\leq{1}}$, interpreted, respectively,
as similarity threshold and influenceability threshold.

We write $C^{\omega\tau}$ for the class of all models for given values of
$\omega$ and $\tau$.

We turn to defining the three types of model updates corresponding to our
three dynamic operators. First, after the diffusion (only) update, the set of
features each agent adopt is updated. Agents might start adopting new features
if enough of their neighbors had already adopted them before the update. Note
that, while [20, 2] consider updates in which agents might start abandoning
previously adopted features, here we restrict ourselves to the case in which
agents are not allowed to start unadopting features, similarly as in [3].

######  Definition 3 (Diffusion update - $M_{\triangle}$).

Given a model ${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$, the
updated model
${M_{\triangle}=\langle{\mathcal{N},\mathcal{V^{\prime}},\omega,\tau}\rangle}$
is such that for any $a,b\in\mathcal{A}$ and any $f\in\mathcal{F}$:

$f\in\mathcal{V}^{\prime}(a)\textrm{ iff
}\left\\{\begin{array}[]{lr}f\in{\mathcal{V}(a)},&\text{ if }N(a)=\emptyset\\\
f\in{\mathcal{V}(a)}\textrm{ or
}\frac{|N_{f}(a)|}{|N(a)|}\geq{\tau},&\text{otherwise}\end{array}\right\\}$

where $N_{f}(a):=\\{b\in{A}:(b,a)\in{\mathcal{N}}\text{ and
}f\in{\mathcal{V}(b)}\\}$ and $N(a):=\\{b\in{A}:(b,a)\in{\mathcal{N}}\\}$.

The diffusion update does not affect the network structure. In contrast, the
network update only affects the connections, not the features adopted by any
of the agents. After a network update, new links may have formed between
agents that agree on sufficiently many features. Just as agents could not
unadopt previously adopted features, agents cannot break old connections,
which differs for instance from [16, 20]. In this respect, our network update
is a monotonic version of that in [20].

######  Definition 4 (Network update - $M_{\square}$).

Given a model ${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$, the
updated model
${M_{\square}=\langle{\mathcal{N^{\prime}},\mathcal{V},\omega,\tau}\rangle}$
is such that for any $a,b\in\mathcal{A}$ and any $f\in\mathcal{F}$:

$(a,b)\in\mathcal{N}^{\prime}\textrm{ iff }(a,b)\in\mathcal{N}\textrm{ or
}\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))|}}{|\mathcal{F}|}\geq{\omega}$

Third, the synchronous update affects features and connections at once.
Adoption of new features happens under the same conditions as with the
diffusion update, and new links are created under the same conditions as with
the network update.

######  Definition 5 (Synchronous update - $M_{\bigcirc}$).

Let ${M={\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}}$, the model
resulting from synchronous update is
${M_{\bigcirc}:=\langle{\mathcal{N}^{\prime},\mathcal{V^{\prime}},\omega,\tau}\rangle}$,
where $\mathcal{N}^{\prime}$ is as in Definition 4 and $\mathcal{V}^{\prime}$
is as in Definition 3.

Now that we have defined the model-updates, we can introduce the semantic
clauses for formulas containing the corresponding operators.

######  Definition 6 (Satisfaction).

For any model $M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle$ and any
formula $\varphi\in\mathcal{L}$, the truth of $\varphi$ in $M$ is inductively
defined as follows:

  * $M\models{f_{a}}$ if and only if $f\in{\mathcal{V}(a)}$

  * $M\models{N_{ab}}$ if and only if $(a,b)\in{\mathcal{N}}$

  * $M\models{\neg\varphi}$ if and only if $M\not\models{\varphi}$

  * $M\models{\varphi\wedge\psi}$ if and only if $M\models\varphi$ and $M\models{\psi}$

  * $M\models{\square\varphi}$ if and only if $M_{\square}\models{\varphi}$

  * $M\models{\triangle\varphi}$ if and only if $M_{\triangle}\models{\varphi}$

  * $M\models{\bigcirc\varphi}$ if and only if $M_{\bigcirc}\models{\varphi}$

where $M_{\triangle}$ is the updated model as in Definition 3, and
$M_{\square}$ is the updated model as in Definition 4, and $M_{\bigcirc}$ is
the updated model as in Definition 5.

As usual, we say that a formula is valid in a class of models if it is true in
all models of that class and valid (tout court) if it is valid in all models.

######  Observation 1.

Let $M_{1}=\langle{\mathcal{N}_{1},\mathcal{V}_{1},\omega,\tau}\rangle$ and
$M_{2}=\langle{\mathcal{N}_{2},\mathcal{V}_{2},\omega,\tau}\rangle$ be two
models. The following are equivalent:

  * •

for all $\varphi_{at}\in\Phi_{at}$, $M_{1}\models\varphi_{at}$ iff
$M_{2}\models\varphi_{at}$

  * •

for all $\varphi\in\mathcal{L}$, $M_{1}\models\varphi$ iff
$M_{2}\models\varphi$

  * •

$M_{1}=M_{2}$

We introduce the following two abbreviations capturing, respectively, when an
agent $a$ has sufficient pressure to adopt a feature ($f^{\tau}_{N(a)}$), and
when two agents $a$ and $b$ have sufficient similarity to connect
($sim^{\omega}_{ab}$).

$f^{\tau}_{N(a)}:={\bigvee_{\\{G\subseteq{N}\subseteq{A},\textrm{
}N\neq{\emptyset}\textrm{
}:\frac{|G|}{|N|}\geq{\tau}\\}}(\bigwedge_{b\in{N}}N_{ba}\wedge\bigwedge_{b\not\in{N}}\neg{N_{ba}}\wedge\bigwedge_{b\in{G}}f_{b})}$

${sim^{\omega}_{ab}:=\bigvee_{\\{E\subseteq{\mathcal{F}}:\frac{|E|}{|\mathcal{F}|}\geq{\omega}\\}}\bigwedge_{f\in{E}}(f_{a}\leftrightarrow{f_{b}})}$

These abbreviations can then be used to obtain reduction axioms for each of
the dynamic modalities in $\mathcal{L}$, which are shown in Table 1. The
reduction axioms for the dynamic operators in $\mathcal{L}$ are very similar
to those in other dynamic logics of social network change. Indeed, the
reduction axioms for the operator $\triangle$ are the same as the those of the
dynamic operator $[adopt]$ in [3], with the exception that our logic captures
multiple diffusing features and thus contains reduction axioms for each
spreading feature in $\mathcal{F}$. In this sense, they resemble the reduction
axioms in [20] with the difference that in our setting features cannot be
unadopted. Moreover, the reduction axioms for the operator $\square$ are
similar to those in [20], with the difference that our framework does not
allow for link deletion. The reduction axioms for the operator $\bigcirc$
merely reflect the fact that both features and links are affected by a
synchronous update.

We will investigate how and when operators can replace one another in the next
section. Before that, by looking at our axioms, we can immediately observe
that an operator can replace another when it precedes specific formulas:

######  Observation 2.

Let ${M={\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}}$ be a model.
For all $a,b\in\mathcal{A}$, for all $f\in\mathcal{F}$:

  * •

$M\models\bigcirc f_{a}$ iff $M\models\triangle f_{a}$

  * •

if $M\models\square f_{a}$, then $M\models\bigcirc f_{a}$

  * •

$M\models\bigcirc N_{ab}$ iff $M\models\square N_{ab}$

  * •

if $M\models\triangle N_{ab}$ then $M\models\bigcirc N_{ab}$

$\square{N_{ab}}\leftrightarrow{N_{ab}\lor{sim^{\omega}_{ab}}}$ | $\triangle{N_{ab}}\leftrightarrow{N_{ab}}$ | $\bigcirc{N_{ab}}\leftrightarrow{N_{ab}\lor{sim^{\omega}_{ab}}}$
---|---|---
$\square{f_{a}}\leftrightarrow{f_{a}}$ | $\triangle{f_{a}}\leftrightarrow{f_{a}\lor{f^{\tau}_{N(a)}}}$ | $\bigcirc{f_{a}}\leftrightarrow{f_{a}\lor{f^{\tau}_{N(a)}}}$
${\square(\varphi\wedge{\psi})}\leftrightarrow{\square{\varphi}\wedge{\square{\psi}}}$ | ${\triangle(\varphi\wedge{\psi})}\leftrightarrow{\triangle{\varphi}\wedge{\triangle{\psi}}}$ | ${\bigcirc(\varphi\wedge{\psi})}\leftrightarrow{\bigcirc{\varphi}\wedge{\bigcirc{\psi}}}$
$\square{\neg{\varphi}}\leftrightarrow{\neg{\square{\varphi}}}$ | $\triangle{\neg{\varphi}}\leftrightarrow{\neg{\triangle{\varphi}}}$ | $\bigcirc{\neg{\varphi}}\leftrightarrow{\neg{\bigcirc{\varphi}}}$
From $\varphi_{1}\leftrightarrow\varphi_{2}$, infer that
$\varphi\leftrightarrow\varphi[\varphi_{1}/\varphi_{2}]$, where
$\varphi[\varphi_{1}/\varphi_{2}]$ is a formula
obtained by replacing one or more occurrences of $\varphi_{1}$ with
$\varphi_{2}$
Table 1: Reduction Axioms and derivation rule for the dynamic modalities
$\square,\triangle,\bigcirc$.

######  Definition 7 (Logic $L^{\omega\tau}$ ).

Let $\omega\in{[0,1]}$ and $\tau\in(0,1]$ be two rational numbers. The Logic
$L^{\omega\tau}$ consists of some complete axiomatisation and derivation rules
of propositional logic, together with the reduction axioms and the derivation
rule in Table 1.

######  Theorem 1.

Let $\omega\in{[0,1]}$ and $\tau\in(0,1]$ be two rational numbers. For any
$\varphi\in\mathcal{L}$: $\models_{\mathcal{C}^{\omega\tau}}\varphi\textrm{
iff }\vdash_{L^{\omega\tau}}\varphi\ $

The proof uses standard techniques and is very similar to that of the related
settings in [3, 20, 2]: a sketch is included in the Appendix.

##  3 Irreplaceability of synchronous operators

Given that our dynamic formulas are reducible to the static fragment of our
language, the question of comparing the expressivity of fragments of our
language excluding one or two of the dynamic operators is uninteresting. In
contrast, what is interesting, as suggested already in [20, 2], is to compare
whether formulas containing some (specific combinations of) dynamic operators
could be translated into formulas containing other (combinations of) dynamic
operators. Another way to put it, closer to the way [20] first introduces the
question, is to ask when different sequences of different model updates result
in the same model.

To be able to investigate the extent to which our dynamic operators are inter-
translatable or not (beyond the atomic preceding cases mentioned in
Observation 2), we first have to introduce some notation and define the
relevant type of expressivity criteria.

######  Definition 8 (Notation for sequences of operators).

Let $D=\\{\bigcirc,\triangle,\square\\}$. For $O\subseteq{D}$, $S_{O}$ denotes
the set of all non-empty finite sequences of operators in $O$. We write
$d_{1}d_{2}...d_{n}$ for the sequence $\langle{d_{1},d_{2},...,d_{n}}\rangle$
and $d^{n}$ for the sequence consisting of $n\in\mathbb{N}$ repetitions of
$d\in D$. We denote by $s^{j:k}$ the subsequence of $s$ starting with the
$j$-th element of $s$ and ending with the $k$-th element of $s$. Given two
sequences $s_{1},s_{2}$ of lengths $n,m\in\mathbb{N}$, respectively, we write
$s_{1}s_{2}$ for the sequence of length $n+m$ obtained by prefixing $s_{1}$ to
$s_{2}$.

######  Definition 9 (Equivalence of sequences).

Two sequences $s_{1},s_{2}\in{S_{D}}$ are equivalent on a model $M$ when
$M_{s_{1}}=M_{s_{2}}$, or, equivalently (by Observation 1), when for all
$\varphi\in\mathcal{L}$, $M\models{s_{1}}\varphi$ if and only if
$M\models{s_{2}}\varphi$. Two sequences $s_{1}$ and $s_{2}$ are equivalent
over a class of models when they are equivalent over all models in the class.
Two sequences are equivalent (tout court) when they are equivalent over the
class of all models.

We start by making some observations about sequences of $\triangle$ and
$\square$ operators.

######  Observation 3.

Let a model ${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be
given.

  * •

Any sequence $s\in{S_{\\{\square\\}}}$ is equivalent to the sequence $\square$
on $M$.

  * •

There exists an $n<{|\mathcal{A}|}$, such that, for any $m>n$, $\triangle^{m}$
is equivalent to $\triangle^{n}$ on $M$.

The first point follows from the fact that the model update in Definition 4 is
idempotent, and therefore $M\models\square^{n}\varphi$ if and only if
$M\models\square\varphi$. A proof of the second point can be found in [3].

We then lift this notion of equivalence between sequences to an existential
notion between sets of sequences, so that we can compare the different dynamic
fragments of our language.

######  Definition 10 (Replaceability of sets).

Let $S_{1},S_{2}\subseteq{S_{D}}$ be two sets of sequences. The set $S_{1}$ is
replaceable with the set $S_{2}$ in a model $M$, when, for all sequences
$s_{1}\in{S_{1}}$, there exists a sequence $s_{2}\in{S_{2}}$ that is
equivalent to $s_{1}$ in $M$. $S_{1}$ is replaceable with $S_{2}$ over a class
of model when it is repleaceable with $S_{2}$ in all models of the class.
$S_{1}$ is replaceable with $S_{2}$ (tout court) when it is repleaceble with
$S_{2}$ over the class of all models.

When comparing our dynamic operators, it is easy to see that
$S_{\\{\square\\}}$ (and therefore any superset of it) is not replaceable by
$S_{\\{\triangle\\}}$ and, vice versa, that $S_{\\{\triangle\\}}$ (and
therefore any superset of it) is not replaceable by $S_{\\{\square\\}}$ and
similarly for $S_{\\{\square\\}}$ and $S_{\\{\bigcirc\\}}$, and
$S_{\\{\triangle\\}}$ and $S_{\\{\bigcirc\\}}$, which implies that
$S_{\\{\square,\triangle\\}}$ is not replaceable with $S_{\\{\bigcirc\\}}$.
The only interesting question is: can we replace our synchronous operator?

######  Theorem 2.

$S_{\\{\bigcirc\\}}$ is not replaceable with $S_{\\{\square,\triangle\\}}$.

Figure 1: The figure represents the model $M$, and its model updates
$M_{\bigcirc}$, $M_{\triangle}$, $M_{\square}$, $M_{\triangle\square}$,
$M_{\square\triangle}$ considered in Theorem 2. The model $M$ is as follows:
$\mathcal{A}=\\{a,b,c\\}$, $\mathcal{F}=\\{f,g,h\\}$,
$\omega=\tau=\frac{1}{2}$. For each model, each agent is represented as a
node, and the influence of one agent on another agent is represented as a
directed arrow from the influencing node to the influenced node. Next to each
node, all and only the features in $\mathcal{F}$ that an agent possess are
reported.

###### Proof.

We show that there is no sequence in $S_{\\{\triangle,\square\\}}$ that is
equivalent to the sequence $\bigcirc$ on all models. Assume, towards a
contradiction that there exists a sequence $s\in{S_{\\{\triangle,\square\\}}}$
equivalent to $\bigcirc$ in the model $M$ given in Fig. 1. Let
$n\in{\mathbb{N}}$ be the length of $s$. One of two cases must hold:

  * [Case 1: $s$ starts with $\triangle$.] We can rewrite $s$ as $\triangle{s^{2:n}}$. From Fig.1, we know that $M\not\models\triangle{{{N_{ac}}}}$, whereas $M\models\bigcirc{{{N_{ac}}}}$ and therefore $s\neq\triangle$. Note that $M$ is such that any number of successive triangles reduce to one: for any $\varphi$, $M\models\triangle\varphi$ iff $M\models\triangle{s^{\prime}}\varphi$ for every ${s^{\prime}}\in{S_{\\{\triangle\\}}}$. Since $M\not\models\triangle{{{N_{ac}}}}$, then $M\not\models\triangle{s^{\prime}}{N_{ac}}$, for every ${s^{\prime}}\in{S_{\\{\triangle\\}}}$. Thus, $s\not\in{S_{\\{\triangle\\}}}$. The sequence $s$ must therefore contain at least one $\square$, and can be rewritten as ${s^{1:m}\square{s^{(m+2):n}}}$ where $s^{1:m}\in{S_{\\{\triangle\\}}}$, with $1\leq{m}<n$. Given that, as mentioned above, all triangles can be reduced to one, for all $\varphi\in{\mathcal{L}}$, $M\models{{s^{1:m}\square{s^{(m+2):n}}}\varphi}$ iff $M\models{{\triangle\square{s^{(m+2):n}}}\varphi}$. As illustrated in Figure 1, $M\not\models{{\triangle\square}N_{ac}}$. Furthermore, note that $M\models{{\triangle\square}\varphi}$ iff $M\models{{\triangle\square}s^{\prime}\varphi}$ for all $s^{\prime}\in S_{\\{\triangle,\square\\}}$, i.e., $M_{\triangle\square}$ is stable. Hence, $M\not\models{{\triangle\square}s^{\prime}{N_{ac}}}$ for all $s^{\prime}\in S_{\\{\triangle,\square\\}}$. Thus, in particular: $M\not\models{{\triangle\square}s^{(m+2):n}{N_{ac}}}$. Hence, using again the fact that the number of initial triangles is irrelevant, $M\not\models{s^{1:m}\square{s^{(m+2):n}}}{N_{ac}}$ which is $M\not\models{s}{N_{ac}}$. But $M\models{\bigcirc}{N_{ac}}$, and hence $s$ is not equivalent to $\bigcirc$ in $M$.

  * [Case 2: $s$ starts with $\square$.] $s$ is of the kind ${\square{s^{2:n}}}$. As illustrated in Fig.1, $M\not\models\square{{{g_{a}}}}$, whereas $M\models\bigcirc{{{g_{a}}}}$. Note that $M$ is such that $M\models{{\square}\varphi}$ iff $M\models{{\square}s^{\prime}\varphi}$ for all $s^{\prime}\in S_{\\{\square,\triangle\\}}$. Hence, $M\not\models{{\square}s^{\prime}{g_{a}}}$ for all $s^{\prime}\in S_{\\{\square,\triangle\\}}$. Thus, $M\not\models{{\square}s^{2:n}{g_{a}}}$ which is the same as $M\not\models{s{g_{a}}}$. Hence, $s$ is not equivalent to $\bigcirc$ in $M$.

Hence, in both cases, $s$ is not equivalent to $\bigcirc$ in $M$.
Contradiction. Thus, there is no sequence in $S_{\\{\triangle,\square\\}}$
equivalent to $\bigcirc$, which implies that $S_{\\{\bigcirc\\}}$ is not
replaceable by $S_{\\{\triangle,\square\\}}$.

∎

From the proof of Theorem 2, we know that there is no sequence in
$S_{\\{\square,\triangle\\}}$ that is equivalent to $\bigcirc$ in the class of
_all_ models. However, we will show in Proposition 1 that there are classes of
models on which $\bigcirc$ does have equivalent sequences in
$S_{\\{\triangle,\square\\}}$. We first need to introduce the following
additional abbreviations, where we already name $\psi_{s}$ the formula that
captures the conditions under which $\bigcirc$ is equivalent to $s$.

######  Definition 11 (Abbreviations $\psi_{\triangle}$, $\psi_{\square}$,
$\psi_{\triangle\square}$ and $\psi_{\square\triangle^{n}}$ ).

  * •

$\psi_{\triangle}:=\bigwedge_{a,b\in\mathcal{A}}(N_{ab}\lor\neg
sim^{\omega}_{ab})$

  * •

$\psi_{\square}:=\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in F}(f_{a}\lor\neg
f^{\tau}_{N(a)})$

  * •

$\psi_{\triangle\square}:=\bigwedge_{{a,b}\in\mathcal{A}}(\neg{N_{ab}}\rightarrow({sim^{\omega}_{ab}}\leftrightarrow\triangle{{sim^{\omega}_{ab}})})$

  * •

For all $n>0$:
$\psi_{\square\triangle^{n}}:=\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in{F}}(\neg{f_{a}}\rightarrow({f^{\tau}_{N(a)}}\leftrightarrow\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})})$

We can now show that these formulas indeed define four classes of models in
which $\bigcirc$ has an equivalent sequence in $S_{\\{\triangle\square\\}}$:

######  Proposition 1.

Let $M$ be a model. $\bigcirc$ is equivalent on $M$ to:

  * •

$\triangle$ iff $M\models\psi_{\triangle}$

  * •

$\square$ iff $M\models\psi_{\square}$

  * •

$\triangle\square$ iff $M\models\psi_{\triangle\square}$

  * •

$\square\triangle^{n}$ iff $M\models\psi_{\square\triangle^{n}}$, for $n>0$

For space reasons, the proof of Proposition 1 is provided in the Appendix.

We can now show that if $\bigcirc$ has an equivalent sequence in
$S_{\\{\triangle\square\\}}$ on some model, then that sequence has to be
equivalent to one of those in Proposition 1 on that model. To prove this, we
need the following lemmas.

######  Lemma 1.

Let $M$ be a model and $s\in{S_{D}}$. If $s$ starts with a subsequence of the
form $\triangle^{n}$ for some $n>0$ and $s$ is equivalent to $\bigcirc$ on
$M$, then $\triangle^{n}$ is equivalent to $\triangle$ on $M$.

###### Proof.

Consider a sequence $s\in{S_{D}}$ such that $s$ starts with a subsequence of
the kind $\triangle^{n}$, for some $n>0$, and $s$ is equivalent to $\bigcirc$
on model ${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$. Two cases:
either $n=1$, or $n>1$. If $n=1$, the claim is trivially true since
$\triangle$ is equivalent to itself. Assume now that $n>1$. Assume also,
towards a contradiction, that $\triangle^{n}$ is not equivalent to $\triangle$
on $M$. By Def. 9, it follows that $M_{\triangle}\neq M_{\triangle^{n}}$. By
Obs. 1, it follows that $M_{\triangle}$ and $M_{\triangle^{n}}$ must differ on
whether they satisfy some atomic proposition. By Def. 3 and Def. 4, since
features can never be abandoned, we know that, for all $a\in\mathcal{A}$ for
all $f\in\mathcal{F}$, if $M\models\triangle f_{a}$, then $M\models\triangle
s^{\prime}f_{a}$ for all $s^{\prime}\in{S_{D}}$; with a similar reasoning,
from Def. 3 and Def. 4, since diffusion updates do not alter the network
structure, we also know that for all $a,b\in\mathcal{A}$, $M\models\triangle
N_{ab}$ iff $M\models\triangle^{n}N_{ab}$. These observations, together with
the fact that $M_{\triangle^{n}}$ and the model $M_{\triangle}$ must differ on
the satisfaction of some atomic proposition, imply that there are
$a\in\mathcal{A}$ and $f\in\mathcal{F}$ such that $M\models\triangle^{n}f_{a}$
and $M\not\models\triangle f_{a}$. From Obs. 2, we know that, for all
$a\in\mathcal{A}$ for all $f\in\mathcal{F}$, $M\models\triangle f_{a}$ iff
$M\models\bigcirc{f_{a}}$. Since $M\not\models\triangle f_{a}$, we can infer
that $M\not\models\bigcirc f_{a}$. At the same time, from the fact that
features can never be abandoned, and the fact that
$M\models\triangle^{n}f_{a}$, it follows that $M\models sf_{a}$, since
$\triangle^{n}$ is the initial subsequence of $s$. Therefore, it must be the
case that both $M\not\models\bigcirc f_{a}$ and that $M\models sf_{a}$. This
contradicts the initial assumption that $s$ and $\bigcirc$ are equivalent on
$M$. Therefore, for all $n\geq 1$, $\triangle^{n}$ must be equivalent to
$\triangle$ on $M$. ∎

######  Lemma 2.

Let $M$ be a a model and
$s\in{S_{\\{\triangle,\square\\}}\setminus(S_{\\{\triangle\\}}\cup{S_{\\{\square\\}}})}$.
If $s$ starts with $\triangle$ and is equivalent to $\bigcirc$ on $M$, then
$s$ is equivalent to $\triangle\square$ on $M$.

###### Proof.

Consider any
$s\in{S_{\\{\triangle,\square\\}}\setminus(S_{\\{\triangle\\}}}\cup{S_{\\{\square\\}}})$,
such that $s$ starts with $\triangle$ and is equivalent to $\bigcirc$ on some
model ${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$. Assume,
towards contradiction, that $s$ is not equivalent to $\triangle\square$ on
$M$. By Lemma 1, we know that if $s$ starts with a sequence of the kind
$\triangle^{n}$, then $\triangle^{n}$ must be equivalent to $\triangle$ on
$M$. For this reason, we can restrict ourselves to consider the case in which
$s$ starts with the subsequence $\triangle\square$. Since $s$ is not
equivalent to $\triangle\square$ on $M$, by Obs.1, it follows that $M_{s}$ and
$M_{\triangle\square}$ must differ on whether they satisfy some atomic
proposition. From Obs. 2, we know that, for all $a\in\mathcal{A}$ for all
$f\in\mathcal{F}$, $M\models\triangle f_{a}$ iff $M\models\bigcirc{f_{a}}$.
From this and the fact that the network update does not affect the features of
the agent, we know that $M\models\triangle\square f_{a}$ iff
$M\models\bigcirc{f_{a}}$, for all $a\in\mathcal{A}$ for all
$f\in\mathcal{F}$. This, combined with the fact that $s$ is equivalent to
$\bigcirc$, implies that $M\models\bigcirc{f_{a}}$ iff $M\models sf_{a}$, and
hence, that $M\models\triangle\square f_{a}$ iff $M\models sf_{a}$, for all
$a\in\mathcal{A}$ and $f\in\mathcal{F}$. Since by Obs.1, we know that $M_{s}$
and $M_{\triangle\square}$ must differ on whether they satisfy some atomic
proposition, it follows that there are $a,b$ such that either: (i)
$M\not\models s{N_{ab}}$ and $M\models\triangle\square{N_{ab}}$ or (ii)
$M\models s{N_{ab}}$ and $M\not\models\triangle\square{N_{ab}}$. Assume that
(i) is the case. If $M\models\triangle\square{N_{ab}}$, then from the Def. 3
and Def. 4, it follows that $M\models\triangle\square s^{\prime}{N_{ab}}$ for
all $s^{\prime}\in S_{D}$, since links cannot be deleted. This fact, together
with the fact that $\square\triangle$ is a subsequence of $s$, implies in
particular that $M\models sN_{ab}$. This contradicts the fact that
$M\not\models s{N_{ab}}$. Therefore (ii) must be the case, i.e. $M\models
s{N_{ab}}$ and $M\not\models\triangle\square{N_{ab}}$. By the assumption that
$s$ is equivalent to $\bigcirc$ it follows that $M\models{\bigcirc N_{ab}}$.
Now, by the reduction axioms and the fact that
$M\not\models\triangle\square{N_{ab}}$, we know that $M\not\models N_{ab}$ and
$M\not\models\triangle{sim^{\omega}_{ab}}$. Since
$M\not\models\triangle{sim^{\omega}_{ab}}$ but $M\models{sN_{ab}}$, there must
$m\in\mathbb{N}$ smaller than the length $n$ of the sequence $s$, such that
$M\models s^{1:m}sim^{\omega}_{ab}$: in other words, it must be the case that
at some point of the sequence $s$, the agents $a,b$ have become similar. The
fact that $M\models s^{1:m}sim^{\omega}_{ab}$ holds implies that there exist
at least one $f\in{\mathcal{F}}$ and a $1<j\leq{m}$ such that either
$M\models{s^{1:j}f_{a}}$ and $M\not\models{s^{1:i}f_{a}}$ for all $i<{j}$, or
$M\models{s^{1:j}f_{b}}$ and $M\not\models{s^{1:i}f_{b}}$ for all $i<{j}$:
this simply means that in order to become similar, at least one among $a$ or
$b$ must have acquired at least one new feature that makes them similar at
some point in the update sequence expressed by $s$. W.l.o.g. consider the case
in which it is $a$ that has acquired a new feature, i.e. that there exist
$f\in{\mathcal{F}}$ and a $1<j\leq{m}$ such that $M\models{s^{1:j}f_{a}}$ and
$M\not\models{s^{1:i}f_{a}}$ for all $i<{j}$. From the fact that features are
never abandoned, $M\models sf_{a}$. Since $M\models sf_{a}$, and, by
assumption $s$ is equivalent to $\bigcirc$ on $M$, it follows that
$M\models\bigcirc{f_{a}}$. Since, by assumption $s$ starts with $\triangle$,
and it is the case that $M\not\models{s^{1:i}f_{a}}$ for all $i<{j}$, we know
that $M\not\models\triangle{f_{a}}$ (triangle is the first operator in $s$).
It follows that both $M\models\bigcirc{f_{a}}$ and
$M\not\models\triangle{f_{a}}$ are true. By Obs. 2, we know that for all
$a\in\mathcal{A}$ for all $f\in\mathcal{F}$, $M\models\bigcirc{f_{a}}$ iff
$M\models\triangle{f_{a}}$. Contradiction. Therefore, there is no sequence
$s\in{S_{\\{\triangle,\square\\}}\setminus(S_{\\{\triangle\\}}}\cup{S_{\\{\square\\}}})$,
such that $s$ starts with $\triangle$, is equivalent to $\bigcirc$ on $M$, and
is not equivalent to $\triangle\square$ on $M$.

∎

######  Lemma 3.

Let $M$ be a model and
$s\in{S_{\\{\triangle,\square\\}}\setminus(S_{\\{\triangle\\}}}\cup
S_{\\{\square\\}})$. If $s$ starts with $\square$ and is equivalent to
$\bigcirc$ on $M$, then $s$ is equivalent to a sequence in the set
$\\{\square\triangle^{n}:n>0\\}$.

###### Proof.

Let a model ${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be
given. Assume that
$s\in{S_{\\{\triangle,\square\\}}\setminus(S_{\\{\triangle\\}}}\cup{S_{\\{\square\\}}})$
starts with $\square$ and is equivalent to $\bigcirc$ on $M$, and that $s$ is
not equivalent to any sequence in the set $\\{\square\triangle^{n}:n>0\\}$ on
$M$. From the fact that any sequence $s^{\prime}\in{S_{\\{\square\\}}}$ is
equivalent to the sequence $\square$, it follows that, if $s$ starts with a
subsequence of the kind $\square^{n}$ before the first occurrence of a
$\triangle$, then $s$ is equivalent on $M$ to a sequence that starts with a
single $\square$ followed by the subsequence of $s$ starting at the first
occurrence of a $\triangle$ and ending with the last operator of $s$. In other
words, it is sufficient to consider the case in which $s$ starts with a
subsequence of the kind $\square\triangle$. From this, and the fact that
$s\in{S_{\\{\triangle,\square\\}}\setminus(S_{\\{\triangle\\}}}\cup{S_{\\{\square\\}}})$
and $s\not\in\\{\square\triangle^{n}:n>0\\}$, $s$ must be such that at some
point of the subsequence of $s$ starting with the third operator of $s$, at
least another $\square$ occurs in it. Furthermore, at least one such
$\square$, must be such that $s$ is not equivalent on $M$ to the sequence $s$
without that $\square$. Otherwise, $s$ would be equivalent to a sequence with
no further elements of the kind $\square$ after the initial subsequence
$\square\triangle$, and hence would be a sequence in the set
$\\{\square\triangle^{n}:n>0\\}$. From this, it follows that there must be a
subsequence $s^{1:m}$ of $s$, with $m\leq{n}$, with $n$ the length of the
sequence $s$, where the $m$-th element is a $\square$, such that for some
$a,b\in\mathcal{A}$, $M\models{s^{1:m}N_{ab}}$, and for all $j<{m}$,
$M\not\models{s^{1:j}N_{ab}}$. Observe that $\square$ is a subsequence of
$s^{1:m}$. Therefore, $M\not\models\square{N_{ab}}$. By the fact that
$M\models{s^{1:m}N_{ab}}$, and since ${s^{1:m}}$ is a subsequence of $s$, and
connections between agents cannot be abandoned by Def. 4, it follows that
$M\models{sN_{ab}}$. By the assumption that $s$ and $\bigcirc$ are equivalent,
it follows that $M\models{sN_{ab}}$. By Obs. 2, we know that for all
$a,b\in\mathcal{A}$, $M\models\bigcirc N_{ab}$ iff $M\models\square N_{ab}$.
This contradicts the previous claim that $M\not\models\square{N_{ab}}$.
Therefore there is no sequence
$s\in{S_{\\{\triangle,\square\\}}\setminus(S_{\\{\triangle\\}}}\cup{S_{\\{\square\\}}})$
that starts with $\square$, is equivalent to $\bigcirc$ on $M$, and is not
equivalent to any sequence in the set $\\{\square\triangle^{n}:n>0\\}$ on $M$.
∎

We can now combine the above lemmas to prove the following theorem.

######  Theorem 3.

Let $M$ be a model and $s\in S_{\\{\square,\triangle\\}}$. If $s$ is
equivalent to $\bigcirc$ on $M$, then $s$ is equivalent to a sequence in the
set
$\\{\square,\triangle,\triangle\square\\}\cup\\{\square\triangle^{n}:n>0\\}$
on $M$.

###### Proof.

Consider an arbitrary model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$, and an arbitrary
sequence in $s\in{S_{\\{\square,\triangle\\}}}$ equivalent to $\bigcirc$ on
$M$. One of three cases must hold: $s\in{S_{\\{\square\\}}}$,
$s\in{S_{\\{\triangle\\}}}$,
$s\in{S_{\\{\triangle,\square\\}}}\setminus({S_{\\{\square\\}}}\cup{S_{\\{\triangle\\}}})$.
[Case 1: $s\in{S_{\\{\square\\}}}$.] Since the model update in Def. 4 is
idempotent, any sequence $s^{\prime}\in{S_{\\{\square\\}}}$ is equivalent to
the sequence $\square$. This implies that $s$ is equivalent to $\square$ on
$M$. [Case 2: $s\in{S_{\\{\triangle\\}}}$.] Then, trivially, $s$ starts with a
subsequence of the form $\triangle^{n}$ for some $n>0$. From Lemma 1, we know
that $s$ is equivalent to $\triangle$ on $M$. [Case 3:
$s\in{S_{\\{\triangle,\square\\}}}\setminus({S_{\\{\square\\}}}\cup{S_{\\{\triangle\\}}})$.]
If $s$ starts with a $\triangle$, we know by Lemma 2 that $s$ is equivalent to
$\triangle\square$ on $M$. If $s$ starts with a $\square$, by Lemma 3, we know
that $s$ is equivalent on $M$ to a sequence in the set
$\\{\square,\triangle,\triangle\square\\}\cup\\{\square\triangle^{n}:n>0\\}$.
From this, it follows that if $s$ is equivalent to $\bigcirc$ on some model
$M$, then $s$ is equivalent on $M$ to a sequence in the set
$\\{\square,\triangle,\triangle\square\\}\cup\\{\square\triangle^{n}:n>0\\}$.

∎

Using Observation 3, Proposition 1 and Theorem 3, we can now characterise the
class of models on which $\bigcirc$ can be replaced by
$S_{\\{\triangle,\square\\}}$.

######  Theorem 4.

$\bigcirc$ is replaceable by $S_{\\{\triangle,\square\\}}$ on a model $M$ iff
$M\models\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}$.

###### Proof.

Consider an arbitrary model $M$.

[$\Rightarrow$] Assume that $\bigcirc$ is replaceable with
$S_{\\{\triangle,\square\\}}$ on $M$: there exists a sequence $s\in
S_{\\{\triangle,\square\\}}$ equivalent to $\bigcirc$ on $M$. By Theorem 3, we
know that $s$ is equivalent to a sequence
$s^{\prime}\in\\{\square,\triangle,\triangle\square\\}\cup\\{\square\triangle^{n}:n>0\\}$.
We distinguish four cases: (i) $s$ is equivalent to $\triangle$ on $M$, (ii)
$s$ is equivalent to $\square$ on $M$; (iii) $s$ is equivalent to
$\triangle\square$ on $M$; (iv) $s$ is equivalent to a sequence in
$\\{\square\triangle^{n}:n>0\\}$ on $M$. Assume that (i). By the first point
in Prop. 1, we know that $M\models\psi_{\triangle}$. From this, it follows
that
$M\models{\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$
for any $n$. Assume that (ii) is the case; by the second point in Prop. 1, and
the fact that $s$ is equivalent to $\square$ on $M$, we know that $s$ is
equivalent to $\bigcirc$ on $M$ iff $M\models\psi_{\square}$. From this, it
follows that
$M\models{\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$
for any $n$. Assume that (iii) is the case; by the third point in Prop. 1, and
the fact that $s$ is equivalent to $\triangle\square$ on $M$, we know that $s$
is equivalent to $\bigcirc$ on $M$ iff $M\models\psi_{\triangle\square}$. From
this, it follows that
$M\models{\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$
for any $n$. Assume that (iv) is the case, and assume that $s$ is equivalent
to a sequence of the kind $\square\triangle^{n}$ on $M$, for arbitrary $n>0$.
By Obs. 3, we know that for all sequences $\square\triangle^{n}$ with
$n\geq|\mathcal{A}|$, there exist an equivalent sequence
$\square\triangle^{m}$ on $M$ such that $m<|\mathcal{A}|$. We therefore
consider the case in which $n<|\mathcal{A}|$: in this case, by the fourth
point in Prop. 1, it then follows that $s$ is equivalent to $\bigcirc$ on $M$
iff $M\models\psi_{\square\triangle^{n}}$. From this, it follows that
$M\models{\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$.
Since $n>0$ was arbitrary, this holds for all $n>0$ in $\mathbb{N}$.

[$\Leftarrow$] Assume that
$M\models{\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$.
Therefore, one of the following four cases must hold: (i)
$M\models\psi_{\triangle}$; (ii) $M\models\psi_{\square}$; (iii)
$M\models\psi_{\triangle\square}$; (iv)
$M\models{\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$. (i)
Assume that $M\models\psi_{\triangle}$. By Prop. 1, we know that this holds
iff $\triangle$ is equivalent to $\bigcirc$ on $M$. In this case, we take $s$
to be $\triangle$. (ii) Assume that $M\models\psi_{\square}$. By Prop. 1, we
know that this holds iff $\square$ is equivalent to $\bigcirc$ on $M$. In this
case, we take $s$ to be $\square$. (iii) Assume that
$M\models\psi_{\triangle\square}$. By Prop. 1, we know that this holds iff
$\triangle\square$ is equivalent to $\bigcirc$ on $M$. In this case, we take
$s$ to be $\triangle\square$. (iv) Assume that
$M\models{\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$.
Therefore there is an $n<|\mathcal{A}|$, such that
$M\models{\psi_{\square\triangle^{n}}}$.By Prop. 1, we know that this holds
iff $\square\triangle^{n}$ is equivalent to $\bigcirc$ on $M$. In this case,
we take $s$ to be $\square\triangle^{n}$.

Since in all cases (i)-(iv), we can find a sequence $s\in
S_{\\{\triangle,\square\\}}$ equivalent to $\bigcirc$ on $M$, we have proven
that, if
$M\models{\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}}$,
$\bigcirc$ is replaceable with $S_{\\{\triangle,\square\\}}$ on $M$.

∎

Informally, Theorem 4 tells us that a sequence $s$ without synchronous
operators can replace a synchronous operator only under one of the following
circumstances: no agent has social pressure to adopt new features ($s$ is
equivalent to $\square$); no agent is similar to any disconnected agent ($s$
is equivalent to $\triangle$); conforming to social pressure preserves
similarity with disconnected agents ($s$ is equivalent to $\triangle\square$);
creating new connections with similar agents does not forbid conforming to old
social pressures ($s$ is equivalent to a sequence in
$\\{\square\triangle^{n}:n>0\\}$).

######  Proposition 2.

Let $M$ be a model. If
$M\models\bigwedge_{0\leq{i}\leq(m-1)}\bigcirc^{i}({\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}})$,
then $\bigcirc^{m}$ is replaceable by $S_{\\{\triangle,\square\\}}$ on $M$.

###### Proof.

Assume
$M\models\bigwedge_{0\leq{i}\leq(m-1)}\bigcirc^{i}({\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}})$.
Then, for all $i\geq 0\leq(m-1)$:
$M_{\bigcirc^{i}}\models\psi_{\triangle}\lor\psi_{\square}\lor\psi_{\triangle\square}\lor\bigvee_{0\leq{n}<{|\mathcal{A}}|}\psi_{\square\triangle^{n}}$,
and therefore, by Theorem 4, $\bigcirc$ is replaceable by
$S_{\\{\triangle,\square\\}}$ on $M_{\bigcirc^{i}}$. Let $s_{i}$ be a sequence
that replaces $\bigcirc$ on $M_{\bigcirc^{i}}$. Then the sequence
$s_{0}...s_{i}...s_{m-1}$ replaces $\bigcirc^{m}$ on $M$.

∎

##  4 Conclusion

We have introduced a logical framework containing dynamic operators to reason
about asynchronous as well as synchronous threshold-induced monotonic changes
in social networks. We showed that, in general, our synchronous operator
cannot be replaced (Theorem 2), and that, on the models on which it can be
replaced, only sequences of four specific types can replace it (Theorem 3).
Finally, we characterised the class of models on which the synchronous
operator can be replaced (Theorem 4).

The two most natural continuations of this work would be, first, to
characterise the models on which sequences of (more than one) synchronous
operators can be replaced, and, second, to study the replaceability of
synchronous operators in the non-monotonic frameworks from [20, 2].

Furthermore, it would be interesting to study the replaceability of richer
operators studied in epistemic/doxastic settings such as [3, 19, 17, 15, 11],
for instance the network announcements in [17, 15, 11] or the message passing
updates in [11]. In this direction, we could compare which models different
updates can reach, as done in [4, 3]. In particular, it would be interesting
to investigate what types of group knowledge are reachable by different social
network dynamic updates.

## Acknowledgments

Zoé Christoff acknowledges support from the project Social Networks and
Democracy (VENI project number Vl.Veni.201F.032) financed by the Netherlands
Organisation for Scientific Research (NWO).

## References

  * [1]
  * [2] Edoardo Baccini, Zoé Christoff & Rineke Verbrugge (2022): _Opinion diffusion in similarity-driven networks_.  In: Logic and the Foundations of Game and Decision Theory (LOFT 14).
  * [3] Alexandru Baltag, Zoé Christoff, Rasmus Kræmmer Rendsvig & Sonja Smets (2018): _Dynamic epistemic logic of diffusion and prediction is social networks_.  Studia Logica 107, 10.1007/s11225-018-9804-x.
  * [4] Alexandru Baltag & Sonja Smets (2013): _Protocols for belief merge: Reaching agreement via communication_.  Logic Journal of IGPL 21(3), pp. 468–487, 10.1093/jigpal/jzs049.
  * [5] Yann Bramoullé, Sergio Currarini, Matthew O. Jackson, Paolo Pin & Brian W. Rogers (2012): _Homophily and long-run integration in social networks_.  Journal of Economic Theory 147(5), pp. 1754–1786, 10.1016/j.jet.2012.05.007.
  * [6] Zoé Christoff & Jens Ulrik Hansen (2015): _A logic for diffusion in social networks_.  Journal of Applied Logic 13(1), pp. 48–77, 10.1016/j.jal.2014.11.011.
  * [7] Zoé Christoff & Pavel Naumov (2019): _Diffusion in social networks with recalcitrant agents_.  Journal of Logic and Computation 29(1), pp. 53–70, 10.1093/logcom/exy037.
  * [8] Hans van Ditmarsch, Wiebe van der Hoek & Barteld Kooi (2007): _Dynamic Epistemic Logic_.  Synthese Library Series, Springer, 10.1007/978-1-4020-5839-4.
  * [9] Peter Dodds & Duncan J. Watts (2011): _Threshold models of social influence_.  In: The Oxford Handbook of Analytical Sociology, Oxford University Press, 10.1093/oxfordhb/9780199215362.013.20.
  * [10] David Easley & Jon Kleinberg (2010): _Networks, Crowds, and Markets: Reasoning About a Highly Connected World_.  Cambridge University Press, New York, USA, 10.1017/CBO9780511761942.
  * [11] Saúl Fernández González (2022): _Change in social networks: Some dynamic extensions of Social Epistemic Logic_.  Journal of Logic and Computation 32(6), pp. 1212–1233, 10.1093/logcom/exac024.
  * [12] Patrick Girard, Jeremy Seligman & Fenrong Liu (2012): _General dynamic dynamic logic_.  In Thomas Bolander, Torben Brauner, Silvio Ghilardi & Lawrence Moss, editors: Advances in Modal Logic, Volume 9, College Publication, pp. 239–260.
  * [13] Mark Granovetter (1978): _Threshold models of collective behavior_.  American Journal of Sociology 83(6), pp. 1420–1443, 10.1086/226707.
  * [14] Barteld Kooi (2007): _Expressivity and completeness for public update logics via reduction axioms_.  Journal of Applied Non-Classical Logics 17(2), pp. 231–253, 10.3166/jancl.17.231-253.
  * [15] Fenrong Liu, Jeremy Seligman & Patrick Girard (2014): _Logical dynamics of belief change in the community_.  Synthese 191(11), pp. 2403–2431, 10.1007/s11229-014-0432-3.
  * [16] Truls Pedersen & Marija Slavkovik (2017): _Formal models of conflicting social influence_.  In Bo An, Ana Bazzan, João Leite, Serena Villata & Leendert van der Torre, editors: PRIMA 2017: Principles and Practice of Multi-Agent Systems, Springer International Publishing, Cham, pp. 349–365, 10.1007/978-3-319-69131-2_21.
  * [17] Jeremy Seligman, Fenrong Liu & Patrick Girard (2011): _Logic in the community_.  In Mohua Banerjee & Anil Seth, editors: Logic and Its Applications, Lecture Notes in Computer Science 6521, Springer, pp. 178–188, 10.1007/978-3-642-18026-2_15.
  * [18] Pramesh Singh, Sameet Sreenivason, Boleslaw K. Szymanski & Gyorgy Korniss (2013): _Threshold-limited spreading in social networks with multiple initiators_.  Scientific Reports 3(2330), 10.1038/srep02330.
  * [19] Sonja Smets & Fernando R. Velázquez-Quesada (2017): _How to make friends: A logical approach to social group creation_.  In Alexandru Baltag, Jeremy Seligman & Tomoyuki Yamada, editors: Logic, Rationality, and Interaction, Springer, Berlin, Heidelberg, pp. 377–390, 10.1007/978-3-662-55665-8_26.
  * [20] Sonja Smets & Fernando R. Velázquez-Quesada (2020): _A logical analysis of the interplay between social influence and friendship selection_.  In Luís Soares Barbosa & Alexandru Baltag, editors: Dynamic Logic. New Trends and Applications, Springer International Publishing, Cham, pp. 71–87, 10.1007/978-3-030-38808-9_5.
  * [21] Sonja Smets & Fernando R. Velázquez-Quesada (2019): _A logical study of group-size based social network creation_.  Journal of Logical and Algebraic Methods in Programming 106, pp. 117–140, 10.1016/j.jlamp.2019.05.003.
  * [22] Sonja Smets & Fernando R. Velázquez-Quesada (2020): _A closeness- and priority-based logical study of social network creation_.  Journal of Logic, Language and Information 29(1), pp. 21–51, 10.1007/s10849-019-09311-5.
  * [23] Anthia Solaki, Zoi Terzopoulou & Bonan Zhao (2016): _Logic of closeness revision_.  ESSLLI 2016 Student Session, p. 123\.
  * [24] Szymon Talaga & Andrzej Nowak (2020): _Homophily as a process generating social networks: Insights from social distance attachment model_.  Journal of Artificial Societies and Social Simulation 23(2), 10.18564/jasss.4252.

## Appendix

### Proof sketch of Theorem 1

###### Proof.

The proof uses standard methods.

[Soundness] The soundness of the reduction axioms for the dynamic operators
$\triangle,\square,\bigcirc$ follows from the fact that they spell out the
model updates in Def. 3, Def. 4 and Def. 5 respectively. The soundness of the
axioms $\triangle N_{ab}\leftrightarrow N_{ab}$ and $\square
f_{a}\leftrightarrow f_{a}$ follows from the fact that the model update
$M_{\triangle}$ does not alter the connections between agents (Def. 3), and
the fact that, respectively, the model update $M_{\square}$ does not alter the
features of the agents (Def. 4). The soundness of the axioms $\triangle
f_{a}\leftrightarrow f_{a}\lor f^{\tau}_{N(a)}$ can be shown as in [3]: by
Def. 5, the soundness of the axiom $\bigcirc f_{a}\leftrightarrow f_{a}\lor
f^{\tau}_{N(a)}$ is shown in the same way.

As an example, we prove the validity of $\square N_{ab}\leftrightarrow
N_{ab}\lor sim^{\omega}_{ab}$.

Consider a model ${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$.
$M\models\square N_{ab}$ iff, by Def. 6, $M_{\square}\models N_{ab}$ iff, by
Def. 4 either $(a,b)\in\mathcal{N}$, or
$\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))|}}{|\mathcal{F}|}\geq{\omega}$.

This holds iff $M\models{N_{ab}}$ or
$\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))|}}{|\mathcal{F}|}\geq{\omega}$.

We now show that
$\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))|}}{|\mathcal{F}|}\geq{\omega}$
iff $M\models sim^{\omega}_{ab}$.

[$\Rightarrow$] If
$\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))|}}{|\mathcal{F}|}\geq{\omega}$,
there exist a subset $E\subseteq\mathcal{F}$, namely the set
$(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}}))$
such that for all $f\in{E}$, $M\models f_{a}\leftrightarrow f_{b}$ (indeed the
set
$(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))}$
contains by definition all and only those features that either both agents
have or that both do not have). This in turn implies that
$M\models\bigvee_{\\{E\subseteq{\mathcal{F}}:\frac{|E|}{|\mathcal{F}|}\geq{\omega}\\}}\bigwedge_{f\in{E}}(f_{a}\leftrightarrow{f_{b}})$.
Thus, $M\models{sim^{\omega}_{ab}}$.

[$\Leftarrow$] Now, assume that $M\models{sim^{\omega}_{ab}}$. This holds iff
$M\models\bigvee_{\\{E\subseteq{\mathcal{F}}:\frac{|E|}{|\mathcal{F}|}\geq{\omega}\\}}\bigwedge_{f\in{E}}(f_{a}\leftrightarrow{f_{b}})$.
This means that there exist a subset $E\subseteq\mathcal{F}$, such that
$\frac{|E|}{|\mathcal{F}|}\geq\omega$, and such that for all $f\in E$,
$M\models f_{a}\leftrightarrow f_{b}$, i.e. $f\in V(a)$ iff $f\in V(b)$. From
this, it is clear that $E$ must be a subset of
$(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))}$.
From this and the fact that $\frac{|E|}{|\mathcal{F}|}\geq\omega$, we can
conclude that
$\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))}|}{|\mathcal{F}|}\geq\omega$.

We thus proved that
$\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))|}}{|\mathcal{F}|}\geq{\omega}$
iff $M\models sim^{\omega}_{ab}$. From above we know that $M\models\square
N_{ab}$ iff $M\models f_{a}$ or
$\frac{|(\mathcal{V}(a)\cap\mathcal{V}(b))\cup(\mathcal{F}\setminus({\mathcal{V}(a)}\cup{{\mathcal{V}(b)}))|}}{|\mathcal{F}|}\geq{\omega}$.
We can therefore conclude that $M\models\square N_{ab}$ iff $M\models f_{a}$
or $M\models sim^{\omega}_{ab}$.

The soundness of the axiom $\bigcirc N_{ab}\leftrightarrow N_{ab}\lor
sim^{\omega}_{ab}$ is proven in the same way. As usual, the soundness of the
distributivity of the dynamic operators over conjunction and the clauses for
negation can be proven by induction on the length of formulas. Finally,
validity preservation of the inference rule in Table 1 can be shown by
induction on the structure of $\varphi$.

[Completeness] Completeness is proven in the standard way by defining a
translation from the dynamic language into the static fragment of the
language, see for instance [8, 14].

∎

### Proof of Proposition 1

###### Proof.

[First point]

[$\Rightarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction, that $\triangle$ is equivalent to $\bigcirc$ on $M$,
and that $M\not\models{\psi_{\triangle}}$. By the definition of
$\psi_{\triangle}$ in Def. 11,
$M\not\models{\bigwedge_{a,b\in\mathcal{A}}({N_{ab}}\lor\neg{sim^{\omega}_{ab}})}$.
Since
$M\not\models{\bigwedge_{a,b\in\mathcal{A}}({N_{ab}}\lor\neg{sim^{\omega}_{ab}})}$,
it follows that there are $a,b\in\mathcal{A}$ such that
$M\models{\neg{N_{ab}}\wedge{sim^{\omega}_{ab}}}$. From this, and the
reduction axioms for the dynamic modalities $\bigcirc$ and $\triangle$ in
Table 1, respectively, it follows that $M\models{\bigcirc{N_{ab}}}$ and
$M\not\models{\triangle{N_{ab}}}$. By Def. 9, this contradicts the initial
assumption that $\triangle$ is equivalent to $\bigcirc$ on $M$.

[$\Leftarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction, that $M\models\psi_{\triangle}$, and that it is not
the case that $\triangle$ is equivalent to $\bigcirc$ on $M$. From the fact
that $\triangle$ is not equivalent to $\bigcirc$ on $M$, by Obs. 1, it follows
that it must be the case that $M_{\triangle}$ and $M_{\bigcirc}$ differ on
whether they satisfy some atomic formula. By Obs. 2, we know that: (i) for all
$a\in\mathcal{A}$, for all $f\in{\mathcal{F}}$, $M\models{\bigcirc{f_{a}}}$
iff $M\models{\triangle{f_{a}}}$ (a synchronous update and a diffusion update
modifies in the same way the features of the agents); (ii) for all
$a,b\in\mathcal{A}$, if $M\models{\triangle{N_{ab}}}$, then
$M\models{\bigcirc{N_{ab}}}$. From (i) and (ii), and the fact that
$M_{\triangle}$ and $M_{\bigcirc}$ differ on whether they satisfy some atomic
formula, it must be the case that there are $a,b,\in\mathcal{A}$ such that
$M\models{\bigcirc{N_{ab}}}$ and $M\not\models{\triangle{N_{ab}}}$. By the
reduction axioms for the modality $\triangle$ in Table 1 and the fact that
$M\not\models{\triangle{N_{ab}}}$, it follows that $M\not\models{{N_{ab}}}$.
By the facts that $M\not\models{{N_{ab}}}$ and that
$M\models{\bigcirc{N_{ab}}}$, by the reduction axioms for the modality
$\bigcirc$, it must be the case that $M\models{{sim^{\omega}_{ab}}}$. We
therefore know that it is both the case that $M\not\models{{N_{ab}}}$ and that
$M\models{{sim^{\omega}_{ab}}}$. Therefore for some $a,b\in\mathcal{A}$, it is
true that $M\models{\neg{N_{ab}}\wedge{sim^{\omega}_{ab}}}$, i.e.
$M\models\bigvee_{a,b\in\mathcal{A}}(\neg N_{ab}\wedge sim^{\omega}_{ab})$,
which implies that $M\not\models\bigwedge_{a,b\in\mathcal{A}}(N_{ab}\lor\neg
sim^{\omega}_{ab})$. This means that $M\not\models\psi_{\triangle}$. This
contradicts the initial assumption that $M\models{\psi_{\triangle}}$.

[Second point]

[$\Rightarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction, that, $\square$ is equivalent to $\bigcirc$ on $M$,
and that $M\not\models\psi_{\square}$. From the definition of $\psi_{\square}$
in Def. 11, it follows that
$M\not\models{\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in{F}}({f_{a}}\lor\neg{f^{\tau}_{N(a)}})}$.
Since,
$M\not\models{\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in{F}}({f_{a}}\lor\neg{f^{\tau}_{N(a)}})}$,
it follows that there are $a\in\mathcal{A}$, and $f\in{\mathcal{F}}$ such that
$M\models{{\neg{f_{a}}}\wedge{f^{\tau}_{N(a)}}}$. From this and the reduction
axioms for the dynamic modalities $\bigcirc$ and $\square$ in Table 1, it
follows that $M\models{\bigcirc{f_{a}}}$ and $M\not\models{\square{f_{a}}}$.
By Def. 9, this contradicts the initial assumption that $\square$ is
equivalent to $\bigcirc$ on $\mathcal{M}$.

[$\Leftarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction that, $M\models\psi_{\square}$, and that it is not the
case that $\square$ and $\bigcirc$ are equivalent on $M$. From this and Def.
9, we know that $M_{\square}\neq M_{\bigcirc}$. By Obs. 1, it follows that it
must be the case that $M_{\square}$ and $M_{\bigcirc}$ differ on whether they
satisfy some atomic proposition. By Obs. 2, we know that: (i) for all
$a,b\in\mathcal{A}$, $M\models{\bigcirc{N_{ab}}}$ iff
$M\models{\square{N_{ab}}}$ (a network update and a synchronous update
modifies the network in exactly the same way); (ii) for all $a\in\mathcal{A}$,
for all $f\in{\mathcal{F}}$, if $M\models{\square{f_{a}}}$, then
$M\models{\bigcirc{f_{a}}}$. From (i) and (ii) and the fact that $M_{\square}$
and $M_{\bigcirc}$ differ on whether they satisfy some atomic proposition, it
must the case that there are $a\in\mathcal{A}$ and $f\in{\mathcal{F}}$, such
that $M\models{\bigcirc{f_{a}}}$ and $M\not\models{\square{f_{a}}}$. By the
fact that $M\not\models{\square{f_{a}}}$ and the reduction axioms for the
$\square$ modality in Table 1, it follows that $M\not\models{{f_{a}}}$. By the
fact that $M\not\models{{f_{a}}}$ and $M\models{\bigcirc{f_{a}}}$, by the
reduction axioms for the $\bigcirc$ modality in Table 1, it follows that it
must be the case that $M\models{{f^{\tau}_{N(a)}}}$. We therefore know that it
is the case that: $M\not\models{{f_{a}}}$ and $M\models{{f^{\tau}_{N(a)}}}$.
Therefore, there exist $a\in\mathcal{A}$ and $f\in\mathcal{F}$ such that
$M\models\neg{f_{a}}\wedge f^{\tau}_{N(a)}$. From this, it follows that
$M\models\bigvee_{a\in\mathcal{A}}\bigvee_{f\in\mathcal{F}}(\neg f_{a}\wedge
f^{\tau}_{N(a)})$, and, therefore,
$M\not\models\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in\mathcal{F}}(f_{a}\lor\neg
f^{\tau}_{N(a)})$. This means that $M\not\models\psi_{\square}$. We have
therefore reached a contradiction with the initial assumption that
$M\models\psi_{\square}$.

[Third point]

[$\Rightarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction, that, $\triangle\square$ is equivalent to $\bigcirc$
on $M$, and that $M\not\models\psi_{\triangle\square}$. By the definition of
$\psi_{\triangle\square}$ in Def. 11, we know that
$M\not\models\bigwedge_{{a,b}\in\mathcal{A}}(\neg{N_{ab}}\rightarrow({sim^{\omega}_{ab}}\leftrightarrow\triangle{{sim^{\omega}_{ab}})})$.
From this, it follows that, for some $a,b\in\mathcal{A}$,
$M\models{\neg{N_{ab}}}$ and
$M\not\models{({sim^{\omega}_{ab}}\leftrightarrow\triangle{{sim^{\omega}_{ab}})}}$.
One of the following two must be the case: (i) $M\models{{sim^{\omega}_{ab}}}$
and $M\not\models\triangle{{sim^{\omega}_{ab}}}$; (ii)
$M\not\models{{sim^{\omega}_{ab}}}$ and
$M\models\triangle{{sim^{\omega}_{ab}}}$. Assume that (i) is the case: the
facts that $M\models{{sim^{\omega}_{ab}}}$ and
$M\not\models\triangle{{sim^{\omega}_{ab}}}$, together with the fact that
$M\models{\neg{N_{ab}}}$ and the reduction axioms in Table 1, imply that
$M\models{\bigcirc{N_{ab}}}$ and $M\not\models{\triangle\square{N_{ab}}}$.
This implies that $\bigcirc$ is not equivalent to $\triangle\square$ on $M$,
contrary to our initial assumption. It must therefore be the case that (ii)
holds. Assume that (ii) is true, i.e. that $M\not\models{{sim^{\omega}_{ab}}}$
and $M\models\triangle{{sim^{\omega}_{ab}}}$. These assumptions, together with
the fact that $M\not\models{N_{ab}}$ and the reduction axioms in Table 1,
imply that $M\not\models{\bigcirc{N_{ab}}}$ and
$M\models{\triangle\square{N_{ab}}}$. By Def. 9, this contradicts the initial
assumption that $\bigcirc$ and $\triangle\square$ are equivalent on $M$. Since
neither (i) nor (ii) are possible, we have established that if $\bigcirc$ is
equivalent $\triangle\square$ on $M$, then $M\models\psi_{\triangle\square}$.

[$\Leftarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction that $M\models\psi_{\triangle\square}$, and that
$\triangle\square$ is not equivalent to $\bigcirc$ on $M$. From the fact that
$\triangle\square$ is not equivalent to $\bigcirc$ on $M$, by Def. 9, it
follows that $M_{\triangle\square}\neq M_{\bigcirc}$. By Obs. 1, we know that
$M_{\triangle\square}$ and $M_{\bigcirc}$ must differ on whether they satisfy
some atomic proposition. By Obs. 2, and by Def. 4 and Def. 5, we know that for
all $a\in\mathcal{A}$, and all $f\in{\mathcal{F}}$,
$M\models{\bigcirc{f_{a}}}$ iff $M\models{\triangle{f_{a}}}$ iff
$M\models{\triangle\square{f_{a}}}$ (informally, this simply mean that, since
a network update does not affect the agent’s features, and a synchronous
update and a diffusion update change the features in the same way, the
features of the agents after one synchronous update are the same as those
after one diffusion update followed by a subsequent network update). From this
and the fact that $M_{\triangle\square}$ and $M_{\bigcirc}$ must differ on
whether they satisfy some atomic proposition, it follows that one of the
following two cases must hold: (i) there are $a,b$ such that
$M\models{\triangle\square{N_{ab}}}$, and $M\not\models{\bigcirc{N_{ab}}}$;
(ii) there are $a,b$ such that $M\not\models{\triangle\square{N_{ab}}}$, and
$M\models{\bigcirc{N_{ab}}}$.

Assume that (i) is the case, i.e. there are $a,b$ such that
$M\models{\triangle\square{N_{ab}}}$, and $M\not\models{\bigcirc{N_{ab}}}$;
from the fact that $M\not\models{\bigcirc{N_{ab}}}$ and the reduction axioms
for $\bigcirc$ in Table 1, we know that $M\not\models{N_{ab}\lor
sim^{\omega}_{ab}}$, which implies that $M\models\neg{N_{ab}}$ and
$M\models\neg sim^{\omega}_{ab}$; furthermore, from the fact that
$M\models\triangle\square N_{ab}$, and that $M\not\models N_{ab}$, we know
that $M\models\triangle sim^{\omega}_{ab}$. If we put these together, we know
that $M\models\neg{N_{ab}}$, $M\models\neg sim^{\omega}_{ab}$, and
$M\models\triangle sim^{\omega}_{ab}$ at the same time: this implies that
$M\models\bigvee_{a,b\in\mathcal{A}}(\neg N_{ab}\wedge\neg
sim^{\omega}_{ab}\wedge\triangle sim^{\omega}_{ab})$. From this, it follows
that $M\not\models\bigwedge_{a,b\in\mathcal{A}}(\neg
N_{ab}\rightarrow(sim^{\omega}_{ab}\leftrightarrow\triangle
sim^{\omega}_{ab}))$: by Def. 11, it follows that
$M\not\models\psi_{\triangle\square}$, which contradicts our initial
assumption that $M\models\psi_{\triangle\square}$.

Since (i) is not possible, it must be the case that (ii) holds, i.e. there are
$a,b$ such that $M\not\models{\triangle\square{N_{ab}}}$, and
$M\models{\bigcirc{N_{ab}}}$. From the fact that
$M\not\models{\triangle\square N_{ab}}$ and the reduction axioms for
$\triangle$ and $\square$, we know that $M\not\models\triangle
sim^{\omega}_{ab}$ and $M\not\models N_{ab}$. From the fact that
$M\models\bigcirc N_{ab}$ and $M\not\models N_{ab}$, by the reduction axioms
for $\bigcirc$, we know that $M\models sim^{\omega}_{ab}$. Summarising the
facts above, we therefore know that $M\models\neg N_{ab}$, $M\models
sim^{\omega}_{ab}$ and $M\models\neg\triangle sim^{\omega}_{ab}$: this means
that $M\models\bigvee_{a,b\in\mathcal{A}}(\neg N_{ab}\wedge
sim^{\omega}_{ab}\wedge\neg\triangle sim^{\omega}_{ab})$. This implies the
fact that
$M\not\models\bigwedge_{{a,b}\in\mathcal{A}}(\neg{N_{ab}}\rightarrow({sim^{\omega}_{ab}}\leftrightarrow\triangle{{sim^{\omega}_{ab}})})$.
By Def. 11, it follows that $M\not\models\psi_{\triangle\square}$, which
contradicts our initial assumption that $M\models\psi_{\triangle\square}$.

Since neither (i) nor (ii) are possible, we have established that if
$M\models\psi_{\triangle\square}$, then $\bigcirc$ must be equivalent to
$\triangle\square$ on $M$.

[Fourth point]

[$\Rightarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction, that, for some arbitrary $n>0$,
$\square\triangle^{n}$ is equivalent to $\bigcirc$ on $\mathcal{M}$ and that
$M\not\models\psi_{\square\triangle^{n}}$. From the fact that
$M\not\models\psi_{\square\triangle^{n}}$, by Def. 11, it follows that
$M\not\models\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in{F}}(\neg{f_{a}}\rightarrow({f^{\tau}_{N(a)}}\leftrightarrow\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})})$.
From this, it follows that there exist $a\in\mathcal{A}$ and
$f\in{\mathcal{F}}$ such that $M\models{\neg{f_{a}}}$ and
$M\not\models({f^{\tau}_{N(a)}}\leftrightarrow\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})}$.
One of the following two must hold: (i) $M\models{f^{\tau}_{N(a)}}$ and
$M\not\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}}}$,
or (ii) $M\not\models{f^{\tau}_{N(a)}}$ and
$M\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}}}$.

Assume that (i) is the case and thus that $M\models{f^{\tau}_{N(a)}}$ and
$M\not\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}}}$.
Since $M\models{f^{\tau}_{N(a)}}$, by the reduction axiom for $\bigcirc$, we
know that $M\models\bigcirc f_{a}$. At the same time, since we know that
$M\not\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}}}$,
we know that for all $0\leq{i}\leq{n-1}$
$M\not\models{\square\triangle^{i}{f^{\tau}_{N(a)}}}$: this simply means that
after a network update, there is no sequence of diffusion update after which
the agent $a$ has social conformity pressure to adopt feature $f$. From this
and the fact that $M\not\models f_{a}$, by the reduction axioms of for the
dynamic modalities, we know that $M\not\models\square\triangle f_{a}$.
Therefore, it is both the case that $M\models\bigcirc f_{a}$, and
$M\not\models\square\triangle^{n}f_{a}$, which, by Def. 9, contradicts the
initial assumption that $\bigcirc$ is equivalent to $\square\triangle^{n}$ on
$M$.

Since (i) is not possible, it must be the case that (ii) holds, i.e. it is the
case that $M\not\models{f^{\tau}_{N(a)}}$ and
$M\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}}}$.
From the fact that $M\not\models f^{\tau}_{N(a)}$, and the fact that
$M\not\models f_{a}$, by the reduction axioms for $\bigcirc$, it follows that
$M\not\models\bigcirc f_{a}$. From the fact that
$M\not\models{f^{\tau}_{N(a)}}$ and
$M\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}}}$,
it follows that there is an $i\leq(n-1)$ such that
$M\models\square\triangle^{i}f^{\tau}_{N(a)}$ (this means that, after a
network update, at some point of a sequence of further diffusion update, agent
$a$ has pressure to adopt feature $f$). From this and the reduction axioms for
the dynamic modality $\triangle$, it follows that
$M\models\square\triangle^{i+1}f_{a}$. Since $i\leq{n-1}$, and by the fact
that features cannot be abandoned, it follows that
$M\models{\square\triangle^{n}f_{a}}$. Thus, it is both true that
$M\not\models\bigcirc f_{a}$, and $M\models\square\triangle^{n}f_{a}$. By Def.
9, this contradicts the initial assumption that $\square\triangle^{n}$ is
equivalent to $\bigcirc$ on $M$.

Since neither (i) nor (ii) are possible, we have established that if
$\bigcirc$ is equivalent $\square\triangle^{n}$ on $M$, then
$M\models\psi_{\square\triangle^{n}}$.

[$\Leftarrow$] Let a model
${M=\langle{\mathcal{N},\mathcal{V},\omega,\tau}\rangle}$ be given. Assume,
towards a contradiction, that, for some $n>0$,
$M\models\psi_{\square\triangle^{n}}$ and that $\bigcirc$ is not equivalent to
$\square\triangle^{n}$ in $M$. From the fact that $\bigcirc$ is not equivalent
to $\square\triangle^{n}$ in $M$, by Def. 9, it follows that
$M_{\square\triangle^{n}}\neq M_{\bigcirc}$. Thus, by Obs. 1, we know that
$M_{\square\triangle^{n}}$ and $M_{\bigcirc}$ must differ on whether they
satisfy some atomic proposition. By Obs. 2 and by Def. 4 and Def. 5, we know
that, for all $a,b\in\mathcal{A}$, $M\models{\bigcirc{N_{ab}}}$ iff
$M\models{\square{N_{ab}}}$ iff $M\models{\square\triangle^{n}{N_{ab}}}$.
Informally, this follows from the fact that, since a diffusion update does not
affect the agent’s features, and a synchronous update and a network update
change the network structure in the same way, the connections between the
agents after one synchronous update are the same as those obtained after one
network update followed by multiple subsequent diffusion update. From this and
the fact that $M_{\square\triangle^{n}}$ and $M_{\bigcirc}$ must differ on
whether they satisfy some atomic proposition, there must exist
$a\in\mathcal{A}$ and $f\in{\mathcal{F}}$, s.t. it is not the case that
$M\models{\square\triangle^{n}f_{a}}$ iff $M\models{\bigcirc{f_{a}}}$.
Therefore, either one of the following cases must hold: (i)
$M\models{\square\triangle^{n}f_{a}}$ and $M\not\models{\bigcirc{f_{a}}}$, or
(ii) $M\not\models{\square\triangle^{n}f_{a}}$ and
$M\models{\bigcirc{f_{a}}}$.

Assume that (i): $M\models{\square\triangle^{n}{f_{a}}}$ and
$M\not\models{\bigcirc{f_{a}}}$. By the fact $M\not\models{\bigcirc{f_{a}}}$
and the reduction axioms for $\bigcirc$, we know that
$M\not\models{f^{\tau}_{N(a)}}$ and $M\not\models f_{a}$. From the fact that
$M\models{\square\triangle^{n}{f_{a}}}$, we know that there exist an
$0\leq{i}\leq{n-1}$ such that $M\models\square\triangle^{i}f^{\tau}_{N(a)}$:
this simply means that, at some point, after a network-update and potentially
after subsequent diffusion updates, $a$ has pressure to adopt $f$. From this,
it follows that
$M\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})}$.
Therefore, from the above we know that $M\models\neg{f_{a}}$,
$M\models\neg{f^{\tau}_{N(a)}}$ and
$M\models\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})}$.
This imply that
$M\models\bigvee_{a\in\mathcal{A}}\bigvee_{f\in\mathcal{F}}(\neg{f_{a}}\wedge\neg{f^{\tau}_{N(a)}}\wedge\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})})$.
Therefore
$M\not\models\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in{F}}(\neg{f_{a}}\rightarrow({f^{\tau}_{N(a)}}\leftrightarrow\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})})$.
Thus, by Def. 11, we know that $M\not\models\psi_{\square\triangle^{n}}$,
which contradicts our initial assumption that
$M\models\psi_{\square\triangle^{n}}$.

Since (i) cannot be the case, it must be the case that (ii):
$M\not\models{\square\triangle^{n}{f_{a}}}$ and $M\models{\bigcirc{f_{a}}}$.

From the fact $M\not\models{\square\triangle^{n}{f_{a}}}$, by the reduction
axioms for the dynamic modalities, we know two things: $M\not\models{f_{a}}$,
and there does not exist $0\leq i\leq n-1$, such that
$M\models\square\triangle^{i}f^{\tau}_{N(a)}$ (this simply means that at no
point after a network update and subsequent diffusion updates $a$ has pressure
to adopt $f$; indeed, if this was the case then $a$ would at some point adopt
$f$, and will never abandon it). From the fact that $M\not\models f_{a}$ and
that $M\models\bigcirc f_{a}$, by the reduction axiom for $\bigcirc$, we know
that $M\models f^{\tau}_{N(a)}$. Summarising the above we know that:
$M\models\neg f_{a}$, $M\models f^{\tau}_{N(a)}$ and
$M\models\neg\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}}}$.
Thus, $M\models\bigvee_{a\in\mathcal{A}}\bigvee_{f\in\mathcal{F}}(\neg
f_{a}\wedge
f^{\tau}_{N(a)}\wedge\neg\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})}$.
Thus,
$M\not\models\bigwedge_{a\in\mathcal{A}}\bigwedge_{f\in{F}}(\neg{f_{a}}\rightarrow({f^{\tau}_{N(a)}}\leftrightarrow\bigvee_{0\leq{i}\leq{n-1}}{\square\triangle^{i}{f^{\tau}_{N(a)}})})$.
By Def. 11, it follows that $M\not\models\psi_{\square\triangle^{n}}$,
contrary to the initial assumption that $M\models\psi_{\square\triangle^{n}}$.

Since neither (i) nor (ii) are possible, we have established that if
$M\models\psi_{\square\triangle^{n}}$, then $\bigcirc$ is equivalent to
$\square\triangle^{n}$ on $M$.

∎