# on_the_computational_complexity_of_gossip_protocols__3251cae5.pdf On the Computational Complexity of Gossip Protocols Krzysztof R. Apt CWI, The Netherlands University of Warsaw, Poland apt@cwi.nl Eryk Kopczy nski University of Warsaw, Poland erykk@mimuw.edu.pl Dominik Wojtczak University of Liverpool, UK d.wojtczak@liv.ac.uk Gossip protocols deal with a group of communicating agents, each holding a private information, and aim at arriving at a situation in which all the agents know each other secrets. Distributed epistemic gossip protocols are particularly simple distributed programs that use formulas from an epistemic logic. Recently, the implementability of these distributed protocols was established (which means that the evaluation of these formulas is decidable), and the problems of their partial correctness and termination were shown to be decidable, but their exact computational complexity was left open. We show that for any monotonic type of calls the implementability of a distributed epistemic gossip protocol is a PNP - complete problem, while the problems of its partial correctness and termination are in co NPNP. 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 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 PNP -complete problem and checking its partial correctness and termination is in co NPNP. 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 Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) 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.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: φ ::= Fap | φ | φ φ | Kaφ, 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; La 1, 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 Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) 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). 2 3.3 Gossip Models 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. (i) If a c, then c.c a d and c a d.c. (ii) If a c and c.c(root)a = d.c(root)a, then c.c a d.c. 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. (ii) For all c, d C if c a d, then c(root)a = d(root)a. 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): (M, c) |= Fap iff p c(root)a, (M, c) |= Kaφ iff d s.t. c a d, (M, d) |= φ. M |= φ iff c (M, c) |= φ. When M |= φ we say that φ is true. 2 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 V a A Fa A is true into one in which the formula V a,b A Fa B 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 [[]m j=1 ψj cj], where m > 0 and each ψj cj is such that ψj La 1 and a cj. Given a formula ψ La 1 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 ca j ], 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 ca j = 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 ca j . 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) |= V a,b A Fa B, i.e., if each agent is an expert Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) in the gossip situation c(root). Note that c is a finite computation iff (M, c) |= V a A Vma j=1 ψa j . We call the formula V a A Vma j=1 ψa j the exit condition of the gossip protocol P. So P is partially correct iff the implication a,b A Fa B (1) 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 La 1 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: [[]j Ni,C SFi C Ki Fj C (i, j)]. 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 V (i,j) E V C S(Fi C Ki Fj C). For all agents i and j and secrets C, the formula Ki Fj C Fj C is true, so the exit condition implies V (i,j) E V C S(Fi C Fj C). 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 V C S(Fig C Fig+1C). By combining these h 1 formulas we get V C S(Fj C Fi C). But Fj J is true, so we conclude Fi J. Consequently V i,j A Fi J, as desired. To prove termination it suffices to note that after each call ij the size of the set {(i, j, C) | Ki Fj C} 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, s I), where AI is a set of agents and s I is a gossip situation. First, we will describe (AI, s I). Then we will show the intended call sequence c I and give some intuition about the gadgets that we use. We then show that if I is triangle 3-colorable, then c I(root AI) = s I. In the last paragraph, we prove that our reduction is correct, i.e., if there exists c such that c(root AI) = s I, 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 All Colors = c Ccolor(c). The intuition behind the definition of these sets will become clearer once we define c I 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 All Colors and Fix. Each agent Sv is familiar with All Colors, Fix, Gadget(v), and K(v). Each agent Kj,k is familiar with All Colors, Fix, Gadget(tj,k), Lj,k, and K(tj,k). Each agent Lj,k is familiar with All Colors, Gadget(tj,l), Lj,l, and K(tj,l) for all l C. Each agent Gv is familiar with All Colors, Fix, Gadget(v), and K(v). Each agent Hj,k is familiar with All Colors, Fix, Gadget(t(j, k)), Lj,k, and K(tj,k). Intended call sequence. We now define the call sequence c I such that c I(root AI) = s I 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 c I, 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, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) 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. 3. 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. 4. The problem with 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 s I can only be reached by a call sequence essentially the same as c I. 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(root AI) = s I 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 s I. 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 c I. 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(root AI) = s I then I has to be triangle-3-colorable. 2 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). 2 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) = V a A V B Qa Fa B V B Qa Fa B . 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. 2 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. 2 We can now establish an appropriate complexity result that refers to the already mentioned complexity class PNP . Theorem 2 For any formula ψ L1 and a call sequence c checking whether (M, c) |= ψ is PNP -complete. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) Proof. We first show that the problem is in PNP , 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 Fa B 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 PNP . To prove PNP -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 PNP -hardness of the ODD-INDEX problem follows from the sufficient conditions for PNP -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 Vl j=1 Ka ζ(sj) Vk j=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. 2 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. 2 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: (M, c1.c.c2.c.c3) |= ψ iff (M, c1.c.c2.c3) |= ψ. 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. If a c, it suffices to check that c 1.c.c 2.c.c 3 a c1.c.c2.c.c3 (M, c 1.c.c 2.c.c 3) |= φ iff (M, c 1.c.c 2.c 3) |= φ. 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. 2 Lemma 7 For any formula ψ L1, checking M |= ψ is in co NPNP. 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 PNP -complete. This immediately gives a co NPPNP algorithm for our problem, because it suffices to check for all polynomiallylong call sequences c whether (M, c) |= ψ holds. However, a co NPPNP Turing machine can can be simulated by a co NPNP Turing machine, because polynomially many PNP queries can be replaced by polynomially many queries to an NP oracle. This concludes the proof that the problem is in co NPNP. 2 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 co NPNP. We conclude by addressing the termination problem. Theorem 4 Checking whether a gossip protocol always terminates is in co NPNP. 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 PNP . But in fact checking whether they both hold at the same time is also in PNP , because we can execute all their non-adaptive queries to an NP oracle simultaneously. This also shows that termination is in PNP , 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 co NPNP. 2 8 Future Work 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 co NPNP-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. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17) References [Apt and Wojtczak, 2016] Krzysztof R. Apt and Dominik Wojtczak. On decidability of a logic of gossips. In Proc. of the 15th European Conference on Logics in Artificial Intelligence (JELIA 2016), volume 10021 of Lecture Notes in Computer Science, pages 18 33. Springer, 2016. [Apt and Wojtczak, 2017a] Krzysztof R. Apt and Dominik Wojtczak. Common Knowledge in a Logic of Gossips. In Proc. of TARK 2017 (to appear). EPTCS, 2017. [Apt and Wojtczak, 2017b] Krzysztof R. Apt and Dominik Wojtczak. Decidability of Fair Termination of Gossip Protocols. In Proc. of the IWIL Workshop and LPAR Short Presentations, volume 1, pages 73 85. Kalpa Publications, 2017. [Apt et al., 2016] Krzysztof R. Apt, Davide Grossi, and Wiebe van der Hoek. Epistemic protocols for distributed gossiping. In Proc. of the 15th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2015), volume 215 of EPTCS, pages 51 66, 2016. [Attamah et al., 2014a] Maduka Attamah, Hans van Ditmarsch, Davide Grossi, and Wiebe van der Hoek. A framework for epistemic gossip protocols. In Proc of the 12th European Conference on Multi-Agent Systems (EUMAS 2014), pages 193 209, 2014. [Attamah et al., 2014b] Maduka Attamah, Hans van Ditmarsch, Davide Grossi, and Wiebe van der Hoek. Knowledge and gossip. In Proceedings of ECAI 14. IOS Press, 2014. [Cooper et al., 2016a] Martin C. Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, and Pierre Régnier. A simple account of multiagent epistemic planning. In Proc. of ECAI 2016, pages 193 201. IOS Press, 2016. [Cooper et al., 2016b] Martin C. Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, and Pierre Régnier. Simple Epistemic Planning: Generalised Gossiping. In Proc. of ECAI 2016, pages 1563 1564. IOS Press, 2016. [Fagin et al., 1997] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Knowledge-based programs. Distributed Computing, 10(4):199 225, 1997. [Hedetniemi et al., 1988] Sandra Mitchell Hedetniemi, Stephen T. Hedetniemi, and Arthur L. Liestman. A survey of gossiping and broadcasting in communication networks. Networks, 18(4):319 349, 1988. [Herzig and Maffre, 2017] Andreas Herzig and Faustine Maffre. How to share knowledge by gossiping. AI Communications, 30(1):1 17, 2017. [Hromkovic et al., 2005] Juraj Hromkovic, Ralf Klasing, Andrzej Pelc, Peter Ruzicka, and Walter Unger. Dissemination of Information in Communication Networks - Broadcasting, Gossiping, Leader Election, and Fault-Tolerance. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2005. [Kempe et al., 2003] David Kempe, Alin Dobra, and Johannes Gehrke. Gossip-based computation of aggregate information. In Foundations of Computer Science, 2003. Proceedings. 44th Annual IEEE Symposium on, pages 482 491. IEEE, 2003. [Kermarrec and van Steen, 2007] Anne-Marie Kermarrec and Maarten van Steen. Gossiping in distributed systems. Operating Systems Review, 41(5):2 7, 2007. [Khuller et al., 2003] Samir Khuller, Yoo-Ah Kim, and Yung Chun Justin Wan. Algorithms for data migration with cloning. In Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, pages 27 36. ACM, 2003. [Ladin et al., 1992] Rivka Ladin, Barbara Liskov, Liuba Shrira, and Sanjay Ghemawat. Providing high availability using lazy replication. ACM Transactions on Computer Systems (TOCS), 10(4):360 391, 1992. [Liben-Nowell, 2002] David Liben-Nowell. Gossip is synteny: Incomplete gossip and the syntenic distance between genomes. Journal of Algorithms, 43(2):264 283, 2002. [Spakowski and Vogel, 2000] Holger Spakowski and Jörg Vogel. Θp 2-completeness: A classical approach for new results. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 348 360. Springer, 2000. [Tijdeman, 1971] Robert Tijdeman. On a telephone problem. Nieuw Archief voor Wiskunde, 3(XIX):188 192, 1971. [van der Meyden and Wilke, 2005] Ron van der Meyden and Thomas Wilke. Synthesis of distributed systems from knowledge-based specifications. In Proceedings 16th International Conference CONCUR 2005, volume 3653 of Lecture Notes in Computer Science, pages 562 576. Springer, 2005. [van Ditmarsch et al., 2017] Hans van Ditmarsch, Jan van Eijck, Pere Pardo, Rahim Ramezanian, and François Schwarzentruber. Epistemic protocols for dynamic gossip. Journal of Applied Logic, 20:1 31, 2017. [Wagner, 1987] Klaus W. Wagner. More complicated questions about maxima and minima, and some closures of NP. Theoretical Computer Science, 51(1-2):53 80, 1987. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17)