On the Computational Complexity of Gossip Protocols

1 Introduction

The aim of this paper is to study natural complexity questions concerning gossip protocols. The set up of these protocols is the following. Each agent holds a secret initially known only to him. During the communications (for example phone calls) the participating agents share the secrets they know. The aim of the gossip protocols is to arrive at a situation in which all agents know all secrets. One of the early results established by a number of authors in the seventies, e.g., [Tijdeman, 1971], is that for n ≥ 4 agents 2n - 4 phone calls is necessary and sufficient to reach such a final situation. However, the protocols solving the problem using 2n - 4 phone calls are centralized in the sense that they require a centralized scheduler. We are concerned here with the distributed gossip protocols that were introduced in [Attamah et al., 2014b] and further studied with different type of calls in [Apt et al., 2016]. These protocols use as guards epistemic formulas and thus are examples of knowledge based programs introduced in [Fagin et al., 1997]. The formulation of distributed gossip protocols as knowledge-based programs considerably simplifies the task of their verification. The reason is that these protocols are defined simply as a parallel composition of simple loops in which the agents repeatedly evaluate a guard, which is an epistemic formula, and subsequently perform a corresponding call. As a result implementability of the protocol can be reduced

Dominik Wojtczak

University of Liverpool, UK d.wojtczak@liv.ac.uk

to the problem of decidability of semantics of the underlying epistemic language and its partial correctness and termination to the problem of decidability of truth for this language.

In [Apt and Wojtczak, 2016] we established that such distributed epistemic gossip protocols (in short, protocols) are implementable, i.e., the problem of evaluating a guard after a sequence of calls is decidable (implicitly shown there to be in EXPTIME), and that the problems of their partial correctness and termination are also decidable (implicitly shown there to be in 3-EXPTIME) in the setup when during the calls the agents exchange all their secrets (so-called push-pull type of calls) and the underlying topology of the network is a clique.

In this paper we sharpen this analysis and study the computational complexity of these three problems. We show that for any monotonic type of calls and network topology, the implementability of a protocol is an P NP ‖ -complete problem and checking its partial correctness and termination is in coNP NP .

Related work. Gossip protocols have been studied for more than forty years and have been successful in various domains, e.g., communication networks [Hedetniemi et al., 1988], computation of aggregate information [Kempe et al., 2003], and data replication [Ladin et al., 1992]. A more recent account is given in the book [Hromkovic et al., 2005] and in [Kermarrec and van Steen, 2007]. In these references gossip protocols are viewed as parallel, probabilistic and/or distributed programs.

Epistemic gossip protocols were studied in a number of recent publications. In [Attamah et al., 2014a] a tool is discussed that given a high level description of an epistemic protocol in the setting of [Attamah et al., 2014b] generates the characteristics of the protocol. The calls considered there differ from the ones considered here, so this approach is not applicable to our setting. In turn, in [van Ditmarsch et al., 2017] dynamic distributed gossip protocols are studied in which the calls allow the agents not only to share the secrets but also to transmit the links. The purpose of the paper is to characterize such protocols in terms of the class of graphs for which they terminate. Such protocols then differ from the ones considered here, which are static. Next, [Herzig and Maffre, 2017] and [Cooper et al., 2016b] consider gossip protocols that aim at achieving higher-order shared knowledge. Finally, in [Cooper et al., 2016a] gossip protocols are expressed as an instance of multi-agent epistemic planning and subsequently translated into the classical planning language PDDL. In parallel with this work, we proved in [Apt and Wojtczak, 2017b] the decidability of fair termination for gossip protocols, while in [Apt and Wojtczak, 2017a] established first results concerning their extension with the common knowledge operator.

Plan. The paper is organized as follows. In the next two sections we recall the syntax and semantics of the gossip protocols considered in [Apt et al., 2016]. The set up is more general since a broader definition of a call is adopted. To illustrate the considered protocols we discuss in Section 5 a protocol over an undirected graph, together with its partial correctness and termination proofs.

Next, in Section 6, we show that the following problem is NP-complete:

Can a given distribution of sets of secrets among the agents be the outcome of a sequence of calls?

This problem turns out to be crucial for the computational complexity analysis of the partial correctness and of termination that is carried out in Section 7. Finally, in Section 8 we discuss some open problems.

2 Syntax

2.1 Calls and Call Types

Throughout the paper we assume a fixed finite set A of at least three agents that is an implicit parameter in all considerations. We assume that at the beginning each agent holds exactly one secret and that there exists a bijection between the set of agents and the set of secrets. We denote by S the set of all secrets. One could consider other initial secret distributions and the set of secrets to be larger than the set of agents. This would not alter our results, but would make the notation harder to read, so we opted for this simpler set up. Our aim is to analyse what the agents know after a sequence of calls took place. So first we introduce different type of calls and then consider an epistemic language allowing us to refer to agents' knowledge.

A call type is a pair ▷◁ = (E▷◁, f▷◁), where E▷◁ ⊆ A × A and f▷◁ : 2A ×2A → 2A ×2A . Intuitively, f▷◁ is the transformer of the sets of secrets that are familiar to the caller and callee. Each call is a triple x▷◁ y, where agent x is the caller, agent y is the callee y, and ▷◁ is the type of the call. A call x ▷◁ y is feasible if (x, y) ∈ E▷◁. Calls are denoted by c, d. Abusing notation we write x ∈ c to denote that agent x is one of the two agents involved in the call c.

In other words, (A,E▷◁) is a directed graph and its edges specify which agent can ▷◁-call another. In turn, f▷◁ specifies the outcome of such a call given the sets of secrets the caller and callee are familiar with. In [Apt et al., 2016] the following call types were studied.

• Push-pull calls, written as x ◦ y or simply xy, where agents x and y exchange all their secrets. In this case we define f◦(X, Y ) := (X ∪ Y, X ∪ Y ), where X and Y are, respectively, the set of secrets the caller and callee are familiar with before this call takes place.
• Push calls, written as x ▷ y, where only the caller x passes his secrets to the callee y. In this case we define f▷(X, Y ) := (X, X ∪ Y ).
• Pull calls, written as x ◁ y, where only the caller x learns the secrets of the callee y. In this case we define f◁(X, Y ) := (X ∪ Y, Y ).

In this paper we generalize the setting and allow the outcome of a call to be any polynomially computable function, f , which is also monotonic, i.e., no agent ever forgets his secrets. Formally, if f(X, Y ) = (X′ , Y ′ ) then X ⊆ X′ and Y ⊆ Y ′ .

An example of a call type captured by this definition is the one in which during each call each agent reveals only one secret (e.g., the least one in some ordering on S). Our results also hold for call types with non-deterministic outcomes as long as there are polynomially many of them. We opted for deterministic call types only to keep the definitions simple.

2.2 Epistemic Logic

We consider formulas in a simple epistemic language L defined by the following grammar:

where p ∈ S and a ∈ A. Each secret is viewed as a distinct constant. We denote the secret of agent a by A, the secret of agent b by B and so on and sometimes implicitly switch between an agent and its secret.

We read Fap as 'agent a is familiar with the secret p' and Kaφ as 'agent a knows that formula φ is true'. So Fap is an atomic formula, while Kaφ is a compound formula. In fact, all atomic formulas of L have the form Fap.

In what follows we shall distinguish the following sublanguages of L:

• L0, its propositional part, which consists of the formulas that do not use the Ka modalities;
• L1, which consists of the formulas without the nested use of the Ka modalities;
• La1 , where a ∈ A is a fixed agent, which consists of the formulas from L1 where the only modality is Ka.

3 Semantics

We now recall from [Apt et al., 2016] semantics of the epistemic formulas. To this end we recall first the concept of a gossip situation.

3.1 Gossip Situations

A gossip situation (in short a situation) is a sequence s = (Qa)a∈A, where Qa ⊆S for each agent a. Intuitively, Qa is the set of secrets agent a is familiar with in situation s. The initial gossip situation is the one in which each Qa equals {A} (recall that A is the secret of agent a) and is denoted by root. This situation reflects the fact that initially each agent is familiar only with his own secret. We say that an agent a is an expert in a situation s if he is familiar in s with all the secrets, i.e., if Qa = S.

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, then root = A.B.C and the gossip situation ({A, B}, {A, B}, {C}) will be written as AB.AB.C.

Each feasible call transforms the current gossip situation by modifying the set of secrets the agents involved in the call are familiar with. Consider a gossip situation s := (Qd)d∈A. Then (a ▷◁ b)(s) := (Q′d )d∈A, where (Q′a , Q′b ) = f▷◁(Qa, Qb), and Q′c = Qc, for c ̸∈ {a, b}. This simply says that the only effect of a feasible call a▷◁ b is that the secrets of the involved agents, a and b, are shared according to f▷◁.

3.2 Call Sequences

In [Apt et al., 2016] computations of the gossip protocols were studied, so both finite and infinite call sequences were used. Here we focus on the finite call sequences as we are only interested in the semantics of epistemic formulas. So to be brief, unless explicitly stated, a call sequence is assumed to be finite. A call sequence is valid if each of its calls is feasible. Checking whether a call sequence is valid can easily be done in linear time, so from now on we assume that all considered call sequences are valid.

The empty call sequence is denoted by ϵ. We use c to denote a call sequence and C to denote the set of all finite (valid) call sequences. Given call sequences c and d and a call c we denote by c.c the outcome of adding c at the end of the sequence c and by c.d the outcome of appending the sequences c and d.

The result of applying a call sequence to a situation s is defined inductively by putting ϵ(s) := s and (c.c)(s) := c(c(s)).

Example 1 Let A = {a, b, c}. Consider the call sequence (ac, b ▷ c, a ◁ c) involving three different call types. It generates the following successive gossip situations starting from root: A.B.C ac -→ AC.B.AC b▷c -→ AC.B.ABC a◁b -→ ABC.B.ABC. Hence (ac, b ▷ c, a ◁ c)(root) = (ABC.B.ABC). ✷

3.3 GossipModels and Truth

A gossip situation is a set of possible combinations of secret distributions among the agents. As calls progress in sequence from the initial gossip situation, agents may be uncertain about which one of such secrets distributions is the actual one. This uncertainty is captured by appropriate equivalence relations on the call sequences.

Definition 1 A gossip model is a tuple M := (C, {∼a}a∈A ), where each ∼a⊆ C × C is the minimal relation satisfying the following conditions:

• ϵ ∼a ϵ,
• Suppose c ∼a d.
• (ii) If a ∈ c and c.c(root)a = d.c(root)a, then c.c ∼a

A gossip model with a designated call sequence is called a pointed gossip model.

For instance, by (i) we have ab, bc ∼a ab, bd. But we do not have bc, ab ∼a bd, ab since (bc, ab)(root)a = ABC ̸= ABD = (bd, ab)(root)a.

The following two properties of ∼a from [Apt et al., 2016] will be used in the sequel.

Fact 1 (i) Each ∼a is an equivalence relation.

Finally, we recall the definition of truth.

Definition 2 Let (M, c) be a pointed gossip model with M := (C, (∼a)a∈A) and c ∈ C. We define the satisfaction relation |= inductively as follows (clauses for Boolean connectives are as usual and omitted):

Further

When M |= φ we say that φ is true.

So a formula Fap is true whenever secret p belongs to the set of secrets agent a is familiar with in the situation generated by the designated call sequence c applied to the initial situation root. In turn, the knowledge operator is interpreted as is customary in epistemic logic, using the equivalence relations ∼a.

4 Gossip Protocols

In [Apt et al., 2016], as a follow up on [Attamah et al., 2014b], distributed epistemic gossip protocols were studied. 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 ∧a∈A FaA is true into one in which the formula ∧a,b∈A FaB is true. Let us recall their definition.

By a component program, in short a program, for an agent a we mean a statement of the form ∗[[]mj=1 ψj → cj ], where m > 0 and each ψj → cj is such that ψj ∈ La1 and a ∈ cj .

Given a formula ψ ∈ La1 and a call c, we call the construct ψ → c a rule and refer in this context to ψ as a guard. The symbol [] denotes a nondeterministic choice among the rules of a given agent, while ∗ denotes a repeated execution of the rules, one at a time, where each time a rule is selected whose guard is true. Finally, by a distributed epistemic gossip protocol, in short a gossip protocol, we mean a parallel composition of component programs, one for each agent.

Assume a gossip protocol P that is a parallel composition of the component programs ∗[[]ma j=1 ψa j → caj ], one for each agent a ∈ A.

The computation tree of P is defined as the (possibly infinite) set CP of (possibly infinite) call sequences c = c0, c1, . . . , cn, . . . such that:

• CP is closed under prefixes,
• for any call sequence (c0, c1, . . . , ci, ci+1) in it: for some a and j ∈ {1, . . .,ma} we have (M, (c0, . . . , ci)) |= ψa j and caj = ci+1.

In this case we say that a transition between (c0, c1, . . . , ci) and (c0, c1, . . . , ci, ci+1) took place due to the execution of the rule ψa j → caj .

By a computation of a gossip protocol we mean a maximal rooted path in its computation tree. We say that the gossip protocol P is partially correct if for all finite computations c of P: (M, c) |= ∧a,b∈A FaB, i.e., if each agent is an expert in the gossip situation c(root). Note that c is a finite computation iff (M, c) |= ∧a∈A ∧ma j=1 ¬ψa j . We call the formula ∧a∈A ∧ma j=1 ¬ψa j the exit condition of the gossip protocol P. So P is partially correct iff the implication

is true. We say furthermore that P terminates if all its computations are finite.

All gossip protocols studied in [Apt et al., 2016] use as guards only formulas from L1, that is in a program for agent a only guards from La1 are used.

5 Example Gossip Protocol

To illustrate the power of gossip protocols suppose that the agents are nodes of an undirected connected graph (V, E) and that the calls can take place only between agents connected by an edge. Let Ni denote the set of neighbours of node i.

Consider a gossip protocol with the following program for agent i:

Informally, agent i calls a neighbour j if i is familiar with some secret (here C) and he does not know whether j is familiar with it.

To prove its partial correctness consider the exit condition ∧(i,j)∈E ∧C∈S (FiC → KiFjC). For all agents i and j and secrets C, the formula KiFjC → FjC is true, so the exit condition implies ∧(i,j)∈E ∧C∈S (FiC → FjC).

Consider now an agent i and the secret J of agent j. Let j = i1, . . ., ih = i be a path that connects j with i. The above formula implies that for g ∈ {1, . . ., h - 1} we have ∧C∈S (Fig C → Fig+1 C). By combining these h-1 formulas we get ∧C∈S (FjC → FiC). But FjJ is true, so we conclude FiJ. Consequently ∧i,j∈A FiJ, as desired.

To prove termination it suffices to note that after each call ij the size of the set {(i, j,C) | ¬KiFjC} decreases.

6 Incomplete Gossiping Problem

In [Apt and Wojtczak, 2016], the following problem was stated and was shown to be decidable.

Definition 3 (INCOMPLETE GOSSIPING) Can a given gossip situation s = (Qd)d∈A be the outcome of a call sequence starting at root?

Despite it apparent simplicity, we show that INCOMPLETE GOSSIPING problem is NP-hard even if the only type of calls allowed is push-pull and everyone can call everybody else, i.e., the graph is a clique. This result is of independent interest as it connects with other computational problems. For instance, [Liben-Nowell, 2002] shows that computing the distance between two genomes can be reduced to the problem of computing the minimum number of calls necessary to reach a given gossip situation. In [Khuller et al., 2003], the same was shown for the problem of data migration for storage devices in the setting where only one secret is exchanged during a call.

We show the stated result by a reduction from the following TRIANGLE 3-COLORING problem.

Definition 4 (TRIANGLE 3-COLORING) The input is given as (V, T ) where V = {1, . . . , n} be a set of vertices and T = {(t1,0, t1,1, t1,2), . . . , (tm,0, tm,1, tm,2)} a set of m triangles, i.e., triplets of vertices. Let the set of colors be C = {0, 1, 2}.

The problem is defined as follows. Is it possible to color each vertex in V in such a way that each triangle is colored with three distinct colors, i.e., find a function c : V →C such that for each j ∈ T , k, l ∈ C, k ̸= l, we have c(tj,k) ̸= c(tj,l)?

Note that TRIANGLE 3-COLORING problem is NPcomplete - indeed, we can reduce from the standard NPcomplete problem of GRAPH 3-COLORING by adding a new fresh vertex to each edge, thus making it a triangle.

Theorem 1 The INCOMPLETE GOSSIPING problem is NPhard.

Proof. Let I = (V, T) be an instance of TRIANGLE 3COLORING. We will reduce it to an instance of INCOMPLETE GOSSIPING (AI, sI), where AI is a set of agents and sI is a gossip situation. First, we will describe (AI , sI). Then we will show the intended call sequence cI and give some intuition about the gadgets that we use. We then show that if I is triangle 3-colorable, then cI(rootAI ) = sI. In the last paragraph, we prove that our reduction is correct, i.e., if there exists c such that c(rootAI ) = sI, then I is triangle-3-colorable.

Reduction. Let I = (V, T) be an instance of TRIANGLE 3COLORING. Let the set of agents be AI = {Cc,v | c ∈ C, v ∈ V } ∪ {Ac,v | c ∈ C, v ∈ V } ∪ {Fc | c ∈ C} ∪ {Sv | v ∈ V }∪{Kj,k | j ∈ T, k ∈ C}∪{Lj,k | j ∈ T, k ∈ C}∪{Gv | v ∈ V } ∪ {Hj,k | j ∈ T, k ∈ C}.

For every c ∈ C, v ∈ V let us define color(c) = {Cc,v | v ∈ V } ∪ {Fc}, Gadget(v) = {Ac,v | c ∈ C} ∪ {Sv}, Fix = {Fc | c ∈ C} ∪ {Gv | v ∈ V } ∪ {Hj,k | j ∈ T, k ∈ C}, and K(v) = {Kj,k | tj,k = v}. Also let AllColors = ∪c∈Ccolor(c). The intuition behind the definition of these sets will become clearer once we define cI in the next subsection.

We now define the target gossip situation s as follows (where c iterates over C and v iterates V ). Each agent Cc,v is familiar with color(c) and Gadget(v). Each agent Ac,v is familiar with color(c) and Gadget(v). Each agent Fc is familiar with AllColors and Fix. Each agent Sv is familiar with AllColors, Fix, Gadget(v), and K(v). Each agent Kj,k is familiar with AllColors, Fix, Gadget(tj,k), Lj,k, and K(tj,k). Each agent Lj,k is familiar with AllColors, Gadget(tj,l), Lj,l, and K(tj,l) for all l ∈ C. Each agent Gv is familiar with AllColors, Fix, Gadget(v), and K(v). Each agent Hj,k is familiar with AllColors, Fix, Gadget(t(j, k)), Lj,k, and K(tj,k).

Intended call sequence. We now define the call sequence cI such that cI(rootAI ) = sI if I is triangle-3-colorable.

1. At the beginning, for each c ∈ C, all agents in color(c) call each other. After this, for every agent a ∈ AI, color c ∈ C, and at any point of cI, agent a is either familiar with all the secrets from color(c), or none of them. We say that agent a has color c ∈ C iff it is familiar with all the secrets from color(c).
2. In this step, we use a gadget which simulates coloring of the vertices with at most one color. For each v ∈ V , the gadget Gadget(v) consists of agents Ac,v for each c ∈ C,

and the selection agent Sv. In step 2a, for each v ∈ V , we let Sv and all Ac,v for c ∈ C call each other. In step 2b, Ac,v calls Cc,v. In step 2c, Ac,v calls Sv.

Suppose that we request the agents Cc,v and Ac,v to be familiar with only secrets of Gadget(v) and color(c), and the agent Sv to be familiar with Gadget(v), but do not restrict its knowledge of secrets of color(c). It is, however, impossible for Sv to have more than one color at the end of this step, because otherwise one of the agents Cc,v or Ac,v would also have more than one color.

1. In this step, we make sure that each triangle is indeed colored with all three colors. In step 3a, we let agent Sv call all agents in K(v), which is the set of all agents Kj,k such that tj,k = v. In step 3b, each agent Kj,k calls Lj,k. In step 3c, for each j ∈ T , all agents {Lj,k | k ∈ C} call each other, i.e., each agent Lj,k will have all three colors.
2. The problemwith the construction so far is that our gossiping situation at this point gives away the total knowledge of secrets of each agent. Currently, agents Sv and Kj,k have just one color, which reveals the chosen coloring. To fix this, in step 4a, all agents in Fix call each other, thus all of them will have all colors. In step 4b, for each v ∈ V , agent Gv calls Sv, and, for each j ∈ T , k ∈ C, Hj,k calls Kj,k.

Proof of correctness. Now, we will prove that sI can only be reached by a call sequence essentially the same as cI.

W.l.o.g., we can assume that the call sequence has to start, for each color c ∈ C, with all agents in color(c) calling each other. If c is a call sequence such that c(rootAI ) = sI then adding these calls at the beginning of c, would not affect its final gossip situation.

Note that a call between agents X and Y is possible only if X is familiar with the secret of Y , and Y is familiar with the secret of X. Furthermore, if agent X calls Y and Z, and Y is not familiar with secret Z, then we know that X cannot call Y after he has called Z. Based on this, we can deduce that only the following calls are possible in a call sequence c leading to sI. Each agent Cc,v can call color(c), then Ac,v. Each agent Ac,v can call Gadget(v) \ {Sv}, then Cc,v, then Sv. Each agent Fc can call color(c), then Fix. Each agent Sv can call Gadget(v), then K(v), then Gv. Each agent Kj,k can call Stj,k and Ktj,k , then Lj,k, then Hj,k. Each agent Lj,k can call Kj,k, then Lj,l. Each agent Gv can call Fix, then Sv. Each agent Hj,k can call Fix, then Kj,k.

Note that all these calls actually take place in cI.

Now, consider how Lj,k could have received the colors. He could have received them from Lj,l for l ∈ C. Now, Lj,l could have received these colors from Kj,l, but before Kj,k has called Lj,k or Hj,k. Hence, Kj,l could have received the colors only from Sv where v = tj,l, but only before Stj,l called K(v) or Gv. Hence, Sv must have received the color from Gadget(v). Since no agent in Gadget(v) other than Sv has more than one color, Sv must have received at most one color at that time, cv. Hence, Lj,k could have learned only the colors ctj,l for l ∈ C. Thus, if there exists call sequence c such that c(rootAI ) = sI then I has to be triangle-3-colorable. ✷

7 Computational Complexity

We now use the result of the previous section to determine the computational complexity of the implementability of the gossip protocols. We focus on a more general problem of determining the complexity of semantics for formulas with no nested modalities. We begin with the simplest case.

Lemma 1 For any formula φ ∈ L0 and a call sequence c checking whether (M, c) |= φ is in P.

Proof.(sketch) We construct c(root) in polynomial time by a successive application of the calls in c. We then simply check (in polynomial time) whether φ holds in c(root). ✷

Consider a call sequence c. If for some prefix c1.c of c, c1(root) = c1.c(root), then we say that c is redundant in c. We say that a call sequence c is redundant free if no call c from c is redundant in it. First, let us recall the following result that follows from Lemmas 1 and 2 in [Apt and Wojtczak, 2016].

Lemma 2 Suppose that c := c1, c, c2 and d := c1, c2, where c is redundant in c. Then for all formulas φ ∈ L0, (M, c) |= φ iff (M, d) |= φ. Also, the maximum length of a redundant free call sequence is |S|2 .

We can now use the result from the previous section.

Lemma 3 For any formula φ ∈ L0, checking whether M |= φ is CO-NP-complete.

Proof. We consider the complement of this problem. By the definition of semantics and Lemma 2, M ̸|= φ holds iff for some redundant free call sequence c, (M, c) |= ¬φ. By Lemma 2 the length of such a call sequence is at most |S|2 . This in conjunction with Lemma 1 implies that the complement problem is in NP.

To show NP-hardness note that each gossip situation s = (Qd)d∈A can be encoded as the following conjunction of size at most |S|2 : ζ(s) = ∧a∈A ( ∧B∈Qa FaB ∧ ∧B̸∈Qa ¬FaB). Now, a gossip situation s is a solution to the INCOMPLETE GOSSIPING problem iff ∃c (M, c) |= ζ(s) iff M ̸|= ¬ζ(s). So the NP-hardness follows from Theorem 1. ✷

Lemma 4 For any formula φ ∈ L0 and a call sequence c checking whether (M, c) |= Kaφ is CO-NP-complete.

Proof. By definition (M, c) |= Kaφ holds iff ∀d s.t. c ∼a d, (M, d) |= φ. Due to Lemma 2, it suffices to consider only call sequences d in which all calls except those involving agent a are redundant. The same argument as in the proof of Lemma 2 shows that the length of each such a call sequence d is at most |c| + |S|2 . This implies by Lemma 3 that checking (M, c) |= Kaφ can be done in CO-NP.

Now we show CO-NP-hardness already for the special case when c = ϵ and φ does not refer to agent a. Note that d ∼a ϵ iff no call in d involves agent a. Consider the model M′ with the set of agents A′ = A\{a}. Notice that ∀d ∼a ϵ (M, d) |= φ iff ∀d (M′ , d) |= φ iff M′ |= φ. The conclusion now follows from Lemma 3. ✷

We can now establish an appropriate complexity result that refers to the already mentioned complexity class P NP ‖ .

Theorem 2 For any formula ψ ∈ L1 and a call sequence c checking whether (M, c) |= ψ is P NP ‖ -complete.

Proof. We first show that the problem is in P NP ‖ , i.e., solvable by a deterministic polynomial-time Turing machine with parallel (i.e., non-adaptive) access to an NP oracle. Fix the appropriate formula ψ and a call sequence c. By assumption ψ is a propositional formula over the set of basic formulas of the form FaB or Kaφ, where φ is a propositional formula. We first check for each subformula Kaφ of ψ whether (M, c) |= Kaφ. By Lemma 4 each such a check can be done by a single query to an NP oracle.

Replace now in ψ each basic subformula φ by true if (M, c) |= φ and by false otherwise. The resulting ground propositional formula is true iff (M, c) |= ψ. The former problem is in P, so the latter is in P NP ‖ .

To prove P NP ‖ -hardness we show a reduction from the following decision promise problem.

Definition 5 (ODD-INDEX) Let ¯s = s1, . . . , sk be a sequence of gossip situations such that for some i ≤ k all s1, . . . , si can be the outcome of a call sequence (i.e., are positive instances of INCOMPLETE GOSSIPING) and none of si+1, . . . , sk can. Decide whether this promised index i is an odd number.

Since the INCOMPLETE GOSSIPING problem is NP-hard, the P NP ‖ -hardness of the ODD-INDEX problem follows from the sufficient conditions for P NP ‖ -hardness given in Theorem 5.2 in [Wagner, 1987] (see also Lemma 7 in [Spakowski and Vogel, 2000]). Now given an ODD-INDEX instance ¯s = s1, . . . , sk we construct a formula ψ ∈ L1 such that (M, ϵ) |= ψ iff the index i for ¯s is odd. First, let us add an additional agent a to A and set his secrets in ¯s to {A}. For a gossip situations s, let ζ(s) be defined as in the proof of Lemma 3. Let ψl be the formula ∧lj=1 ¬Ka¬ζ(sj) ∧ ∧kj=l+1 Ka¬ζ(sj). Intuitively, ψl is true iff the index i is equal to l. This is the case because (M, ϵ) |= ¬Ka¬ζ(s) iff s can be the outcome of a call sequence, and (M, ϵ) |= Ka¬ζ(s) iff s cannot be the outcome of a call sequence. Let ψ = ψ1 ∨ ψ3 ∨ . . . ∨ ψ2⌈k/2⌉-1. We claim that (M, ϵ) |= ψ iff i is an odd number. This is because ψ tests whether i is equal to an odd number between 1 and k. ✷

This yields the desired conclusion about the implementability of the gossip protocols. To analyze their partial correctness and termination, we will need the following three lemmas.

Lemma 5 For any call sequences c ∼a d and arbitrary formula φ: (M, c) |= Kaφ iff (M, d) |= Kaφ.

Proof. It follows directly from the definition of Ka. ✷

We call the second call c in a call sequence c1.c.c2.c.c3 epistemically redundant if c1.c(root) = c1.c.c2.c(root). We now show that removing an epistemically redundant call does not affect the truth of any formula with no nested modalities.

Lemma 6 If c1.c.c2.c.c3 is a call sequence where the 2nd call c is epistemically redundant, then for any formula ψ ∈ L1:

Proof. The proof proceeds by structural induction and the only non-trivial case is when ψ = Kaφ. If a ̸∈ c then c1.c.c2.c.c3 ∼a c1.c.c2.c3, because c1.c.c2.c(root) = c1.c.c2(root). The claim then follows from Lemma 5.

First, due to Fact 1, c′1 .c.c′2 .c.c′3 ∼a c1.c.c2.c.c3 implies that c′1 .c(root) = c′1 .c.c′2 .c(root). Thus, the second c is redundant in c′1 .c.c′2 .c.c′3 and the claim follows from Lemma 2. ✷

Lemma 7 For any formula ψ ∈ L1, checking M |= ψ is in coNP NP .

Proof. By definition M |= ψ holds iff ∀c (M, c) |= ψ. Due to Lemma 6 it suffices to check this condition for call sequences c of polynomial length, because there are polynomially many different calls c and due to Lemma 2 in each c at most |S|2 calls may be non-redundant. At the same time (M, c) |= ψ is P NP ‖ -complete. This immediately gives a coNP P NP ‖ algorithmfor our problem, because it suffices to check for all polynomiallylong call sequences c whether (M, c) |= ψ holds. However, a coNP P NP ‖ Turing machine can can be simulated by a coNP NP Turing machine, because polynomially many P NP ‖ queries can be replaced by polynomially many queries to an NP oracle. This concludes the proof that the problem is in coNP NP . ✷

Due to Lemma 7 and the characterization of partial correctness as the truth of formula (1) we get the following.

Theorem 3 Checking partial correctness of a gossip protocol is in coNP NP .

We conclude by addressing the termination problem.

Theorem 4 Checking whether a gossip protocol always terminates is in coNP NP .

Proof.(sketch) Non-termination of a gossip protocol is equivalent to checking whether for one of its guards, ψ, there exists a call sequence c and a call c such that both (M, c) |= ψ and (M, c.c) |= ψ hold. Due to Theorem 2 checking either of them can be done in P NP ‖ . But in fact checking whether they both hold at the same time is also in P NP ‖ , because we can execute all their non-adaptive queries to an NP oracle simultaneously. This also shows that termination is in P NP ‖ , because one can simply negate the result of these checks. Now, the same argument as at the end of the proof of Lemma 7 shows that the termination problem is in coNP NP . ✷

8 FutureWork

In this paper, we established the computational complexity of implementability of a gossip protocol and an upper bound on checking its partial correctness and termination, which we conjecture to be coNP NP -complete problems. An interesting future work would be to study the same problems for gossip protocols with nested modalities or with a common knowledge operator. Another interesting issue is to study the synthesis of a distributed gossip protocol from epistemic specifications (see, e.g., [van der Meyden and Wilke, 2005]).

Acknowledgements

We thank André Hernich for useful discussions on some aspects of this work. This work was initiated at Autobóz'16 and partly supported by NCN grant 2014/13/B/ST6/01807 and EPSRC grants EP/M027651/1 and EP/P020909/1.