# propositional_gossip_protocols_under_fair_schedulers__83bca3f9.pdf Propositional Gossip Protocols under Fair Schedulers Joseph Livesey and Dominik Wojtczak University of Liverpool, UK {joseph.livesey, d.wojtczak}@liverpool.ac.uk Gossip protocols are programs that can be used by a group of agents to synchronize what information they have. Namely, assuming each agent holds a secret, the goal of a protocol is to reach a situation in which all agents know all secrets. Distributed epistemic gossip protocols use epistemic formulas in the component programs for the agents. In this paper, we study the simplest classes of such gossip protocols: propositional gossip protocols, in which whether an agent wants to initiate a call depends only on the set of secrets that the agent currently knows. It was recently shown that such a protocol can be correct, i.e., always terminates in a state where all agents know all secrets, only when its communication graph is complete. We show here that this characterization dramatically changes when the usual fairness constraints are imposed on the call scheduler used. Finally, we establish that checking the correctness of a given propositional protocol under a fair scheduler is a co NP-complete problem. 1 Introduction 1.1 Background and Motivation Gossip protocols have the goal of spreading information through a network via point-to-point communications (which we refer to as calls). Each agent holds initially a secret and the aim is to arrive at a situation in which all agents know each other s secret. During each call the caller and callee exchange all secrets that they know at that point. Such protocols were successfully used in a number of domains, for instance communication networks [Hedetniemi et al., 1988], computation of aggregate information [Kempe et al., 2003], and data replication [Ladin et al., 1992]. For a more recent account see [Hromkoviˇc et al., 2005] and [Kermarrec and van Steen, 2007]. One of the early results established by a number of authors in the 1970s, e.g., [Tijdeman, 1971], is that for n agents 2n 4 calls are necessary and sufficient when every agent can communicate with any other agent. When such a communication graph is not complete, 2n 3 calls may be needed [Bumby, 1981] and are sufficient for any connected communication graph [Harary and Schwenk, 1974]. However, the protocols considered in these papers were centralized, i.e., a central planner was telling each agent who and when to call. In [Attamah et al., 2014] 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 also means that they can be seen as special cases of knowledge-based programs introduced in [Fagin et al., 1997]. In [Apt et al., 2016] 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 right and was subsequently studied in a number of papers. In this paper, we are going to focus on its simplest propositional fragment. Propositional gossip protocols are a particular type of epistemic gossip protocols in which all guards are propositional. This means that calls being made by each agent are dependent only on the secrets that the agent has had access to. Such protocols have many potential applications. They are particularly simple and quick to execute (as evaluation of a guard can be done in linear time), so they are well-suited even for small devices with limited memory and computational capabilities. They can, e.g., be used for synchronization of information in sensor networks or swarms of robots. They can also be viewed as a special tractable case of multi-agent planning. During the execution of a protocol, a state can be reached where multiple calls are possible at the same time. Then a call scheduler would decide which call takes priority. The scheduler can be assumed to be demonic, meaning it picks the order of calls in a way such that the protocol fails or to maximize the number of calls made before termination. In distributed and concurrent systems, it is common to impose fairness constraints on schedulers without which even the classic Peterson s algorithm for mutual exclusion would not work. In the context of gossip protocols this may require, e.g., that an agent makes a call eventually if he wants to call (which we will call agent-fairness) or that a call is eventually made if it can be (rule-fairness). In [Apt and Wojtczak, 2019], many challenging open problems about general as well as propositional gossip protocols were proposed. The open problems listed there regarding propositional gossip protocols were addressed in [Livesey and Wojtczak, 2021b] and [Livesey and Wojtczak, 2021a]. In the former it was shown that the communication graph (i.e., Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) who can call who) of a correct propositional protocol has to be complete (when ignoring the edges directions), addressing Problem 5 of [Apt and Wojtczak, 2019]. We revisit here this answer by looking at the communication graph classes of correct propositional protocols under fair schedulers. We show that in this new setting this characterization completely changes: for any undirected connected graph, as well as directed strongly connected graph, there exists a correct propositional protocol under both agent-fair and rule-fair schedulers. Finally, we establish that checking the correctness of a given protocol under such fair schedulers is a co NP-complete problem. 1.2 Related Work Much work has been done on general epistemic gossip protocols. The various types of calls used in [Attamah et al., 2014] and [Apt et al., 2016] were presented in a uniform framework in [Apt et al., 2018], where in total 18 types of communication were considered and compared w.r.t. their epistemic strength. In this paper we study the asynchronous communication setting where agents are not aware of the calls they do not participate in nor can they synchronize their actions precisely as there is no global clock. This is the most appropriate model to study in the context of distributed systems. In [Apt and Wojtczak, 2018], the decidability of the semantics of the gossiping logic and truth in this model was established for the limited fragment of the logic (namely, without nesting of modalities). The precise computational complexity of this fragment was further studied in [Apt et al., 2017] and checking termination, partial correctness and correctness in this case was shown to be in co NPNP. In [Apt and Wojtczak, 2017] it was shown that checking agent-fair and rule-fair termination and correctness for such protocols are decidable. Building on these results, [van Ditmarsch et al., 2020] showed decidability of the full logic for various variants of the gossiping model. Centralized gossip protocols were studied in [Herzig and Maffre, 2017; Cooper et al., 2016]. These had the goal to achieve higher-order shared knowledge. Such problems were further studied in [Cooper et al., 2018] with temporal constraints where each call is assigned a time interval when this call can only be made. In [van Ditmarsch et al., 2017a; van Ditmarsch and Kokkinis, 2017] the expected time of termination of several gossip protocols for complete graphs was studied. Dynamic distributed gossip protocols were studied in [van Ditmarsch et al., 2017b], in which the calls allow the agents to transmit the links as well as share secrets. Similar to this paper, it characterized different distributed epistemic protocols in terms of the (largest) class of graphs where each protocol is correct, i.e., where the protocol necessarily ends up with all agents knowing all secrets. 1.3 Plan of the Paper We first go through the logic, originally defined in [Apt et al., 2016], in Section 2, where we also define the notions of agent-fair and rule-fair schedulers. We then investigate the structure of feasible communication graphs for agent-fair and rule-fair correct propositional gossip protocols in Section 3. Finally, we study the computational complexity of agent-fair and rule-fair termination and correctness in Section 4. 2 Gossiping Logic We recall here the framework of [Apt et al., 2016], which we restrict to the propositional setting. We assume a fixed set G of n 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 Sec the set of all secrets. The propositional language Lp is defined by the following grammar: ϕ ::= Fa S | ϕ | ϕ ϕ, where S Sec and a G. We will distinguish the following sublanguage La p, where a G is a fixed agent, which disallows all Fb operators for b = a. So Fa S is an atomic formula, which we read as agent a is familiar with the secret S . Note that in [Apt et al., 2016], a compound formula Kaϕ, i.e., agent a knows the formula ϕ is true , was used. Dropping Kaϕ from the logic simplifies greatly its semantics and the execution of a gossip protocol, while still being capable of defining a rich class of protocols. Below we shall freely use other Boolean connectives that can be defined using and in a standard way. We shall use the following formula S Sec Fi S, that denotes the fact that agent i is an expert, i.e., he is familiar with all the secrets. Each call, written as ab or sometimes a b, concerns two different agents, the caller, a, and the callee, b. After a call, the caller and the callee learn each other s secrets. Calls are denoted by c, d, etc. 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 ϵ. We use c to denote a call sequence and C to denote the set of all finite 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. We say that c is an extension of a call sequence c if for some call sequence d we have c = c.d. To describe what secrets the agents are familiar with, we use the concept of a gossip situation. It is a sequence s = (Qa)a G, where {A} Qa Sec for each agent a. Intuitively, Qa is the set of secrets a is familiar with in the gossip situation s. The initial gossip situation is the one in which each Qa equals {A} and is denoted by root. It reflects the fact that initially each agent is familiar only with his own secret. Note that an agent a is an expert in a gossip situation s iff Qa = 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 s := (Qd)d G and a call ab. Then ab(s) := (Q d)d G, where Q a = Q b = Qa Qb, and for c {a, b}, Q c = Qc. So the effect of a call is that the caller and the callee share the secrets they are familiar with. Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) The result of applying a call sequence to a gossip situation s is defined inductively as follows: ϵ(s) := s, (c.c)(s) := c(c(s)). 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 a comma. e.g., if there are three agents, a, b and c, then root = A, B, C and the gossip situation ({A, B}, {A, B}, {C}) will be written as AB, AB, C. Let G = {a, b, c}. Consider the call sequence ac.bc.ac. It generates the following successive gossip situations starting from root: A, B, C ac AC, B, AC bc AC, ABC, ABC ac ABC, ABC, ABC. Definition 1. Consider a call sequence c C. We define the satisfaction relation |= inductively as follows: c |= Fa S iff S c(root)a, c |= ϕ iff c |= ϕ, c |= ϕ1 ϕ2 iff c |= ϕ1 and c |= ϕ2. So a formula Fa S is true after the call sequence c whenever secret S belongs to the set of secrets agent a is familiar with in the situation generated by the call sequence c applied to the initial situation root. Hence c |= Expa iff agent a is an expert in c(root). By a propositional component program, in short a program, for an agent a G we mean a statement of the form [[]ma j=1 ψj cj], where each ψj cj (which we will call a rule), is such that agent a is the caller in the call cj, ψj La p (which we will call a guard of this rule), and ma 0 is the number of rules agent a has. If the guard of a rule is true then the corresponding agent, call and the rule is said to be active. Intuitively, denotes a repeated execution of the rules, one at a time, where each time non-deterministically an active rule is selected. Consider a propositional gossip protocol, P, that is a parallel composition of the propositional component programs [[]ma j=1 ψa j ca j ], one for each agent a G. 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 ϵ. Further, if c is a node and for some rule ψa j ca j we have c |= ψa j , then c.ca j is a node that is a direct descendant of c. Intuitively, the arc from c to c.ca j records the effect of the execution of the rule ψa j ca j performed after the call sequence c took place. By a computation of a gossip protocol P 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 leaves c of the computation tree of P, and all agents a, we have c |= Expa, i.e., if each agent is an expert in the gossip situation c(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. In [Attamah et al., 2014] the following correct propositional gossip protocol, called Learn New Secrets (LNS in short), for complete digraphs was proposed. Example 2 (LNS protocol). The following program is used by agent i: [[]j G Fi J ij]. Informally, agent i calls agent j if agent i is not familiar with j s secret. We also consider two variants of fair termination, but we first have to recall the notion of fairness. An infinite computation is rule-fair (resp. agent-fair) if all rules (resp. agents) that are active after infinitely many prefixes of this computation are selected infinitely often. By default a finite computation is rule-fair and agent-fair. 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. We do not define agent-fair nor rule-fair partial correctness, because they are equivalent to partial correctness. This is simply because partial correctness is a condition on finite computations only and every finite computation is agent-fair and rule-fair. A protocol which rule-fairly (agent-fairly) terminates and is partially correct is said to be rule-fair (agent-fair) correct. The agents and possible calls of a given protocol can be thought of as nodes (agents) and edges (calls) of its (directed) communication graph. In the next section, we are going to study for which classes of communication graphs an agent-fair or rule-fair correct propositional gossip protocol exists. 3 Fair and Correct Communication Graphs We begin by showing that the scheduler s type has a huge impact on whether a gossip protocol works correctly. In particular we show that rule-fairness and agent-fairness are not equivalent. Proposition 1. There exists an agent-fair correct propositional gossip protocol which is not a correct propositional gossip protocol. Proof. Let us have three agents, a, b and c. The protocol only consists of a rule Fa C ab for agent a, and Fb A Fb C bc for agent b. Clearly this is not a correct propositional gossip protocol as it may never terminate, e.g., ab call can be repeated indefinitely. However, this is an agent-fair correct propositional gossip protocol. Note that the first call has to be ab. After that call, both ab and bc calls are active. Due to the agent-fairness of the scheduler used, eventually the bc call must take place, ensuring that both b and c become experts. After that, the only active call is ab, and once this occurs no calls are active and so the protocol terminates. Moreover, all agents are experts at that point. Note that, straight from the definition, any agent-fair correct protocol is also rule-fair correct, because rule-fairness can only narrow down further the set of permitted computations. We now show that the opposite does not hold. Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) Proposition 2. There exists a rule-fair correct propositional gossip protocol which is not an agent-fair correct propositional gossip protocol. Proof. Let us have three agents, a, b and c. The protocol only consists of a rule Fa C ab for agent a, and rules Fb A Fb C bc, Fb A Fb C ba for agent b. This is not an agent-fair correct propositional gossip protocol. Its computation has to start with ab, at which point calls ab, ba and bc are active. Note that a computation repeatedly alternating between making calls ab and ba after that is agent-fair, because a call of each active agent (a and b only) is picked infinitely many times. The protocol will not terminate in this case, so it is not agent-fair correct. However, this is a rule-fair correct propositional gossip protocol, because under a rule-fair scheduler the active call bc has to be picked eventually. Once bc is made both b and c will become experts. This leaves ab as the only active call, and once this occurs, the protocol terminates in a gossip situation where all agents are experts. With this knowledge that the type of the scheduler used can change if a given protocol is correct, we revisit the Problem 5 of [Apt and Wojtczak, 2019] to determine what the underlying communication graph should be for agent-fair or rule-fair correct propositional gossip protocols. We start with the simplest case of a path (linear) graph where the n agents are labeled x1, . . . , xn and, for any i < n, agent xi can only call xi+1. We then proceed with increasingly broader graph classes, which on the downside require increasingly more complex protocols to be agent-fair or rule-fair correct. Theorem 1. For any path graph, there exists an agent-fair correct propositional gossip protocol. Proof. The protocol will only consist of rules Expx1 x1x2 for agent x1, Fx2X1 Expx2 x2x3 for agent x2, . . . , Fxn 1Xn 2 Expxn 1 xn 1xn for agent xn 1. In other words, an agents wants to call the next agent if he is familiar with the secret of the previous agent and he is not yet an expert. Note that initially only agent x1 is active and he will call x2, after which both of these agents become active. Due to agentfairness, agent x2 will eventually make his call after which agent x3 becomes active and so on. Note that, for every i < n, when the call xi 1xi becomes active, xi 1 already knows all secrets X1, . . . , Xi 1. This means that when eventually the call xn 1xn takes place, both of the agents involved become the first two experts. Then eventually, the call xn 2xn 1 will take place due to agent-fairness, and xn 2 will become the third expert and so on until x1 becomes an expert when the protocol terminates. As pointed out earlier, Theorem 1 implies that the same result holds for rule-fairness. We can also get that every graph with a Hamiltonian path can be a communication graph of a agent-fair / rule-fair correct protocol by simply ignoring the rest of the edges and constructing the protocol as in Theorem 1. But instead we are going to generalize this construction to show this result for any tree, which is any connected acyclic undirected graph. The gossip protocol will be set up in a way to ensure there is a unique directed path from every agent to a special agent x, who is guaranteed to be the first agent to become an expert. Then all the secrets collected in x will slowly filter back up the directed paths to all the other agents. Theorem 2. For any tree T, there exists an agent-fair correct propositional gossip protocol. Proof. Let us pick any agent x in this tree T. We now turn this undirected tree into a directed one by setting the direction of all edges in this tree towards x. First, the distance of an agent x from x is the length of the shortest path from x to x traversing just edges of T. Now, formally, the direction of an edge connecting two agents is from the agent at a larger distance from x towards the agent at a smaller distance to x. This is well-defined, because we now show that no two neighboring agents in T can have the same distance to x. If they had then these two paths of equal length, from each of them to x, cannot completely overlap. So these paths would intersect at x or another agent. The two parts of these paths until the intersection together with the edge connecting these two agents would form a cycle, which is not possible as T was supposed to be acyclic. Similarly, we can argue that each node apart from x in such formed tree has a unique outgoing edge ( x has none). This is because if an agent x has two successors in such a directed tree then there would be a path from each of them to x that intersect at some point. These paths to the intersection point together with the edges from x would form a cycle; a contradiction. Let pred(x) denote the set of all agents who have an outgoing edge to x in such a defined directed tree and succ(x) denote the unique agent who has an incoming edge from x. Now, the protocol will only consist of a single rule for each agent x G \ { x}: Expx V y pred(x) Fx Y x succ(x). In other words, an agent wants to call its unique direct successor agent if he is familiar with all the secrets of his direct predecessors and he is not yet an expert. Agent x has no rules. The rest of the proof proceeds similarly to Theorem 1. First, note that when the call x succ(x) becomes active then x has to already be familiar with all secrets of all his (indirect) predecessors in this directed tree. This is because it can only become active after all direct predecessors of x call him and by inductive assumption all of them have to know all secrets of their (indirect) predecessors at that point. Second, due to agent-fairness, every call that is active will eventually be made, because there is only at most one such call per agent. Initially, only agents that do not have predecessors are active and all of them will make their calls. A call does not stop being active until the agent making it becomes an expert. Due to the protocol setup this cannot happen before x becomes an expert, but that only takes place once all the calls that can be made were made (otherwise some secrets would not reach x). Note that once x becomes an expert (and the agent calling him), the number of active agents is n 2. Now, only when a new agent becomes an expert (by calling an agent who is already an expert), he stops being active and will never become active again. This shows that the protocol is partially correct. Moreover, as long as there is at least one active call, one of them will have an expert as its callee. This guarantees the protocol to agent-fairly terminate, because eventually such Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22) a call is made and the number of active agents decreases. Together this shows the protocol to be agent-fair correct. We are now ready to prove the result for undirected graphs in its full generality. This result is essentially an almost immediate corollary of Theorem 2. Corollary 1. For any undirected connected graph G, there exists an agent-fair and rule-fair correct propositional gossip protocol. Proof. Any such graph G has a spanning tree T, which we pick arbitrarily. We use the same protocol as defined in Theorem 2 when applied to T. As such a protocol is agent-fair correct, it is also rule-fair correct. It is trivial to see that for any undirected graph which is not connected there cannot be a correct protocol, because no agent can ever become an expert as secrets cannot be shared across different components. This together with Corollary 1 resolves the case of undirected communication graphs, but naturally leads on to the question of what happens in the directed case. Theorem 3. For any strongly connected digraph D, a rule-fair correct propositional gossip protocol exists. Proof. The protocol that we are going to use is simply: Expx xy for all agents x and agents y which are direct successors of x in D. In other words, an agent keeps on calling every agent he can until he is an expert. Clearly, this protocol can only terminate once every agent is an expert, so it is partially correct. Now suppose this protocol does not rule-fairly terminate and so there exists a rule-fair computation such that agent a does not learn secret B. As the scheduler is rule-fair, every call which is active will eventually be made. As a is not an expert, and there is a path from a to b, a must be trying to make a call to an agent whose distance to b in D is smaller than that of a. If this agent, say c, already knows B then a would get to know B eventually due to rule-fairness. If c does not yet know B, then c must be trying to make a call to an agent who is closer to b, and so on. As the number of calls in this path that ends at b or at another agent already knowing B is finite, and all these calls are active, eventually all agents along this path will learn B; a contradiction. Now, we are going to generalize even further the result of Corollary 1 by showing a construction of an agent-fair correct protocol for an arbitrary strongly connected digraph (note that any undirected connected graph can be viewed as a strongly connected digraph). Theorem 4. For any strongly connected digraph D, an agentfair correct propositional gossip protocol exists. Proof. Let us number all the agents x1, . . . , xn. Intuitively, the constructed protocol will proceed in stages, but agents can progress through stages at a different pace. At stage i an agent tries to learn the secret Xi. Once he achieves that he moves on to stage i + 1 until eventually he reaches stage n + 1 when he becomes an expert and stops being active. Note that an agent can skip a stage if he already knows the desired secret. It is clear the guard of the rule for an agent a at stage i can be written down as a propositional formula: V j