Open Problems in a Logic of Gossips

TL;DR

This paper discusses open problems in a logic for distributed gossip protocols, highlighting unresolved questions about their semantics, correctness, and extensions with common knowledge, despite recent advances in their formal verification.

Contribution

It identifies and clarifies key open issues in the logic of gossip protocols, providing background and partial results to guide future research.

Findings

Decidability of semantics and truth for the logic

Decidability of the logic with common knowledge operator

Identification of open questions and challenges

Abstract

Gossip protocols are programs used in a setting in which each agent holds a secret and the aim is to reach a situation in which all agents know all secrets. Such protocols rely on a point-to-point or group communication. Distributed epistemic gossip protocols use epistemic formulas in the component programs for the agents. The advantage of the use of epistemic logic is that the resulting protocols are very concise and amenable for a simple verification. Recently, we introduced a natural modal logic that allows one to express distributed epistemic gossip protocols and to reason about their correctness. We proved that the resulting protocols are implementable and that all aspects of their correctness, including termination, are decidable. To establish these results we showed that both the definition of semantics and of truth of the underlying logic are decidable. We also showed that the analogous results hold for an extension of this logic with the 'common knowledge' operator. However, several, often deceptively simple, questions about this logic and the corresponding gossip protocols remain open. The purpose of this paper is to list and elucidate these questions and provide for them an appropriate background information in the form of partial of related results.

Equations

$$\varphi ::=F_{a}S\mid \neg \varphi \mid \varphi \wedge \varphi \mid K_a\varphi ,$$

$${\text{Exp}}_a\equiv \underset{S\in \mathsf{Sec}}{\bigwedge }{F}_{a}S,$$

$$ab(\mathsf{s}):=({\mathsf{Q}}_d^{\prime }{)}_{d\in \mathsf{A}},$$

$$ϵ(\mathsf{s}):=\mathsf{s},(\mathsf{c}.\mathsf{c})(\mathsf{s}):=\mathsf{c}(\mathsf{c}(\mathsf{s})).$$

$$A.B.C\stackrel{ac}{⟶}AC.B.AC\stackrel{bc}{⟶}AC.ABC.ABC\stackrel{ac}{⟶}ABC.ABC.ABC.$$

$$\mathsf{c}\models F_{a}S$$

$$\mathsf{c}\models K_a\varphi$$

$$\underset{\begin{array}{c}a,b\in \mathsf{A}\\ a\ne b\end{array}}{\bigwedge }(F_{a}B\to \underset{k=2}{\overset{n}{\bigvee }}\underset{\begin{array}{c}{a}_1,\dots ,a_k\in \mathsf{A}\\ a_1=b,a_k=a\\ a_i\ne a_j\text{ for all }i\ne j\end{array}}{\bigvee }\underset{h=1}{\overset{k-1}{\bigwedge }}(F_{a_h}{A}_{h+1}\wedge F_{a_{h+1}}{A}_h)).$$

$$\underset{\begin{array}{c}a,b,c\in \mathsf{A}\\ \{a,b,c\}=\mathsf{A}\end{array}}{\bigwedge }(F_{a}B\to (F_{b}A\wedge F_{a}B)\vee (F_{b}C\wedge F_{c}B\wedge F_{c}A\wedge F_{a}C)).$$

$$\underset{\begin{array}{c}a,b\in \mathsf{A}\\ a\ne b\end{array}}{\bigwedge }(F_{a}B\to \underset{\begin{array}{c}c,a\in \mathsf{A}\\ c\ne a\end{array}}{\bigvee }{F}_{c}A).$$

$$\underset{\begin{array}{c}a,b\in \mathsf{A}\\ a\ne b\end{array}}{\bigwedge }(F_{a}B\to \underset{k=2}{\overset{n}{\bigvee }}\underset{\begin{array}{c}{a}_1,\dots ,a_k\in \mathsf{A}\\ a_1=b,a_k=a\\ a_i\ne a_j\text{ for all }i\ne j\end{array}}{\bigvee }{F}_{a_{k-1}}A),$$

$$\bigwedge_{\begin{subarray}{c}a,b\in\mathsf{A}\\ a\neq b\end{subarray}}\Big{(}F_{a}B\land\bigwedge_{\begin{subarray}{c}i\in\mathsf{A}\\ i\neq a,i\neq b\end{subarray}}\neg F_{i}B\Big{)}\to F_{b}A.$$

$$\underset{\begin{array}{c}a,b\in \mathsf{A}\\ a\ne b\end{array}}{\bigwedge }(F_{a}B\to F_{b}A\vee \underset{k=3}{\overset{n}{\bigvee }}\underset{\begin{array}{c}{a}_1,\dots ,a_k\in \mathsf{A}\\ a_1=b,a_k=a\\ a_i\ne a_j\text{ for all }i\ne j\end{array}}{\bigvee }{F}_{a_2}B),$$

$$\varphi ::=F_{a}S\mid \neg \varphi \mid \varphi \wedge \varphi \mid C_G\varphi ,$$

$$C_G\varphi \equiv \underset{t\in G^{\ast }}{\bigwedge }{K}_t\varphi .$$

$$C_{G}\phi\mbox{$\>\leftrightarrow\>$}K_{t}\phi$$

$$\mathsf{c}\models C_G\varphi \text{mbox}iff\models \varphi .$$

$$\mathsf{c}\models C_{\{a,b\}}\varphi \text{mbox}iff\mathsf{c}\models K_{abab}\varphi .$$

$$\ast [[{]}_{j=1}^m{\psi }_j\to {\mathsf{c}}_j],$$

$$\ast [[{]}_{j\in \mathsf{A}}\neg F_{i}J\to ij].$$

$$\ast [[{]}_{j\in \mathsf{A}}\neg K_i{F}_{j}I\to ij].$$

$$\mathsf{c}\models \underset{a\in \mathsf{A},S\in \mathsf{Sec}}{\bigwedge }{F}_{a}S,$$

$$\ast [[{]}_{j\in N_i,S\in \mathsf{Sec}}{F}_{i}S\wedge \neg K_i{F}_{j}S\to ij].$$

$$\ast [[{]}_{j\in N_i}\neg F_{i}J\to ij].$$

$$\ast [[{]}_{j\in N_i}\neg {\text{Exp}}_i\to ij]$$

$$\begin{array}[]{l}(a,i_{1}),(a,i_{2}),\mbox{$\ldots$},(a,i_{n-4}),\\ (a,b),(c,d),(a,d),(b,c),\\ (a,i_{1}),(a,i_{2}),\mbox{$\ldots$},(a,i_{n-4}).\end{array}$$

$$\mathsf{c}\models K_a\varphi$$

$$\mathsf{c}\models {\varphi }_c$$

$$\mathsf{c},cd\models {\varphi }_a$$

$$\mathsf{c},ab,cd,{\mathsf{d}}^{\prime }\models K_i\varphi$$

$$\mathsf{c},ab,cd,\mathsf{d}\models \varphi$$

Full text

Recently, we introduced a natural modal logic that allows one to express distributed epistemic gossip protocols and to reason about their correctness. We proved that the resulting protocols are implementable and that all aspects of their correctness, including termination, are decidable. To establish these results we showed that both the definition of semantics and of truth of the underlying logic are decidable. We also showed that the analogous results hold for an extension of this logic with the ‘common knowledge’ operator.

However, several, often deceptively simple, questions about this logic and the corresponding gossip protocols remain open. The purpose of this paper is to list and elucidate these questions and provide for them an appropriate background information in the form of partial of related results.

1 Introduction

Gossip protocols concern a set up in which each agent holds initially a secret and the aim it to arrive, by means of point-to-point or group communications (called calls), at a situation in which all agents know each other secrets. During the calls the agents exchange some, possibly all, secrets they know.

These protocols were successfully used in a number of domains, for instance communication networks [21], computation of aggregate information [26], and data replication [28]. For a more recent account see [25] and [27].

In [11] a dynamic epistemic logic was introduced in which gossip protocols could be expressed as formulas. These protocols rely on agents’ knowledge and are distributed, so they are distributed epistemic gossip protocols. This means that they can be seen as special cases of knowledge-based programs introduced in [19].

In [4] a simpler modal logic was introduced that is sufficient to define these protocols and to reason about their correctness. This logic is interesting in its own rights and was subsequently studied in a number of papers. In particular, in [6], and in the full version in [9], we established decidability of its semantics and truth for a limited fragment. Building upon these results we then proved that the distributed gossip protocols, the guards of which are defined in this logic, are implementable, that their partial correctness is decidable, and that termination and two forms of fair termination of these protocols are decidable, as well. Further, in [5] the computational complexity of this fragment was studied and in [7] we considered its extension with the common knowledge operator for which we established analogous decidability results.

In spite of the simplicity of this modal logic several natural questions about it and the gossip protocols defined using this logic remain open. In what follows we discuss these problems. For each of them we provide the relevant background information and establish some partial results.

Among these partial results let us mention the following ones:

• •

When the agents form a star graph, each correct distributed epistemic gossip protocol in the framework of [4] has to rely on guards with the modal operators (Theorem 7.3 in Section 7). This is relevant since the complexity of determining truth of guards is higher in presence of modal operators (see Section 4).

• •

It is well known (see, e.g., [32] discussed in Section 7) that for 4 agents 4 calls are both needed and sufficient to reach a situation in which all agents know all secrets. The resulting protocol is centralized. We show that when distributed epistemic gossip protocols are used, for 4 agents 5 calls are both needed and sufficient (Theorems 7.14 and 7.16 in Section 7).

• •

In the literature on distributed computing, e.g., on Calculus of Communicating systems (CCS) of [29], there is a wealth of literature on various ways of comparing behaviour of two processes (see, e.g., [30] for an extensive overview of the fundamental concept of bisimulation). Distributed epistemic gossip protocols can be naturally compared by means of a notion that one of them can simulate another. We show that checking it can be done in exponential time (Theorem 8.25 in Section 8).

Further, the arguments used to prove the last result imply that all computations of a terminating gossip protocol are of length $<n^{4}$.

The paper is organized as follows. In the next section we discuss related work. Then, in Section 3, introduce the already mentioned logic, originally defined in [4], and in Section 4 discuss some natural open problems about it. In Section 5 we recall an extension of this logic with the common knowledge operator and introduce two open problems concerning it. Next, in Section 6, we recall the distributed epistemic gossip protocols considered in [4]. Then, in Sections 7 and 8 we discuss natural open problems about these protocols. For several open problems we provide some partial results.

2 Related work

As already mentioned, distributed epistemic gossip protocols were introduced in [11]. In [10] a tool was presented that given a high level description of an epistemic protocol in this setting generates the characteristics of the protocol. In both papers three types of calls were considered but the ones considered here (initially studied in [4]) differ from them in that we assume that agents not participating in the call are not aware of it. In [4] also two other modes of communication were considered, in which only one agent (the caller or the called one) learns new secrets. The assumptions about the calls used in [11] and [4] were presented in a uniform framework in [3], where in total 18 types of communication were introduced and compared w.r.t. their epistemic strength.

In [22] and [23] centralized gossip protocols were studied the aim of which is to achieve higher-order shared knowledge, for example knowledge of level 2 which stipulates that everybody knows that everybody knows all secrets. In particular, a protocol was presented and proved correct that achieves in $(k+1)(n-2)$ steps shared knowledge of level $k$. These matters were further investigated in [13], where optimal protocols for various versions of such a generalized gossip problem were presented. These protocols depend on various parameters, for example type of the underlying graph or the type of communication. Further, different gossip problems were also studied in which some negative goals, for example that certain agents must not know certain secrets, are supposed to be achieved. In [14] such problem were studied further in the presence of temporal constraints, i.e., a given call can only (or has to) be made within a given time interval.

Then in [12] gossip protocols were analyzed as an instance of multi-agent epistemic planning that was subsequently translated into a planning language.

The underlying framework was analyzed from a number of views. In [17] gossip problems were considered in an epistemic framework that provides several parameters allowing us to capture various aspects of it, for example the initial knowledge of the agents, the type of communication used, and the desired type of the protocol (for example, a symmetric one). For some of the combinations of the parameters the minimum number of calls needed to reach the final situation was established. The expected time of termination of several gossip protocols for complete graphs was studied by [18].

Next, in [15] dynamic distributed gossip protocols were studied in which the calls allow the agents not only to share the secrets but also to transmit the links. These protocols were characterized in terms of the class of graphs for which they terminate. They differ from the ones here considered, which are static. This set up was further investigated in [16] where various dynamic gossip protocols were proposed and analyzed. In [20] such protocols were analyzed by embedding them in a network programming language NetKAT proposed in [2].

3 Logic: a recall

We recall here the framework of [4]. We assume a fixed set $\mathsf{A}$ of $n\geq 3$ agents and stipulate that each agent holds exactly one secret, and that there exists a bijection between the set of agents and the set of secrets. We use it implicitly by denoting the secret of agent $a$ by $A$, of agent $b$ by $B$, etc. We denote by $\mathsf{Sec}$ the set of all secrets.

The language $\mathcal{L}$ is defined by the following grammar:

[TABLE]

where $S\in\mathsf{Sec}$ and $a\in\mathsf{A}$.

So $F_{a}S$ is an atomic formula, while $K_{a}\phi$ is a compound formula. We read $F_{a}S$ as ‘agent $a$ is familiar with the secret $S$’ (or ‘agent $a$ holds secret $S$’) and $K_{a}\phi$ as ‘agent $a$ knows the formula $\phi$’. Below we shall freely use other Boolean connectives that can be defined using $\neg$ and $\land$ in a standard way.

In the sequel we shall use the following formula

[TABLE]

that denotes the fact that agent $a$ is familiar with all the secrets (is an ‘expert’).

In the paper we shall use the following sublanguages of $\mathcal{L}$:

• •

$\mathcal{L}_{0}$, its propositional part, which consists of the formulas that do not use the $K_{a}$ modalities;

• •

$\mathcal{L}_{1}$, which consists of the formulas without the nested use of the $K_{a}$ modalities;

• •

$\mathcal{L}^{a}_{1}$, where $a\in\mathsf{A}$ is a fixed agent, which consists of the formulas from $\mathcal{L}_{1}$ where the only modality is $K_{a}$.

Each call, written as $ab$, concerns two different agents, the caller, $a$, and the callee, $b$. After the call the caller and the callee learn each others secrets. Calls are denoted by $\mathsf{c}$, $\mathsf{d}$. Abusing notation we write $a\in\mathsf{c}$ to denote that agent $a$ is one of the two agents involved in the call $\mathsf{c}$.

Following [4] we stipulate that agents not involved in the call are not aware of it. This will be addressed in Definition 1 below.

In what follows we focus on call sequences. Unless explicitly stated each call sequence is assumed to be finite. The empty sequence is denoted by $\epsilon$. We use $\bm{\mathsf{c}}$ to denote a call sequence and $\bm{\mathsf{C}}$ to denote the set of all finite call sequences. Given call sequences $\bm{\mathsf{c}}$ and $\bm{\mathsf{d}}$ and a call $\mathsf{c}$ we denote by $\bm{\mathsf{c}}.\mathsf{c}$ the outcome of adding $\mathsf{c}$ at the end of the sequence $\bm{\mathsf{c}}$ and by $\bm{\mathsf{c}}.\bm{\mathsf{d}}$ the outcome of appending the sequences $\bm{\mathsf{c}}$ and $\bm{\mathsf{d}}$. We say that $\bm{\mathsf{c}}_{2}$ is a subsequence of a call sequence $\bm{\mathsf{c}}$ if for some call sequences $\bm{\mathsf{c}}_{1}$ and $\bm{\mathsf{c}}_{3}$ we have $\bm{\mathsf{c}}=\bm{\mathsf{c}}_{1}.\bm{\mathsf{c}}_{2}.\bm{\mathsf{c}}_{3}$.

To describe what secrets the agents are familiar with, we use the concept of a gossip situation. It is a sequence $\mathsf{s}=(\mathsf{Q}_{a})_{a\in\mathsf{A}}$, where \{A\}\mbox{>\subseteq>}\mathsf{Q}_{a}\mbox{>\subseteq>}\mathsf{Sec} for each agent $a$. Intuitively, $\mathsf{Q}_{a}$ is the set of secrets $a$ is familiar with in the gossip situation $\mathsf{s}$. The initial gossip situation is the one in which each $\mathsf{Q}_{a}$ equals ${\{A\}}$ and is denoted by $\mathsf{root}$. It reflects the fact that initially each agent $a$ is familiar only with his own secret, $A$. We say that an agent $a$ is an expert in a gossip situation $\mathsf{s}$ if $a$ is familiar in $\mathsf{s}$ with all the secrets, i.e., if $\mathsf{Q}_{a}=\mathsf{Sec}$.

Each call transforms the current gossip situation by modifying the sets of secrets the agents involved in the call are familiar with as follows. Consider a gossip situation $\mathsf{s}:=(\mathsf{Q}_{d})_{d\in\mathsf{A}}$ and a call $ab$.

Then

[TABLE]

where $\mathsf{Q}^{\prime}_{a}=\mathsf{Q}^{\prime}_{b}=\mathsf{Q}_{a}\cup\mathsf{Q}_{b}$, and for $c\not\in\{a,b\}$, $\mathsf{Q}^{\prime}_{c}=\mathsf{Q}_{c}$.

So the effect of a call is that the caller and the callee share the secrets they are familiar with.

The result of applying a call sequence to a gossip situation $\mathsf{s}$ is defined inductively as follows:

[TABLE]

Example 1

We will use the following concise notation for gossip situations. Sets of secrets will be written down as lists. E.g., the set ${\{A,B,C\}}$ will be written as $ABC$. Gossip situations will be written down as lists of lists of secrets separated by dots. E.g., if there are three agents, $a$, $b$ and $c$, then $\mathsf{root}=A.B.C$ and the gossip situation $({\{A,B\}},{\{A,B\}},{\{C\}}$) will be written as $AB.AB.C$.

Let $\mathsf{A}={\{a,b,c\}}$. Consider the call sequence $(ac,bc,ac)$. It generates the following successive gossip situations starting from $\mathsf{root}$:

[TABLE]

Hence $(ac,bc,ac)(\mathsf{root})=(ABC.ABC.ABC)$. $\Box$

As calls progress in sequence from the initial situation, agents may be uncertain about which call sequence took place. This uncertainty is captured by the appropriate equivalence relations on the call sequences.

Definition 1

Fix an agent $a$. We define $\sim_{a}\subseteq\bm{\mathsf{C}}\times\bm{\mathsf{C}}$ as the smallest equivalence relation satisfying the following conditions:

[Base]* $\epsilon\sim_{a}\epsilon$,*

[Step]* Suppose $\bm{\mathsf{c}}\sim_{a}\bm{\mathsf{d}}$.*

1. (i)

If $a\not\in\mathsf{c}$, then $\bm{\mathsf{c}}.\mathsf{c}\sim_{a}\bm{\mathsf{d}}$ and $\bm{\mathsf{c}}\sim_{a}\bm{\mathsf{d}}.\mathsf{c}$. 2. (ii)

If there exists $b\in\mathsf{A}$ and $\mathsf{c}\in{\{ab,ba\}}$ such that $\bm{\mathsf{c}}.\mathsf{c}(\mathsf{root})_{a}=\bm{\mathsf{d}}.\mathsf{c}(\mathsf{root})_{a}$, then $\bm{\mathsf{c}}.\mathsf{c}\sim_{a}\bm{\mathsf{d}}.\mathsf{c}$.

In (i) we formalize the assumption that the agents are not aware of the calls they do not participate in. In turn, in (ii) we capture the intuition that two call sequences are indistinguishable for an agent if the sets of his calls in both sequences are the same and in each sequence he observes the same set of secrets. For instance, by (i) we have $ab,bc\sim_{a}ab,bd$. But we do not have $bc,ab\sim_{a}bd,ab$ since $C\in(bc,ab)(\mathsf{root})_{a}$, while $C\not\in(bd,ab)(\mathsf{root})_{a}$.

Next, we recall the definition of truth.

Definition 2

Consider a call sequence $\bm{\mathsf{c}}\in\bm{\mathsf{C}}$. We define the satisfaction relation $\models$ inductively as follows (clauses for Boolean connectives are as usual and omitted):

[TABLE]

Further, we say that $\phi$ is true, and write $\models\phi$, when $\forall\bm{\mathsf{c}}\ \bm{\mathsf{c}}\models\phi$. Also, we say that $\phi$ and $\psi$ are equivalent if \forall\bm{\mathsf{c}}\ \bm{\mathsf{c}}\models\phi\mbox{>\leftrightarrow>}\psi.

So a formula $F_{a}S$ is true after the call sequence $\bm{\mathsf{c}}$ whenever secret $S$ belongs to the set of secrets agent $a$ is familiar with in the situation generated by the call sequence $\bm{\mathsf{c}}$ applied to the initial situation $\mathsf{root}$. Hence $\bm{\mathsf{c}}\models Exp_{a}$ iff agent $a$ is an expert in $\bm{\mathsf{c}}(\mathsf{root})$.

The knowledge operator is interpreted as customary in epistemic logic, using the equivalence relations $\sim_{a}$.

4 Open problems about the logic

The first problem concerns the propositional part $\mathcal{L}_{0}$ of the language $\mathcal{L}$. In [5] we established that the problem of determining the complexity of the semantics of the language of $\mathcal{L}_{0}$ (i.e, determining whether $\bm{\mathsf{c}}\models\phi$ for a given call sequence $\bm{\mathsf{c}}$) is in P, while the problem of determining truth in the language of $\mathcal{L}_{0}$ (i.e, determining whether $\bm{\mathsf{c}}\models\phi$ for all call sequences $\bm{\mathsf{c}}$) is co-NP-complete. Note that the latter implies that checking whether there exists a call sequence $\bm{\mathsf{c}}$ such that $\bm{\mathsf{c}}\models\phi$ is NP-complete.

Problem 1

Find an axiomatization of $\mathcal{L}_{0}$.

Comments

We stipulate that the following formula should be an axiom:

[TABLE]

It formalizes the fact that communication is bidirectional and that agents learn secrets through a chain of calls, and is easily seen to be true. Here and elsewhere we make use of the fact that there is a bijection between secrets and agents, which allows us to use agents (here $b,a_{h}$ and $a_{h+1}$) when referring to the corresponding secrets (here $B,A_{h}$ and $A_{h+1}$). Note that the second disjunction is finite, since we postulate that the agents a_{1},\mbox{\ldots},a_{k} are pairwise different.

Here is the version of (1) when $\mathsf{A}$ has three agents that is more readable:

[TABLE]

Assuming a sound and complete proof system for Boolean formulas formula (1) implies the following natural formula of $\mathcal{L}_{0}$ stating that each agent can learn a new secret only by revealing its own:

[TABLE]

To see the claim it suffices to note that (1) implies

[TABLE]

from which (2) follows.

In [3] it was observed that the following formula is true:

[TABLE]

It states that if agent $a$ is the only agent (different from $b$) familiar with the secret of $b$, then agent $b$ is familiar with the secret of $a$.

It is easy to see that assuming a sound and complete proof system for Boolean formulas (1) implies (3). To this end it suffices to note that (1) implies

[TABLE]

from which (3) follows.

A more ambitious problem is the following one.

Problem 2

Find an axiomatization of $\mathcal{L}$. Determine the complexity of the semantics and of truth in the language of $\mathcal{L}$.

Comments

In [6] and in the full version in [9], we showed that for the sublanguage $\mathcal{L}_{1}$ of $\mathcal{L}$ both the semantics and truth are decidable. In [5] we sharpened these results by showing that the first problem is $\text{P}^{\text{NP}}_{\parallel}$-complete, while the complexity of determining the truth is in $\text{coNP}^{\text{NP}}$. It is not clear how to extend these results to larger fragments of $\mathcal{L}$. Recall that the complexity class $\text{P}^{\text{NP}}_{\parallel}$, defined in [33], corresponds to the class of problems solvable by a deterministic polynomial-time Turing machine that has a parallel access to an NP oracle (i.e., no query to this oracle can depend on the outcome of any other). In [33, 31] many natural problems were shown to be complete for this class. One of them is checking for two Boolean formulas $\phi,\phi^{\prime}$ whether the maximum number of variables assigned true in a satisfying assignment is greater for $\phi$ than for $\phi^{\prime}$. On the other hand, the complexity class ${\text{coNP}}^{\text{NP}}$, commonly denoted by $\Pi^{P}_{2}$, corresponds to a non-deterministic polynomial-time Turing machines with an access to an NP oracle that accepts a given input if and only if all its non-deterministic branches accept it. An example problem complete for this class is the satisfiability for quantified Boolean formulas with two alternations of quantifiers $\forall{x_{1},\ldots,x_{k}}\exists{y_{1},\ldots,y_{l}}\phi$, where $\phi$ is a Boolean formula over the variables $x_{1},\ldots,x_{k},y_{1},\ldots,y_{l}$.

5 Open problems concerning common knowledge

In [7] an extension of the language $\mathcal{L}$ was considered that involves the common knowledge operator. The resulting language $\mathcal{L}_{ck}$ is defined by the following grammar:

[TABLE]

where $S\in\mathsf{Sec}$ and $a\in\mathsf{A}$ and G\mbox{>\subseteq>}\mathsf{A}.

Recall that the semantics of the $C_{G}$ operator is defined as follows. Given a set $A$ let $A^{*}$ be the set of all finite sequences formed from the elements of $A$. For t=a_{1},\mbox{\ldots},a_{k} let K_{t}=K_{a_{1}}\mbox{\ldots}K_{a_{k}}. Then we stipulate that

[TABLE]

Note that the formula on the right-hand side is an infinite conjunction.

When $G$ is a singleton, say $G=\{a\}$, the formula $C_{G}\phi$ has the same semantics as $K_{a}\phi$, since $K_{a}K_{a}\phi$ is equivalent to $K_{a}\phi$. So the language $\mathcal{L}_{ck}$ can be viewed as an extension of $\mathcal{L}$.

Problem 3

Determine whether common knowledge is equivalent to a nested knowledge. More precisely, determine whether for every $G$ and $\phi$ there exists $t\in G^{*}$ such that the formulas $C_{G}\phi$ and $K_{t}\phi$ are equivalent.

If the answer to Problem 3 is positive, then it is natural to ask whether $t\in G^{*}$ can be found independently of the formula $\phi$, that is, whether for some $t\in G^{*}$ the equivalence

[TABLE]

holds for all formulas $\phi$ in $\mathcal{L}_{ck}$ or in some fragment of it.

Problem 4

Find an axiomatization of $\mathcal{L}_{ck}$. Determine the complexity of the semantics and of truth in the language of $\mathcal{L}_{ck}$.

Comments

We do not know the answer to Problem 3 even for the formulas of the form $C_{G}\phi$, where $\phi\in\mathcal{L}_{0}$. In [8] we succeeded to establish the following limited results.

Theorem

1. (i)

Suppose that $|G|\geq 3$. Then for all call sequences $\bm{\mathsf{c}}$ and formulas $\phi\in\mathcal{L}_{ck}$

[TABLE]

*Consequently, the formulas $C_{G}\phi$ and $\phi$ are equivalent. * 2. (ii)

For all call sequences $\bm{\mathsf{c}}$ that do not contain the call $ab$ and all formulas $\phi\in\mathcal{L}_{ck}$ that do not contain the $\neg$ symbol

[TABLE]

Part (i) states that the formulas commonly known by a group of at least three agents are precisely the true formulas. Part (ii) states that for a group of two agents common knowledge of negation-free formulas is equivalent to the 4th fold iterated knowledge w.r.t. a call sequence in which no calls between these two agents were made. Examples in [8] show that this claim does not hold for arbitrary formulas and that the restriction on the call sequence cannot be dropped.

In [8] we showed that both the semantics and truth in the sublanguage of $\mathcal{L}_{ck}$ that consists of the formulas with no nested $C_{G}$ modalities are decidable.

6 Distributed epistemic gossip protocols: a recall

In [4], as a follow up on [11], we studied distributed epistemic gossip protocols. Their goal is to reach a gossip situation in which each agent is an expert. In other words, their goal is to transform a gossip situation in which the formula $\bigwedge_{a\in\mathsf{A}}(F_{a}A\land\bigwedge_{b\in\mathsf{A},b\neq a}\neg F_{a}B)$ is true into one in which the formula $\bigwedge_{a,b\in\mathsf{A}}F_{a}B$ is true. As explained in the introduction, in [4] a different syntax of the gossip protocols than in [11] was used.

Let us recall the definition. The adopted syntax follows the syntax of the CSP language (Communicating Sequential Processes) of [24], in which ’$*$’ denotes a repetition and ‘$[]$’ a nondeterministic choice. By a component program, in short a program, for an agent $a$ we mean a statement of the form

[TABLE]

where $m\geq 0$ and each $\psi_{j}\to\mathsf{c}_{j}$ is such that

• •

$a$ is the caller in the call $\mathsf{c}_{j}$,

• •

$\psi_{j}\in\mathcal{L}^{a}_{1}$ and all atomic formulas used in $\psi$ start with $F_{a}$.

If $m=0$, the program is empty.

We call each such construct $\psi\to\mathsf{c}$ a rule and refer in this context to $\psi$ as a guard. Intuitively, $*$ denotes a repeated execution of the rules, one at a time, where each time non-deterministically a rule is selected whose guard is true.

By a distributed epistemic gossip protocol, from now on just a gossip protocol, we mean a parallel composition of component programs, one for each agent. We call a gossip protocol propositional if all guards in it are propositional, i.e., are from the language $\mathcal{L}_{p}$.

We presuppose that in each gossip protocol the agents are the nodes of a directed graph (digraph) and that each call $ab$ is allowed only if $a\to b$ is an edge in the digraph. A minimal digraph that satisfies this assumption is uniquely determined by the syntax of the protocol. Given that the aim of each gossip protocol is that all agents become experts it is natural to assume that this digraph is connected.

Here are two examples of gossip protocols to which we shall return later.

Example 2

In [11] the following correct gossip protocol, called Learn New Secrets (LNS in short), for complete graphs was proposed. In the syntax of [4] used here it is propositional, as it has the following program for agent $i$:

[TABLE]

Informally, agent $i$ calls agent $j$ if agent $i$ is not familiar with $j$’s secret. $\Box$

Example 3

In [11] also the following correct gossip protocol, called Hear My Secret (HMS in short), for complete graphs was proposed. In the syntax of [4] it has the following program for agent $i$:

[TABLE]

Informally, agent $i$ calls agent $j$ if agent $i$ does not know whether $j$ is familiar with his secret. $\Box$

Consider a gossip protocol $P$ that is a parallel composition of the component programs $*[[]^{m_{a}}_{j=1}\ \psi^{a}_{j}\to\mathsf{c}^{a}_{j}]$, one for each agent $a\in\mathsf{A}$.

The computation tree of $P$ is a directed tree defined inductively as follows. Its nodes are call sequences and its root is the empty call sequence $\epsilon$. Further, if $\bm{\mathsf{c}}$ is a node and for some rule $\psi^{a}_{j}\to\mathsf{c}^{a}_{j}$ we have $\bm{\mathsf{c}}\models\psi^{a}_{j}$, then $\bm{\mathsf{c}}.\mathsf{c}^{a}_{j}$ is a node that is a direct descendant of $\bm{\mathsf{c}}$. Intuitively, the arc from $\bm{\mathsf{c}}$ to $\bm{\mathsf{c}}.\mathsf{c}^{a}_{j}$ records the effect of the execution of the rule $\psi^{a}_{j}\to\mathsf{c}^{a}_{j}$ performed after the call sequence $\bm{\mathsf{c}}$ took place.

By a computation of a gossip protocol we mean a maximal rooted path in its computation tree. In what follows we identify each computation with the unique call sequence it generates. We say that the gossip protocol $P$ is partially correct if for all leafs $\bm{\mathsf{c}}$ of the computation tree of $P$

[TABLE]

i.e., if each agent is an expert in the gossip situation $\bm{\mathsf{c}}(\mathsf{root})$.

We say furthermore that $P$ terminates if all its computations are finite and say that $P$ is correct if it is partially correct and terminates.

We also consider two variants of termination. To define them we need a subsidiary notion. We call a rule enabled after a call sequence $\bm{\mathsf{c}}$ if its guard is true after $\bm{\mathsf{c}}$. Given a gossip protocol we say that an agent is enabled after a call sequence $\bm{\mathsf{c}}$ if one of the rules in its program is enabled.

We now stipulate that each finite computation is rule-fair and agent-fair. An infinite computation is rule-fair (resp. agent-fair) if all rules (resp. agents) that are enabled after infinitely many prefixes (in short, infinitely often) are selected infinitely often. We say that a gossip protocol $P$ rule-fairly terminates (resp. agent-fairly terminates) if all its rule-fair (resp. agent-fair computations) are finite. Agent-fairness was introduced in [4], where it was simply called fairness, while rule-fairness was introduced in [8] and further studied in [9].

7 Open problems about the gossip protocols

We begin with the following problem.

Problem 5

Characterize the class of graphs for which correct propositional gossip protocols exist.

Note that the LNS protocol from Example 2 shows that this class of graphs include all complete digraphs. However, as we will show in Theorem 7.3, star graphs do not belong to this class. We conjecture that any digraph whose complement of its set of edges contains a directed cycle does not have this property.

Comments

For further discussion it is useful to introduce some terminology. We say that a gossip protocol is for arbitrary connected digraphs if each agent $a$ can only call the agents from the set $N_{a}$ of its in-neighbours. In such gossip protocols the underlying digraph is a parameter that can be uncovered from the sets $N_{a}$. If the underlying digraph is supposed to be complete, we say that the gossip protocol is parametric. So in both cases we actually deal with a ‘parametrized’ gossip protocol, which is a template for an infinite set of gossip protocols.

For example, in [8] and [9] a correct gossip protocol with the following program for agent $i$ was considered:

[TABLE]

Informally, agent $i$ calls a neighbour $j$ if $i$ is familiar with some secret (here $S$) and he does not know whether $j$ is familiar with it. This gossip protocol is for arbitrary connected digraphs. However, it is not propositional.

In Example 2 the LNS gossip protocol was introduced. It is parametric and is both correct and propositional. However, its counterpart for arbitrary connected digraphs, so with the program

[TABLE]

for agent $i$, is obviously incorrect. Indeed, for the graph

i$$j$$k

it terminates after the calls $ij$, $jk$ with the agent $i$ not being an expert.

In turn, a natural gossip protocol Exp for arbitrary connected digraphs, with the program

[TABLE]

for agent $i$, is obviously partially correct but it does not terminate, as initially a fixed call $ij$, with $j\in N_{i}$, can be repeated indefinitely.

In [9] we proved that the Exp gossip protocol agent-fairly terminates in the case of rings. However, this is not the case in general. Indeed take the graph

i$$j$$k$$l

Then $(ij,ji,kl,lk)^{*}$ is an infinite agent-fair computation.

On the other hand, the following result holds. It generalizes the above result of [9] since for the case of rings the program for each agent has just one guard and consequently the notions of agent-fairness and rule-fairness coincide.

Theorem 1

The gossip protocol $Exp$ for arbitrary connected digraphs rule-fairly terminates.

Proof 7.2**.**

Suppose otherwise. Consider an infinite rule-fair computation $\xi$. We say that an agent $i$ becomes an expert in $\xi$ if for some element $\bm{\mathsf{c}}$ of $\xi$ we have $\bm{\mathsf{c}}\models\text{Exp}_{i}$.

As some agent $i$ does not become an expert in $\xi$, there is a secret $J$ that $i$ does not learn in $\xi$. Let i=i_{1},i_{2},\mbox{\ldots},i_{h}=j be a path connecting agent $i$ with $j$. By rule-fairness the call $i_{1}i_{2}$ takes place infinitely often. Hence agent $i_{2}$ does not become an expert in $\xi$ and consequently by rule-fairness the call $i_{2}i_{3}$ takes place infinitely often. Repeating this argument we conclude that each call $i_{g}i_{g+1}$, where g\in\{1,\mbox{\ldots},h-1\}, takes place infinitely often in $\xi$. So the call sequence i_{h-1}i_{h},i_{h-2}i_{h-1},\mbox{\ldots},i_{1}i_{2}, possibly interspersed with other calls, exists in $\xi$. After the last call agent $i$ learns the secret $J$, which yields a contradiction.

We now show that for a natural class of connected graphs no correct propositional gossip protocol exists.

Theorem 7.3**.**

Suppose that the agents form a star graph, so a graph in which some agent, say $a$, is present in all edges. Then no correct propositional gossip protocol exists.

Proof 7.4**.**

We begin by making two simple observations.

Claim 1**.**

Consider a propositional gossip protocol $P$. Suppose that $\bm{\mathsf{c}},\mathsf{c},\bm{\mathsf{d}},\mathsf{d}$ is a prefix of a computation of $P$ such that some agent $a$

• •

is involved in the call $\mathsf{c}$,

• •

is not involved in any call in $\bm{\mathsf{d}}$, and

• •

is a caller in $\mathsf{d}$.

Then also $\bm{\mathsf{c}},\mathsf{c},\mathsf{d}$ is a prefix of a computation of $P$.

Proof 7.5**.**

Consider the guard $\phi$ associated with the call $\mathsf{d}$. By assumption on $P$, $\phi$ is a propositional formula built out of the atomic formulas of the form $F_{a}S$. By assumption on $\bm{\mathsf{d}}$ the truth of these atomic formulas is not affected by any call in $\bm{\mathsf{d}}$. So the truth value of $\phi$ before and after the call sequence $\bm{\mathsf{d}}$ is the same. But $\phi$ is true just after this call sequence, so it is also true just before it. This shows that $\mathsf{d}$ can be performed immediately after $\mathsf{c}$.

Claim 2**.**

Let $\xi$ be a computation of a terminating propositional gossip protocol. If an agent, say $a$, becomes an expert after the call $\mathsf{c}$, then $a$ is not a caller in any call that follows $\mathsf{c}$ in $\xi$.

Proof 7.6**.**

Suppose otherwise. Let $\mathsf{d}$ be such a call in $\xi$ and let $\phi$ be the corresponding guard. This call does not affect the set of gossips agent $a$ is familiar with since this set as of the call $\mathsf{c}$ equals $\mathsf{Sec}$. By assumption $\phi$ is a propositional formula built out of the atomic formulas of the form $F_{a}S$, so after the call $\mathsf{d}$ the formula $\phi$ remains true. Hence the call $\mathsf{d}$ can be indefinitely repeated, which shows that the considered protocol does not terminate.

Let now $G$ be the considered star graph with an agent $a$ present in all edges. Suppose by contradiction that a correct propositional gossip protocol $P$ for $G$ exists. Let $\xi$ be a computation of $P$. Then agent $a$ is involved in all calls in $\xi$. Let $\mathsf{c}^{\prime}$ be the call after which $a$ became an expert and let $\mathsf{c}$ be the call that precedes $\mathsf{c}^{\prime}$ in $\xi$. By assumption the call $\mathsf{c}$ concerns agent $a$ and some agent $b$ not involved in the call $\mathsf{c}^{\prime}$. After the call $\mathsf{c}^{\prime}$ agent $b$ is not yet an expert, hence it is involved in $\xi$ in another call. Let $\mathsf{d}$ be the first such call.

So for some call sequences $\bm{\mathsf{c}}$ and $\bm{\mathsf{d}}$, we have that $\bm{\mathsf{c}},\mathsf{c},\bm{\mathsf{d}},\mathsf{d}$ is a prefix of $\xi$. Agent $b$ is not involved in any calls in $\bm{\mathsf{d}}$ and by Claim 2 it is also the caller in $\mathsf{d}$. So by Claim 1 also $\bm{\mathsf{c}},\mathsf{c},\mathsf{d}$ is a prefix of a computation, say $\chi$, of $P$. Since both $\mathsf{c}$ and $\mathsf{d}$ involve the same pair of agents, after the second call the set of gossips of agent $b$ does not change. Hence in $\chi$ the guard $\phi$ remains true after $\mathsf{d}$ and consequently this call can be indefinitely repeated. So $P$ does not terminate.

One of the early results, see for instance [32], is that for $n\geq 4$ agents at least $2n-4$ phone calls are needed to reach a situation in which each agent is an expert. Further, it is easy and well-known that this final situation can be reached using $2n-4$ calls. Indeed, assume that the set of agents is \{a,b,c,d,i_{1},\mbox{\ldots},i_{n-4}\}, where $n\geq 4$, (if $n=4$ then there are no $i_{j}$ agents) and take the following call sequence

[TABLE]

Problem 7.7**.**

Prove that the lower bound $2n-4$ cannot be achieved for the gossip protocols. In other words, prove that every correct gossip protocol for $n\geq 4$ agents generates computations of length $>2n-4$.

Comments

We show that this problem can be solved for $n=4$. To prove it we need the following observations.

Lemma 7.8**.**

For all agents $a,b,c$ and all call sequences $\bm{\mathsf{c}}$ and all formulas $\phi$

[TABLE]

Consequently, the same equivalence holds for all formulas that are Boolean combinations of formulas of the form $K_{a}\phi$, so in particular for each guard $\psi$ used in a program for agent $a$.

Proof 7.9**.**

By definition $\bm{\mathsf{c}}\sim_{a}\bm{\mathsf{c}},bc$, which implies the claim.

This note states that the calls in which agent $a$ is not involved have no effect on the truth of the guards used in the programs for agent $a$. This clarifies the syntax of the guards. If we allowed in guards for agent $a$ formulas of the form $F_{b}C$ as conjuncts, this natural and desired property would not hold anymore. Indeed, for $\bm{\mathsf{c}}=\epsilon$ we have $\bm{\mathsf{c}},bc\models F_{b}C$, while $\bm{\mathsf{c}}\not\models F_{b}C$.

We also need the following observation that confirms the intuition that two calls involving different pairs of agents can be executed in an arbitrary order.

Lemma 7.10**.**

Consider a protocol $P$. Let $a,b,c,d$ be four agents such that for some call sequences $\bm{\mathsf{c}}$ and $\bm{\mathsf{d}}$ we have that $\bm{\mathsf{c}},ab,cd,\bm{\mathsf{d}}$ is a computation of $P$. Then also $\bm{\mathsf{c}},cd,ab,\bm{\mathsf{d}}$ is a computation of $P$.

Proof 7.11**.**

Let $\phi_{a}$ be the guard that precedes the call $ab$ in the program for agent $a$ and $\phi_{c}$ the guard that precedes the call $cd$ in the program for agent $c$. We have $\bm{\mathsf{c}}\models\phi_{a}$ and $\bm{\mathsf{c}},ab\models\phi_{c}$. By Lemma 7.8

[TABLE]

and

[TABLE]

Hence $\bm{\mathsf{c}}\models\phi_{c}$ and $\bm{\mathsf{c}},cd\models\phi_{a}$. This means that $\bm{\mathsf{c}},cd,ab$ is a prefix of a computation of $P$.

Further, by the definition of the $\sim_{i}$ relations, for all agents $i$ and all call sequences $\bm{\mathsf{d}}^{\prime}$ we have $\bm{\mathsf{c}},ab,cd,\bm{\mathsf{d}}^{\prime}\sim_{i}\bm{\mathsf{c}},cd,ab,\bm{\mathsf{d}}^{\prime}$. Hence for all formulas of the form $K_{i}\phi$ we have

[TABLE]

and consequently for all guards $\phi$ preceding the calls in $\bm{\mathsf{d}}$ we have

[TABLE]

This concludes the proof.

The above observation also holds for infinite computations but we shall not need it in the sequel.

Finally, we need to reason about the following notion. We call a computation of a gossip protocol bad if some agent is involved in the first two calls of it.

Lemma 7.12**.**

Every gossip protocol admits bad computations.

Proof 7.13**.**

Fix a gossip protocol $P$ and consider its computation $\xi$ that is not bad. By appropriate renaming we can assume that it begins with $ab,cd$. Let $\mathsf{c}$ be the third call in $\xi$ and $\psi$ the guard associated in $P$ with the call $\mathsf{c}$. By assumption we have $(ab,cd)\models\psi$. Four cases arise.

Case 1*. Agent $a$ is the caller in $\mathsf{c}$.*

We have $ab,cd\sim_{a}ab$, so by Lemma 7.10

[TABLE]

and hence $ab\models\psi$. In other words, the call $\mathsf{c}$ can be executed in $P$ directly after the call $ab$, that is, $ab,\mathsf{c}$ is a prefix of a computation of the protocol $P$.

Case 2*. Agent $b$ is the caller in $\mathsf{c}$.*

We have $ab,cd\sim_{b}ab$, so, as in Case 1, $ab\models\psi$. Hence the call $\mathsf{c}$ can be executed in $P$ directly after the call $ab$, that is, $ab,\mathsf{c}$ is a prefix of a computation of the protocol $P$.

Case 3*. Agent $c$ is the caller in $\mathsf{c}$.*

By Lemma 7.10 the calls $ab$ and $cd$ can be reversed in $\xi$, hence a computation of $P$ exists that begins with $cd,ab,\mathsf{c}$. So $(cd,ab)\models\psi$. We have $cd,ab\sim_{c}cd$, so, as in Case 1, $cd\models\psi$. Hence the call $\mathsf{c}$ can be executed in $P$ directly after the call $cd$, that is, $cd,\mathsf{c}$ is a prefix of a computation of the protocol $P$.

Case 4*. Agent $d$ is the caller in $\mathsf{c}$.*

As in Case 3 a computation of $P$ exists that begins with $cd,ab,\mathsf{c}$. We have $(cd,ab)\models\psi$ and $cd,ab\sim_{d}cd$, so, as in Case 3, $cd\models\psi$. Hence the call $\mathsf{c}$ can be executed in $P$ directly after the call $cd$, that is, $cd,\mathsf{c}$ is a prefix of a computation of the protocol $P$.

Theorem 7.14**.**

Every correct gossip protocol for 4 agents generates computations of length $>4$.

Proof 7.15**.**

Suppose that $\mathsf{A}=\{a,b,c,d\}$. Consider a correct protocol $P$.

We first show that each bad computation $\xi$ is of length $>4$. There are 4 agents, so some agent, say $a$, is involved neither in the first nor the second call of $\xi$. So after these two calls none of the agents $b,c,d$ is familiar with the secret of agent $a$. Each call increases the number of agents familiar with the secret of agent $a$ by at most 1. So at least three more calls are needed to obtain a situation which all agents are familiar with the secret of $a$. We conclude that $\xi$ is of length at least 5.

The conclusion now follows by Lemma 7.12.

Problem 7.7 concerned the lower bound $2n-4$. It is useful to note that the lower bound $2n-3$ can be achieved. So for $n=4$ the precise bound is 5.

Theorem 7.16**.**

Suppose that $n\geq 4$. There exists a correct gossip protocol for $n$ agents all computations of which are of length $2n-3$.

Proof 7.17**.**

Assume that \mathsf{A}=\{a_{1},\mbox{\ldots},a_{n}\}. We use the observation due to [10] that the following call sequence results in all agents being experts:

[TABLE]

In this call sequence first agent $a_{1}$ calls all other agents and subsequently calls them again except agent $a_{n-1}$. But the exact order of the calls in each phase is not important. This allows us to use a gossip protocol with a simple structure.

We choose an arbitrary agent $a\in\mathsf{A}$ and select for it the following program:

[TABLE]

The programs for the other agents are empty.

Note that after each call the corresponding guard becomes false. Further, by the form of the above program in every computation of the protocol first $n-1$ calls of $a$ take place, each to a different agent. These calls correspond to the first set of guards and are executed in an arbitrary order.

After the last of these $n-1$ calls, say $ab$, agents $a$ and $b$ both become experts and agent $a$ knows it. So from this moment on the guard $\text{Exp}_{a}\land\neg K_{a}\text{Exp}_{b}$ is false and the second call $ab$ does not take place. Hence the remaining part of the computation consists of $n-2$ calls of agent $a$, each to a different agent from $\mathsf{A}\setminus\{a,b\}$. These calls correspond to the second set of guards and are executed in an arbitrary order, as well.

After these $2n-3$ calls all agents become experts and the protocol terminates.

Problem 7.18**.**

Prove that the lower bound $2n-3$ cannot be achieved by a correct propositional gossip protocol.

8 Open problems about verification of gossip protocols

We studied in [5] the computational complexity of partial correctness and termination of gossip protocols and showed that when in guards only formulas from the sublanguage $\mathcal{L}_{1}$ are used both problems are in $\text{coNP}^{\text{NP}}$. This brings us naturally to the following problems.

Problem 8.19**.**

What is the exact computational complexity of checking whether a given gossip protocol

• •

is partially correct,

• •

terminates?

We conjecture that both problems are $\text{coNP}^{\text{NP}}$-complete. This problem can be generalized as follows. In generalized gossiping the aim is to reach a gossip situation in which some given formula $\phi\in\mathcal{L}$ is true, possibly other than $\bigwedge_{a\in\mathsf{A}}Exp_{a}$. We say that a a gossip protocol $P$ is $\phi$-partially correct if for all leafs $\bm{\mathsf{c}}$ of the computation tree of $P$

[TABLE]

For example the HMS gossip protocol from Example 3 is $\bigwedge_{i,j\in\mathsf{A}}K_{i}F_{j}I$-partially correct, since upon termination all the guards are false. In contrast, this protocol is not $\bigwedge_{i,j\in\mathsf{A}}K_{i}\,\text{Exp}_{j}$-partially correct. Indeed, assume three agents, $a,b,c$, and the call sequence $(ab,ac,bc)$ after which this gossip protocol terminates. However, $(ab,ac,bc)\models K_{a}\,\text{Exp}_{b}$ does not hold.

Problem 8.20**.**

What is the complexity of checking whether for a given formula $\phi\in\mathcal{L}$ a given gossip protocol is $\phi$-partially correct?

These questions can also be asked for parametrized gossip protocols.

Problem 8.21**.**

What is the complexity of checking whether a given gossip protocol for arbitrary connected digraphs

• •

is partially correct,

• •

terminates?

Next problem concerns relation between two gossip protocols. To define it we need to discuss the computation trees.

We say that two unordered trees are equal if they become identical after some possible rearrangement of the children of each node in these trees.111This rearrangement is allowed because computational trees are unordered. If we fix an order of children, e.g., subject to lexicographic order on the last call, then a computational tree for a given protocol is unique and this problem when checking for the equality of two trees no longer occurs. Given a tree $T$, any removal of branches from $T$ yields a subtree of $T$.

Consider now two gossip protocols $P$ and $P^{\prime}$. We say that $P$ can simulate $P^{\prime}$ if the computational tree of $P^{\prime}$ is equal to some subtree of $P$. If both $P$ can simulate $P^{\prime}$ and $P^{\prime}$ can simulate $P$ then we say that they are bisimilar. Clearly the computational trees of two bisimilar gossip protocols are equal.

Example 8.22**.**

Consider the LNS and HMS gossip protocols introduced in Examples 2 and 3.

Assume that there are only three agents, $a,b,c$. There are only four maximal call sequences that can be generated by LNS beginning with the call $ab$, namely:

[TABLE]

For every other starting call $ac$, $ba$, $bc$, $ca$, or $cb$, there are analogous four such maximal call sequences. It is easy to check that all these call sequences can be generated by HMS. So for three agents HMS can simulate LNS.

However, HMS can also generate the call sequence $ab.bc.ca$ that LNS cannot, so these two protocols are not bisimilar. $\Box$

We actually conjecture that HMS can simulate LNS for any number of agents. This naturally suggests the following two problems.

Problem 8.23**.**

What is the exact complexity of checking for two given parametric protocols whether

• •

one simulates the other,

• •

they are bisimilar?

Problem 8.24**.**

What is the exact computational complexity of checking for two gossip protocols $P$ and $P^{\prime}$ whether

• •

$P$* simulates $P^{\prime}$,*

• •

$P$* and $P^{\prime}$ are bisimilar?*

Comments

The following result provides some insights into the last problem.

Theorem 8.25**.**

Checking whether a gossip protocol $P$ can simulate another protocol $P^{\prime}$ can be done in exponential time.

To prove it we need some preparatory results. We call the second call $\mathsf{c}$ in a call sequence $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}.\bm{\mathsf{c}}_{3}$ epistemically redundant if $\bm{\mathsf{c}}_{1}.\mathsf{c}(\mathsf{root})=\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}(\mathsf{root})$. In [5] we established the following result (as Lemma 6) showing that removing an epistemically redundant call does not affect the truth of any formula from $\mathcal{L}_{1}$.

Lemma 8.26**.**

If $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}.\bm{\mathsf{c}}_{3}$ is a call sequence where the second call $\mathsf{c}$ is epistemically redundant, then for any formula $\psi\in\mathcal{L}_{1}$:

[TABLE]

We say that a call $\mathsf{c}$ that appears in a call sequence $\bm{\mathsf{c}}$ is productive if $\bm{\mathsf{c}}_{1}(\mathsf{root})\neq\bm{\mathsf{c}}_{1}.\mathsf{c}(\mathsf{root})$, where for some call sequences $\bm{\mathsf{c}}_{1}$ and $\bm{\mathsf{c}}_{2}$, $\bm{\mathsf{c}}=\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}$.

Further, we call a subsequence $\bm{\mathsf{c}}_{2}$ of a call sequence $\bm{\mathsf{c}}$ stationary if

[TABLE]

where $\bm{\mathsf{c}}=\bm{\mathsf{c}}_{1}.\bm{\mathsf{c}}_{2}.\bm{\mathsf{c}}_{3}$ for some call sequences $\bm{\mathsf{c}}_{1}$ and $\bm{\mathsf{c}}_{3}$, and for some $k\geq 1$, \bm{\mathsf{c}}_{2}=\mathsf{c}_{1}.\mathsf{c}_{2}\mbox{\ldots}\mathsf{c}_{k}.

Recall that $n$ is the number of agents.

Lemma 8.27**.**

Every call sequence contains at most $n^{2}-n$ productive calls.

Proof 8.28**.**

The minimal total number of secrets in a gossip situation is $n$, which is achieved in the initial gossip situation $\mathsf{root}$. In turn, the maximal total number of secrets is $n^{2}$, which is achieved in the gossip situation in which every agent is an expert. After each productive call at least one agent learns a new secret. So in a given call sequence there can be at most $n^{2}-n$ productive calls.

Lemma 8.29**.**

Every call sequence $\bm{\mathsf{c}}$ of length $\geq n^{4}$ has a stationary subsequence of length $\geq n^{2}$.

Proof 8.30**.**

Split $\bm{\mathsf{c}}$ into a sequence of $n^{2}$ subsequences, each of length at least $n^{2}$. Suppose none of these subsequences is stationary. Then each of them contains a productive call. So $\bm{\mathsf{c}}$ contains at least $n^{2}$ productive calls, which contradicts Lemma 8.27.

Corollary 8.31**.**

Every call sequence $\bm{\mathsf{c}}$ of length $\geq n^{4}$ contains an epistemically redundant call.

Proof 8.32**.**

Take a stationary subsequence $\bm{\mathsf{c}}_{1}$ of $\bm{\mathsf{c}}$ guaranteed by Lemma 8.29. There are at most $n^{2}-n$ different calls, so some call $\mathsf{c}$ appears in $\bm{\mathsf{c}}_{1}$ at least twice. Its second occurrence in $\bm{\mathsf{c}}_{1}$ is then epistemically redundant in $\bm{\mathsf{c}}$.

Next lemma shows that lack of simulation entails existence of a specific call sequence of a bounded length.

Lemma 8.33**.**

If $P$ cannot simulate $P^{\prime}$ then there exist a call sequence $\bm{\mathsf{c}}$ of length $\leq n^{4}$ that can be generated by $P^{\prime}$, but not by $P$.

Proof 8.34**.**

If $P$ cannot simulate $P^{\prime}$ then take a shortest rooted path in the computation tree of $P^{\prime}$ that does not exist in the computation tree of $P$. This path corresponds to some call sequence $\bm{\mathsf{c}}$.

Suppose by contradiction that the length of $\bm{\mathsf{c}}$ exceeds $n^{4}$. By Corollary 8.31, $\bm{\mathsf{c}}$ can be partitioned into $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}.\bm{\mathsf{c}}_{3}.\mathsf{c}^{\prime}$ such that $\bm{\mathsf{c}}_{1}.\mathsf{c}(\mathsf{root})=\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}(\mathsf{root})$.

By Lemma 8.26 for any formula $\phi\in\mathcal{L}_{1}$ and a subsequence $\bm{\mathsf{c}}_{4}$ of $\bm{\mathsf{c}}_{3}$ we have

[TABLE]

By the definition of $\bm{\mathsf{c}}$ the call sequence $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}.\bm{\mathsf{c}}_{3}$ can be generated by $P$, while the call sequence $\bm{\mathsf{c}}$ cannot. So $P$ does not have a rule $\phi\to\mathsf{c}^{\prime}$ such that $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}.\bm{\mathsf{c}}_{3}\models\phi$.

Further, by (5) the call sequence $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\bm{\mathsf{c}}_{3}$ can be generated by $P$, while, again by (5), the call sequence $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\bm{\mathsf{c}}_{3}.\mathsf{c}^{\prime}$ (so $\bm{\mathsf{c}}$ with the second indicated occurence of $\mathsf{c}$ omitted) cannot.

On the other hand, by assumption $\bm{\mathsf{c}}$ can be generated by $P^{\prime}$, so $P^{\prime}$ has a rule $\phi^{\prime}\to\mathsf{c}^{\prime}$ such that $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}.\bm{\mathsf{c}}_{3}\models\phi^{\prime}$. Together with (5) this implies that also $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\bm{\mathsf{c}}_{3}.\mathsf{c}^{\prime}$ can be generated by $P^{\prime}$. This yields a contradiction with the definition of $\bm{\mathsf{c}}$.

Proof of Theorem 8.25. To show that $P$ can simulate $P^{\prime}$ it suffices by Lemma 8.33 to check that each call sequence of length $\leq n^{4}$ which can be generated by $P^{\prime}$ can also be generated by $P$.

We showed in [5] that checking for a given call sequence $\bm{\mathsf{c}}$ and a formula $\phi\in\mathcal{L}_{1}$ whether $\bm{\mathsf{c}}\models\phi$ can be done in exponential time (actually in $\text{coNP}^{\text{NP}}$ time). This implies that checking whether a given call sequence $\bm{\mathsf{c}}$ of length $\leq n^{4}$ can be generated by a gossip protocol can be done in exponential time.

Consequently, checking whether $P$ can simulate $P^{\prime}$ can be done in exponential time, as well, since there are exponentially many call sequences of length $\leq n^{4}$. $\Box$

Corollary 8.35**.**

Checking whether gossip protocols $P$ and $P^{\prime}$ are bisimilar can be done in exponential time.

As a side remark of independent interest we conclude the paper with the following consequence of Corollary 8.31.

Corollary 8.36**.**

If a gossip protocol terminates then all its computations are of length $<n^{4}$.

To prove we use the following result from [9] that for the case of formulas from $\mathcal{L}_{1}$ is actually a special case of Lemma 8.26.

Lemma 8.37** (Stuttering).**

Suppose that $\bm{\mathsf{c}}:=\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}$ and $\bm{\mathsf{d}}:=\bm{\mathsf{c}}_{1}.\mathsf{c}.\mathsf{c}.\bm{\mathsf{c}}_{2}$. Then for all formulas $\phi\in\mathcal{L}$, $\bm{\mathsf{c}}\models\phi$ iff $\bm{\mathsf{d}}\models\phi$.

Proof of Corollary 8.36. Consider a finite computation of length $\geq n^{4}$ and the corresponding call sequence $\bm{\mathsf{c}}$. By Corollary 8.31, $\bm{\mathsf{c}}$ begins with a call sequence $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}$, where $\bm{\mathsf{c}}_{1}.\mathsf{c}(\mathsf{root})=\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}(\mathsf{root})$.

Let $\psi\to\mathsf{c}$ be the rule used in the considered gossip protocol to generate the second occurrence of the call $\mathsf{c}$. Then $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}\models\psi$ and by Lemma 8.26 for $\bm{\mathsf{c}}_{3}=\epsilon$ we have $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}\models\psi$.

Hence by the repeated use of the Stuttering Lemma 8.37 for $\bm{\mathsf{c}}_{2}=\epsilon$ and all $i\geq 1$, $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}^{i}\models\psi$. Consequently, after the call sequence $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}$ is generated, the rule $\psi\to\mathsf{c}$ can be repeatedly applied. Hence $\bm{\mathsf{c}}_{1}.\mathsf{c}.\bm{\mathsf{c}}_{2}.\mathsf{c}^{\omega}$ is an infinite sequence of calls that corresponds to an infinite computation. $\Box$

Acknowledgements

We thank reviewers for useful suggestions concerning the presentation. The second author was partially supported by EPSRC grants EP/M027287/1 and EP/P020909/1.