# verification_of_distributed_epistemic_gossip_protocols__6e8c2d37.pdf

Journal of Artificial Intelligence Research 62 (2018) 101-132 Submitted 04/17; published 05/18

Verification of Distributed Epistemic Gossip Protocols

Krzysztof R. Apt apt@cwi.nl CWI, Amsterdam, The Netherlands MIMUW, University of Warsaw, Poland

Dominik Wojtczak d.wojtczak@liverpool.ac.uk University of Liverpool, Liverpool, U.K.

Gossip protocols aim at arriving, by means of point-to-point or group communications, at a situation in which all the agents know each other secrets. Distributed epistemic gossip protocols use as guards formulas from a simple epistemic logic and as statements calls between the agents. They are natural examples of knowledge based programs. We prove here that these protocols are implementable, that their partial correctness is decidable and that termination and two forms of fair termination of these protocols are decidable, as well. To establish these results we show that the definition of semantics and of truth of the underlying logic are decidable.

1. Introduction

This paper is concerned with the verification of a specific type of gossip protocols. In such protocols each agent holds a secret initially known only to him. The secrets spread by means of communications. During them, e.g., point-to-point or group communications, the participating agents exchange some, possibly all, secrets they know. The aim of a gossip protocol is to arrive at a situation in which all the agents know each other secrets. Gossip protocols have been successful in various domains, e.g., communication networks (Hedetniemi, Hedetniemi, & Liestman, 1988), computation of aggregate information (Kempe, Dobra, & Gehrke, 2003), and data replication (Ladin, Liskov, Shrira, & Ghemawat, 1992). A more recent account is given by Hromkovic, Klasing, Pelc, Ruzicka, and Unger (2005) and Kermarrec and van Steen (2007). In these references gossip protocols are viewed as parallel, probabilistic or distributed programs. As a simple example assume that the set of agents is {a, b, c, d, e1, . . ., en 4}, where n 4, (if n = 4 then there are no ei agents) and assume that the agents communicate by means of phone calls during which they exchange all secrets they know. Then take the call sequence

(a, e1), (a, e2), . . ., (a, en 4).

After it agent a knows all the secrets of the agents e1, . . ., en 4. We follow it by the call sequence (a, b), (c, d), (a, d), (b, c). After it agents a, b, c, d know all the secrets. So following it by the above call sequence (a, e1), (a, e2), . . ., (a, en 4) we achieve the desired situation in which all agents know all the secrets. This took 2n 4 calls. One of the early results established by a number of authors in the seventies, for instance by Tijdeman (1971), is that for n 4 agents at least 2n 4 phone calls are needed to reach the above final situation.

c 2018 AI Access Foundation. All rights reserved.

Apt & Wojtczak

The above protocol is centralized in the sense that it consists of a globally scheduled sequences of calls. Attamah, van Ditmarsch, Grossi, and Van der Hoek (2014b) introduced and studied distributed epistemic gossip protocols. Distributed means that each agent acts autonomously, and epistemic means that the gossip protocols refer to agents knowledge. These protocols were described as formulas in an epistemic dynamic logic. Consequently they are examples of knowledge-based programs that were introduced by Fagin, Halpern, Moses, and Vardi (1997). These are programs that use tests for knowledge. Examples are protocols for the sequence transmission problem, such as the alternating bit protocol, studied by Halpern and Zuck (1992). Apt, Grossi, and Van der Hoek (2016) built upon the work of Attamah et al. (2014b) and studied distributed epistemic gossip protocols (from now on just: gossip protocols) for calls of a different type than the ones considered by Attamah et al. (2014b), which in our view are closer to the setting of distributed programming. These gossip protocols are strikingly simple in their syntax (though not semantics): they are just parallel compositions of loops in which the agents repeatedly perform a call assuming the corresponding epistemic formula (a guard) evaluates to true. This considerably simplified the task of their verification. The subject of our paper is to analyze semantics and verification of these gossip protocols. We prove the following results.

These gossip protocols are implementable.

More precisely, we show that the semantics of the underlying epistemic logic is decidable and consequently it is decidable to determine whether a guard is true after a sequence of calls.

Partial correctness of these gossip protocols is decidable.

More precisely, we show that truth in the underlying epistemic logic is decidable. This implies the claim since partial correctness of a gossip protocol can be expressed as a specific formula in this logic.

Termination of these gossip protocols is decidable.

Fair termination (in two different senses) of these gossip protocols is decidable.

Moreover, we show that the concepts of fairness and justice, that differ for arbitrary nondeterministic and distributed programs, coincide for these gossip protocols.

This implies that distributed epistemic gossip protocols are very specific programs that in particular do not have the full power of Turing machines. The obtained results, while sufficient for an analysis of the considered gossip protocols, raise a number of interesting open problems concerning both the underlying logic and the protocols and to which we return in the conclusions.

1.1 Related Work

Epistemic reasoning about gossip protocols has been recently investigated from several viewpoints. The stage was set up in the already mentioned work of Attamah et al. (2014b). We shall discuss one specific aspect of this paper, namely the type of calls, in the final section

Verification of Gossip Protocols

of the paper. Attamah, van Ditmarsch, Grossi, and Van der Hoek (2014a) presented a tool 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 ours, so this approach is not applicable to our setting. Further, van Ditmarsch, van Eijck, Pardo, Ramezanian, and Schwarzentruber (2017b) undertook a study of dynamic distributed gossip protocols in which the calls allow the agents not only to share the secrets but also to transmit the links. The purpose of that paper is to characterize such protocols in terms of the class of graphs for which they terminate. Such protocols then differ from the ones here considered, which are static.

Next, Herzig and Maffre (2015) and Herzig and Maffre (2017) studied gossip protocols that aim at achieving higher-order shared knowledge, for example knowledge of level 2 which stipulates that everybody knows that everybody knows all secrets. In particular, a protocol is presented and proved correct that achieves in (k + 1)(n 2) steps shared knowledge of level k. These matters are further investigated by Cooper, Herzig, Maffre, Maris, and Regnier (2016b), where optimal protocols for various versions of such a generalized gossip problem are given depending on various parameters, such as type of the underlying graph or the type of communication. Also gossip problems are studied in which some negative goals, such as that certain agents must not know certain secrets, are supposed to be achieved.

Further, Cooper, Herzig, Maffre, Maris, and Régnier (2016a) studied gossip protocols as an instance of multi-agent epistemic planning that is subsequently translated into the classical planning language PDDL. In turn, van Ditmarsch, Grossi, Herzig, van der Hoek, and Kuijer (2016) presented the gossip problems in an epistemic framework that provides several parameters allowing us to capture such aspects as the initial knowledge of the agents, the type of communication used, and the desired type of the protocol (for example, a symmetric one). For some of the combinations of the parameters the minimum number of calls needed to reach the final situation is established. The expected time of termination of several gossip protocols on completely connected networks was studied by van Ditmarsch, Kokkinis, and Stockmarr (2017a).

Fairness is a widely considered concept in nondeterministic and distributed computing, (see, e.g., Francez, 1986). As shown by Apt, Francez, and Katz (1988), in distributed systems it can be defined in a number of ways.

Finally, let us mention that several decidability results reported here were recently established by Apt and Wojtczak (2017a) for the logic containing the common knowledge operator. Further, Apt, Kopczyński, and Wojtczak (2017) investigated the computational aspects of the problems here studied. Building upon the work here reported it was established that 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. The computational analysis of two types of fair termination studied here was not considered.

The paper is organized as follows. In the next two sections, 2 and 3, we recall the syntax and semantics of the considered epistemic logic, originally introduced by Apt et al. (2016). Then, in Section 4 we recall the distributed epistemic gossip protocols studied in that paper and in

Apt & Wojtczak

Section 5 we discuss in detail an example of such a protocol. Next, in Section 6 we introduce an alternative, equivalent, semantics, which helps us to prove the desired decidability results. In Section 7 we prove the decidability of the problem of checking whether a formula is true after a given sequence of calls. This implies that the considered gossip protocols are implementable. In Section 8 we show that the definition of truth in the considered logic is decidable. In the subsequent two sections, 9 and 10 we apply these results to a study of gossip protocols. We establish there decidability of four properties of these protocols: partial correctness, termination, and fair termination in two different senses. Finally, in Section 11, we discuss some related open problems and recall other types of communications studied by Attamah et al. (2014b).

Throughout the paper we assume a fixed finite set A of at least three agents and a fixed set P of all secrets. We assume that each agent holds exactly one secret and that there exists a bijection between the set of agents and the set of secrets. Further, each agent is uniquely determined by his secret. To indicate this we denote the secret of agent a by A, the secret of agent b by B and so on. Our aim is to analyze what the agents know after a sequence of calls took place. So first we introduce the calls and then consider an epistemic language allowing us to refer to agents knowledge. Each call concerns two different agents, the caller (a below) and the callee (b). Apt et al. (2016) distinguished three modes of communication of a call:

push-pull, written as ab or (a, b). After this call the caller and the callee learn each others secrets,

push, written as a b. After this call the callee learns all the secrets held by the caller,

pull, written as a b. After this call the caller learns all the secrets held by the callee.

So the push-pull mode describes two-way communication, while the push and the pull modes describe one-way communication. Calls are denoted by c, d. Abusing notation we write a c to denote that agent a is one of the two agents involved in the call c (e.g., for c := ab we have a c and b c). Further, we say that a call is a b-call if agent b is involved in it. The mode of communication is concerned only with the agents involved in the call and states nothing about the effect of the call on the knowledge of other agents. Here we follow the approach of Apt et al. (2016) and stipulate that agents not involved in the call are not aware of it. This will be addressed in Definition 1 below. Other options are discussed in the last section. To discuss knowledge of the agents we consider formulas in a simple epistemic language L defined by the following grammar:

φ ::= Fap | φ | φ φ | Kaφ,

Verification of Gossip Protocols

where p P and a A. Each secret is viewed a distinct constant. In the example formulas we shall also use the disjunction φ ψ as an abbreviation for ( φ ψ), the implication φ ψ as an abbreviation for (φ ψ), and the equivalence as a shorthand for the conjunction of two implications. 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 are of the form Fap. Attamah et al. (2014b) used instead of the atomic formula Fap the knowledge formula Kap Ka p, which states that agent a knows the truth value of the proposition p. This leads to a different language in which the atomic formulas are secrets that are viewed as propositional variables. The advantage of the approach adopted by Apt et al. (2016) and followed here is that it simplifies semantics and reasoning about it. Also, it allows one to suppress one level of nesting of the modalities. In what follows we shall distinguish the following sublanguages of L:

Lpr, its propositional part, which consists of the formulas that do not use the Ka modalities,

La, where a A is a fixed agent, which consists of the formulas the only modality of which is Ka, and in which all atomic formulas are of the form Fap,

Lwn, which consists of the formulas without the nested use of the Ka modalities.

In our logic the formulas of the form Kaφ and Ka Kaφ are equivalent, so in the last sublanguage one can also allow the formulas of the form Ka Ka. . .Kaφ. All gossip protocols studied in the work of Apt et al. (2016) use as guards only formulas from Lwn, that is in a program for agent a only guards from La Lwn are used.

3. Semantics

We now recall semantics of the epistemic formulas introduced by Apt et al. (2016). It relies on the concept of a gossip situation.

3.1 Gossip Situations and Their Modifications

A gossip situation is a sequence s = (Qa)a A, where Qa P 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. We say that an agent a is an expert in a gossip situation s if he is familiar in s with all the secrets, i.e., if Qa = P. We will use the following concise notation for gossip situations. Sets of secrets will be written down as lists. e.g., the set {A, B, C} will be written as ABC. Gossip situations will be written down as lists of lists of secrets separated by dots. E.g., if there are three agents, a, b and c, then root = A.B.C and the gossip situation ({A, B}, {A, B}, {C}) will be written as AB.AB.C. Each call c transforms the current gossip situation s by modifying the sets of secrets the agents involved in the call are familiar with. This modification depends on the mode of communication. Consider a gossip situation s := (Qd)d A.

Apt & Wojtczak

Suppose c = ab.

Then c(s) := (Q d)d A, where Q a = Q b = Qa Qb, and for c {a, b}, Q c = Qc.

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

Suppose c = a b.

Then c(s) := (Q a)a A, where Q b = Qa Qb, Q a = Qa, and for c {a, b}, Q c = Qc;

So the effect of a push call is that the callee learns the secrets of the caller.

Suppose c = a b.

Then c(s) := (Q a)a A, where Q a = Qa Qb, Q b = Qb, and for c {a, b}, Q c = Qc.

So the effect of a pull call is that the caller learns the secrets of the callee.

3.2 Call Sequences

Apt et al. (2016) studied computations of the gossip protocols, so both finite and infinite call sequences were used. Here we focus mostly on the finite call sequences. So to be brief, unless explicitly stated, a call sequence is assumed to be finite. For simplicity we assume that all calls in a call sequence are of the same mode. 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 write c d to denote the fact that d extends c, i.e., that for some c we have c.c = d. We have thus two equivalent ways of representing call sequences, either as (c1, c2, . . ., cn) or as c1.c2. . ..cn. The result of applying a call sequence to a situation s is defined inductively as follows:

ϵ(s) := s, (c.c)(s) := c(c(s)).

Example 1. Let A = {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.

Hence (ac, bc, ac)(root) = (ABC.ABC.ABC). Next, consider the call sequence (a c, b c, a c). It generates the following successive gossip situations starting from root:

A.B.C a c AC.B.C b c AC.BC.C a c AC.BC.C.

Hence (a c, b c, a c)(root) = (AC.BC.C). Finally, consider the call sequence (a b, b c, c a). It generates the following successive gossip situations starting from root:

A.B.C a b A.AB.C b c A.AB.ABC c a ABC.AB.ABC.

Hence (a b, b c, c a)(root) = (ABC.AB.ABC). 2

Verification of Gossip Protocols

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 situation, agents may be uncertain about which call sequence took place. This uncertainty is captured by the appropriate equivalence relations on the call sequences. Suppose first that the mode of communication is push-pull.

Definition 1. The gossip model is a tuple M := (C, { a}a A), where each a C C is the smallest relation satisfying the following conditions:

[Base] ϵ a ϵ,

[Step] Suppose c a d.

(i) If a c, then c.c a d and c a d.c.

(ii) If there exists b A and c {ab, ba} such that c.c(root)a = d.c(root)a, then c.c a d.c.

In (i) we formalize the assumption that the agents are not aware of the calls they do not participate in. In turn, in (ii) we capture the intuition that two call sequences are indistinguishable for an agent if the sets of his calls in both sequences are the same and in each sequence he observes the same set of secrets. Note that according to our definition, for a = b, ab a ba. This means that agents are aware of who is calling whom and can differentiate between calls in which these roles are reversed. Apt et al. (2016) used a slightly different definition of (ii) according to which ab a ba. We consider the above definition more intuitive. To illustrate this definition consider the following examples. Based on (ii) we have ab a ab, so by (i) used twice we have (ab, bc) a (ab, bd). But we do not have (ab, bc) a (ba, bd), because ab a ba. We also do not have (bc, ab) a (bd, ab) since (bc, ab)(root)a = ABC = ABD = (bd, ab)(root)a. At the same time, we have by (i) used four times (bc, bd) a (cd, bc), so by (ii) (bc, bd, ab) a (cd, bc, ab). Later, in Section 6, we introduce an alternative definition of the relations a that provides additional insights in the above definition and in particular will allow us to prove that each a is an equivalence relation. Suppose now that the mode of communication is push. Then Definition 1 needs to be modified as follows. The original clause (ii) is replaced by the following clause:

(ii ) If there exists b A and c {a b, b a} such that c.c(root)a = d.c(root)a, then c.c a d.c.

Note that when b and c are different agents, then a b a a c. The intuition is that agent a is fully aware of the calls he performed. The calls a b and a c are different for him even though he does not learn anything from any of them. For instance, by (i) and (ii ) we have (a b, b c) a (b c, a b). But we do not have (b a, c b) a (c b, b a), since (b a, c b)(root)a = AB = ABC = (c b, b a)(root)a. Finally, suppose that the mode of communication is pull. Then Definition 1 needs to be modified as follows. The original clause (ii) is replaced by the following clause:

Apt & Wojtczak

(ii ) If there exists b A and c {a b, b a} such that c.c(root)a = d.c(root)a, then c.c a d.c.

For instance, by (i) and (ii ) we have (b a, c b) a (c b, b a). But we do not have (a b, b c) a (b c, a b) since (a b, b c)(root)a = AB = ABC = (b c, a b)(root)a. Now that we provided the definition of a model we recall the definition of truth, which is the same for all three modes of communication.

Definition 2. Consider the gossip model M := (C, ( a)a A) and a call sequence 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) |= φ.

Further we define

M |= φ iff c (M, c) |= φ.

When (M, c) |= φ we say that φ is true after c and when M |= φ we say that φ is true.

So a formula Fap is true after c whenever secret p 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. The knowledge operator is interpreted as customary in epistemic logic, using the equivalence relations a.

4. Gossip Protocols

Apt et al. (2016), as a follow up on the work of Attamah et al. (2014b), studied distributed epistemic gossip protocols. Their goal is to reach a gossip situation in which each agent is an expert. In other words, their goal is to transform a gossip situation in which the formula V a A Fa A V a,b A,a =b Fa B 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 and a is the caller in the call cj. Given a formula ψ La and a call c, we call the construct ψ c a rule and refer in this context to ψ as a guard. Intuitively, denotes a repeated execution of the rules, one at a time, where each time non-deterministically a rule is selected whose guard is true. Finally, by a distributed epistemic gossip protocol, in short a gossip protocol, we mean a parallel composition of component programs, one for each agent. This syntax loosely follows the syntax of the language CSP (Communicating Sequential Processes) of Hoare (1978) that extends the guarded command language of Dijkstra (1975) by disjoint parallel composition and commands for synchronous communication. CSP was realized in the distributed programming language OCCAM (see INMOS in INMOS Limited, 1984).

Verification of Gossip Protocols

Gossip protocols here considered can be seen special cases of knowledge-based programs introduced by Fagin et al. (1997). This means that one could instantiate their definition of global states, runs and actions in our setup. However, the framework we consider here is very simple (for example assignments are not allowed and only two agents are involved in each action), so a much simpler, direct, definition of computations can be given. Assume now 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 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 (M, 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 we mean a maximal rooted path in its computation tree. This tree is finitely branching, so by König s Lemma (König, 1927) if it has arbitrary long paths, then it also has infinite paths. We say that the gossip protocol P is partially correct if for all leafs c of the computation tree of P (M, c) |=

a,b A Fa B, (1)

i.e., if each agent is an expert in the gossip situation c(root). Note that a rooted finite path χ in the computation tree of P is a finite computation iff its leaf c cannot be extended by any call, so iff

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 iffthe implication

a,b A Fa B (2)

is true after every call sequence corresponding to a node of the computation tree for P. In particular if this implication is true, then P is partially correct. We say furthermore that P terminates if all its computations are finite. We also consider two variants of termination. To define them we need a subsidiary notion. We call a rule enabled after a call sequence c if its guard is true after c. Given a gossip protocol we say that an agent is enabled after a call sequence c if one of the rules in its program is enabled. We now stipulate that each finite computation is rule-fair and agent-fair. An infinite computation is rule-fair (resp. agent-fair) if all rules (resp. agents) that are enabled after infinitely many prefixes (in short, infinitely often) are selected infinitely often. We say that a gossip protocol P rule-fairly terminates (resp. agent-fairly terminates) if all its rulefair (resp. agent-fair computations) are finite. Agent-fairness was introduced by Apt et al. (2016), where it was simply called fairness.

Apt & Wojtczak

5. Example: A Protocol Over Undirected Graphs

To illustrate the power of gossip protocols consider the following example taken from the work of Apt et al. (2017). Suppose that the agents are nodes of an undirected connected graph (V, E) and that the calls can take place only between pairs of agents connected by an edge. Let Na denote the set of neighbours of node a. Consider a gossip protocol P with the following program for agent a:

[[]b Na,C PFa C Ka Fb C ab].

Informally, agent a calls a neighbour b if a is familiar with some secret (here C) and he does not know whether b is familiar with it. Despite its simplicity this protocol can exhibit a complex behaviour. Consider for instance the binary tree depicted in Figure 1 connecting agents a, b, c, d, e, f, g.

Figure 1: A connection graph

The following two example call sequences can be generated for it by the considered protocol:

(ab, ac, bd, ba, ac, be, bd, ba, ac, cf, ca, cg, cf, ca, ab, bd, be),

(bd, be, ba, ac, cf, cg, cf, ca, ab, bd, be).

To prove partial correctness of this protocol consider its exit condition

C P (Fa C Ka Fb C).

For all agents a and b and secrets C, the formula Ka Fb C Fb C is true, so the exit condition implies

C P (Fa C Fb C).

Consider now an agent a and the secret B of agent b. Let i1, . . ., ih be a path that connects b with a. So i1 = b and ih = a. The above formula implies that for g {1, . . ., h 1} we have V C P(Fig C Fig+1C). By combining these h 1 formulas we get V C P(Fb C Fa C). But Fb B is true, so we conclude Fa B. Consequently V a,b A Fa B, as desired. To prove termination it suffices to note that after each call ab the size of the set {(a, b, C) | Ka Fb C} decreases.

Verification of Gossip Protocols

6. An Alternative Equivalence Relation

From now on we focus on the push-pull mode. We provide now an alternative equivalence relation between the call sequences that is easier to work with. Also, it provides another insight into the definition of the a relations. First we introduce the following notion.

Definition 3. Fix an agent a. Its view of a call sequence c, written as ca, is a sequence of gossip situations connected by the successive calls in c in which agent a is involved. It is defined by induction as follows.

[Base] ϵa := root,

( ca c s if a c ca otherwise

where for d A

( c.c(root)d if d c s d otherwise

where s is the last gossip situation in ca.

Intuitively, a view of agent a of a call sequence c is the information he acquires by means of the calls in c he is involved in. It consists of a sequence of gossip situations connected by the calls in which a is involved. After each such call, say ab, agent a updates the set of gossips he and b are currently familiar with.

Example 2. Let us return to Example 1. So A = {a, b, c} and we consider the call sequence (ac, bc, ac). We noticed there that 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.

We now compare it with the view of agent a of the call sequence (ac, bc, ac), which is

A.B.C ac AC.B.AC ac ABC.B.ABC.

Thus, in the final gossip situation of this view, agent b is familiar with neither the secret A nor C. However, the final gossip situation of a view does not reflect agents knowledge. In fact, as we shall explain in Example 4, according to the semantics, after the above sequence of calls, agent a knows that agent b is familiar both with A and C. 2

We now introduce for each agent a an equivalence relation a between the call sequences, defined as follows: c a d iffca = da.

So according to this definition two call sequences are equivalent for agent a if his views of them are the same. The following result explains our interest in the views of call sequences.

Theorem 3 (Equivalence). For each agent a the relations a and a coincide.

Apt & Wojtczak

So two call sequences are a equivalent ifftheir views by agent a coincide.

Proof. Fix an agent a. We prove by induction on the sum of the lengths |c| + |d| that

c a d iffc a d.

[Base] |c| + |d| = 0. Then c = d = ϵ, so the equivalence holds.

[Step] |c| + |d| > 0. ( ) Suppose c a d. On the account of the minimality of the a relation only the following three cases can arise.

Case 1. For some sequence c and call c, we have a c, c = c .c and c a d. By the definition we have then ca = c a. By the induction hypothesis c a d, i.e., c a = da. Hence ca = da, i.e., c a d.

Case 2. For some sequence d and a call c, we have a c, d = d .c and c a d . Analogous to Case 1.

Case 3. For some sequences c and d and a call c, we have a c, c = c .c, d = d .c, c a d

and c(root)a = d(root)a. Let s1 be the last gossip situation in c a and s 1 the last gossip situation in d a. By the definition of a view we have ca = c a c s

and da = d a c s ,

where for d A

( c(root)d if d c (s1)d otherwise

( d(root)d if d c (s 1)d otherwise

By the induction hypothesis c a d , i.e., c a = d a and consequently s1 = s 1. Moreover, by assumption c(root)a = d(root)a, i.e., sa = s a. Further, the last calls in c and d are the same, say c = ab, so sb = sa and s b = s a, and hence sb = s b. This shows that s = s . Consequently ca = da, i.e., c a d.

( ) Suppose c a d. Three cases arise.

Case 1. The last call in c does not involve agent a. For some sequence c and call c, we have c = c .c. By the definition of a we have ca = da. Further, by definition ca = c a, so c a d. By the induction hypothesis c a d, so by the definition of a we have c a d.

Case 2. The last call in d does not involve agent a. Analogous to Case 1.

Verification of Gossip Protocols

Case 3. The last calls in c and in d involve the agent a. Since the views of c and d are the same, these last calls coincide and equal some call c. For some sequences c and d we have c = c .c and d = d .c. By the definition of a we have ca = da. This implies c(root)a = d(root)a and c a = d a, i.e., c a d . By the induction hypothesis c a d , so by the definition of a we have c a d. This concludes the proof.

This alternative definition of the equivalence relation between the call sequences makes it simpler to determine various properties of our semantics. In the examples and proofs below we use the a relation instead of a and repeatedly appeal to the Equivalence Theorem 3. Given a call sequence c, we denote by c a call sequence consisting of zero or more repetitions of c, and by c+ a call sequence consisting of one or more repetitions of c. Given two call sequences c and d, we denote by (c | d) a call sequence that is either equal c or d. Finally, for a call ab, we write ab as a shorthand for (ab | ba). We say that a call sequence c is of the form (ab) .ac.(bc)+ if c is equal to (ab)m.ac.(bc)n

for some m 0 and n > 0. An analogous terminology is used for other call sequences.

Example 4. Suppose that A = {a, b, c} and that (ac, bc, ac) a d. Recall from Example 2 that the view of agent a of the sequence (ac, bc, ac) is

A.B.C ac AC.B.AC ac ABC.B.ABC.

By the Equivalence Theorem 3 this is also the view of agent a of the call sequence d. So there are precisely two calls ac in d. Hence d is of the form (bc) .ac.(bc) .ac.(bc) . But the second gossip situation of the view is AC.B.AC, so d is actually of the form ac.(bc) .ac.(bc) . Further, the third gossip situation of the view is ABC.B.ABC, so we conclude that d is in fact of the form ac.(bc)+.ac.(bc) . This implies that (M, d) |= Fb A. It follows that (M, (ac, bc, ac)) |= Ka Fb A. We conclude that it is possible that an agent, here a, knows that another agent, here b, is familiar with his (so a s) secret even though no communication took place between them. The same argument shows that (M, (ac, bc, ac)) |= Ka Fb C, as claimed in Example 2. 2

Corollary 5.

(i) Each a is an equivalence relation.

(ii) For all c, d C and agents a, if c a d, then c(root)a = d(root)a.

Proof. (i) By the Equivalence Theorem 3.

(ii) By the Equivalence Theorem 3 it suffices to show that ca = da implies that c(root)a = d(root)a. Let c and d be the last calls in c and d, respectively, that involve agent a, i.e., such that a c and a d. This means that for some c , c , d , d we have c = c .c.c and d = d .d.d , and neither c nor d contains an a-call. By the assumption and the definition of a view we have (c .c)a = ca = da = (d .d)a and consequently, again the definition of a view, c .c(root)a = d .d(root)a. Further, c(root)a = c .c.c (root)a = c .c(root)a and d(root)a = d .d.d (root)a = d .d(root)a, which yields the claim.

Apt & Wojtczak

Note that the implication in (ii) cannot be reversed, as (ab, ab)(root)a = (ab)(root)a but (ab, ab) a ab. Next we show that an immediate repetition of a call has no effect on the truth of the formulas. More precisely, the following holds.

Theorem 6 (Stuttering). Suppose that c := c1.c.c2 and d := c1.c.c.c2. Then for all formulas φ L, (M, c) |= φ iff(M, d) |= φ.

Proof. We proceed by induction of the structure of φ. For the formulas of the form Fap it suffices to note that c(root) = d(root). The only induction step of interest is for the formulas of the form Kaφ. Suppose first that a c. Then c a d, so (M, c) |= Kaφ iff(M, d) |= Kaφ. Assume now that a c. Suppose that (M, c) |= Kaφ. Take d such that d a d . Then d is of the form d 1.c.c.d 2. Let c := d 1.c.d 2. By the induction hypothesis (M, d ) |= φ iff (M, c ) |= φ. Further, d a d implies that c a c . So (M, c ) |= φ. Hence (M, d ) |= φ and consequently (M, d) |= Kaφ. The proof in the other direction is analogous.

The above result cannot be extended to a repetition of the call sequences. Indeed, we have (M, (ab, bc)) |= Fa C, and (M, (ab, bc, ab, bc)) |= Fa C. On the other hand a monotonicity result holds for positive formulas.

Theorem 7 (Monotonicity). Suppose that φ L is a formula that does not contain the symbol. Then c d and (M, c) |= φ implies (M, d) |= φ.

Proof. We proceed by induction on the structure of φ. The only case of interest is when φ is of the form Kaψ. Suppose that c d and (M, c) |= φ. Take some call sequence d such that d a d . Then for some call sequences d1 and d 1 such that d1.d 1 = d we have c a d1. We have by the assumption (M, d1) |= ψ, so by the induction hypothesis (M, d ) |= ψ. As d was arbitrarily chosen we conclude that (M, d) |= φ.

Before we deal with the decidability matters consider the formula Ka Fb C for pairwise different agents a, b, c. The following example reveals that it can be true in some subtle ways.

Example 8. (i) First, note that a can learn that agent b is familiar with the secret C through a direct communication with b. Indeed, we have (M, (bc, ab)) |= Ka Fb C. Namely, the view of agent a of the sequence (bc, ab) is

A.B.C ab ABC.ABC.C.

So if (bc, ab) a d, then by the reasoning analogous to the one given in Example 4 d is of the form (bc)+.ab.(bc) , which implies that (M, d) |= Fb C.

(ii) Further, it is also possible that a learns that b is familiar with the secret C through a direct communication with c. Indeed, we have (M, (bc, ac)) |= Ka Fb C. To see this note that the view of agent a of the sequence (bc, ac) is A.B.C ac ABC.B.ABC.

Verification of Gossip Protocols

So if (bc, ac) a d, then by the reasoning analogous to the one given in Example 4, d is of the form (bc)+.ac.(bc) , which implies that (M, d) |= Fb C.

(iii) Also, it is possible that a learns that b is familiar with the secret C without ever communicating with b or c. Namely, we have (M, (cd, ad, bd, ad)) |= Ka Fb C. To see this note first that the view of agent a of the sequence (cd, ad, bd, ad) is

A.B.C.D ad ACD.B.C.ACD ad ABCD.B.C.ABCD.

Suppose now that (cd, ad, bd, ad) a d. Then both calls ad take place in d. Assume first that a call bc does not take place in d before the first call ad. Then by the reasoning analogous to the one given in Example 4 d is of the form (cd)+.ad.d .(bd | bc.d .cd).d .ad.d , where d = (bc | bd | cd) is a call sequence with no a-calls. Intuitively, a call cd has to take place before the first call ad, so that agent a observes that agent d is only familiar with the secret C (apart of his own secret D). A call bd or a call bc and then a call cd has to take place before the second call ad, so that agent a observers that agent d is familiar with all the secrets after its second call. Note that this form of d implies that (M, d) |= Fb C. If a call bc takes place in d, in particular before the call ad, then (M, d) |= Fb C holds directly.

(iv) In (iii) agent a learned that b is familiar with c by communicating with agent d twice. But it is also possible that a learns that b is familiar with the secret C without communicating with any agent twice. To see this note that (M, (cd, ad, bc, ac)) |= Ka Fb C. To see this note that the view of agent a of the sequence (cd, ad, bc, ac) is

A.B.C.D ad ACD.B.C.ACD ac ABCD.B.ABCD.ACD.

Suppose now that (cd, ad, bc, ac) a d and assume that a call bc does not take place in d before the call ad. By the reasoning analogous to the one given in Example 4 d is of the form (cd)+.ad.d .(bc | bd.d .cd).d .ad.d , where d = (bc | bd | cd) . Intuitively, between the calls ad and ac a call bc or a call bd followed by cd has to take place so that agent a observes that after the call ac agent c is familiar with all the secrets. This implies that (M, d) |= Fb C. If a call bc takes place in d before the first call ad, the reasoning is similar and omitted. 2

We conclude by noting that the Monotonicity Theorem 7 does not hold when we extend the call sequences to the left. Indeed, as observed in Example 8(ii), (M, (bc, ac)) |= Ka Fb C. However, (M, (cd, bc, ac)) |= Ka Fb C, since (M, (bd, cd, ac)) |= Fb C and (cd, bc, ac) a (bd, cd, ac).

7. Decidability of Semantics

In this section we show that the definition of semantics given in Definition 2 is decidable for the formulas from the language Lwn. Consider a call sequence c. If for some prefix c1.c of c we have c1(root) = c1.c(root), then we say that the call c is redundant in c. First note the following observation.

Apt & Wojtczak

Lemma 9 (Semantic Stuttering). Suppose that c := c1.c.c2 and d := c1.c2, where c is redundant in c. Then

(i) c(root) = d(root),

(ii) for all formulas φ Lpr, (M, c) |= φ iff(M, d) |= φ.

Proof. (i) By the redundancy of c we have c1(root) = c1.c(root), so c1.c.c2(root) = c1.c2(root).

(ii) We proceed by induction on the structure of φ. The only case of interest is when φ is of the form Fap. By (i) (M, c) |= Fap iffp c(root)a iffp d(root)a iff(M, d) |= Fap.

The following example shows that Lemma 9 does not extend to arbitrary formulas of L.

Example 10. In the call sequence (ab, ac, bc, ab) the second call ab is redundant since

(ab, ac, bc, ab)(root) = (ab, ac, bc)(root) = ABC.ABC.ABC.

We have (M, (ab, ac, bc, ab)) |= Ka Fb C, because if (ab, ac, bc, ab) a d then by the reasoning analogous to the one given in Example 4, d is of the form ab.ac.(bc)+.ab.(bc) . However, (M, (ab, ac, bc)) |= Ka Fb C since (ab, ac, bc) a (ab, ac). 2

Now, consider an agent a and a call sequence c. Starting from c we repeatedly remove from the current call sequence a redundant call that does not involve agent a. We call each outcome of such an iteration an a-reduction of c.

Corollary 11. Let d be an a-reduction of c. Then

(ii) c(root) = d(root),

(iii) for all formulas φ Lpr, (M, c) |= φ iff(M, d) |= φ.

Proof. (i) It suffices to note that a removal of a redundant call that does not involve agent a does not affect his view of the call sequence.

(ii) and (iii) By the repeated use of the Semantic Stuttering Lemma 9.

Given an agent a we now say that a call sequence c is a-redundant free if no call c from c such that a c is redundant in it. Clearly each a-reduction is a-redundant free. We now prove the following crucial lemma.

Lemma 12. For each agent a and a call sequence c the set of a-redundant free call sequences d such that c a d is finite and can be effectively constructed.

Verification of Gossip Protocols

Proof. Consider an a-redundant free call sequence d such that c a d. Then d has the same number, say k, of a-calls as c. Suppose d = d1.d2. . . . .dm, where m is the length of d. Associate with d the sequence of gossip situations d0(root), d1(root), . . . , dm(root), where d0 = ϵ, and di = d1.d2. . . . .di for i = 1, . . . , m. This sequence monotonically grows, where we interpret the inclusion relation componentwise. Moreover, for all calls dj such that a dj the corresponding inclusion is strict. Consequently, m, the length of d, is bounded by k + |A|2, the sum of the number of a-calls in c and of the total number of secrets in the gossip situation in which each agent is an expert. But for each m there are only finitely many call sequences of length at most m. This concludes the proof.

We can now state and prove the desired result.

Theorem 13 (Decidability of Semantics). For each call sequence c it is decidable whether for a formula φ Lwn, (M, c) |= φ holds.

Proof. We use the definition of semantics as an algorithm and prove this by induction over the structure of the formulas. The only interesting case are formulas of the form Kaψ, where ψ Lpr. Thanks to the Equivalence Theorem 3 and Corollary 11 we can rewrite the clause for Kaψ as:

(M, c) |= Kaψ iff d s.t. c a d and d is a-redundant free, (M, d) |= ψ,

and according to Lemma 12 this definition refers to an explicitly constructed finite set of call sequences d, so the problem is decidable.

We now apply this result to gossip protocols. We say that a gossip protocol is implementable if an effective procedure exists that allows one to determine whether a guard is true after a sequence of calls generated by the protocol. We have the following result.

Corollary 14. Each gossip protocol that uses as guards the formulas from Lwn is implementable.

Proof. By the Decidability of Semantics 13.

8. Decidability of Truth

Next, we show that truth definition for the formulas of the language Lwn is decidable. The key notion in our approach is the following.

Definition 4. An epistemic view is a function EV( ) defined on the set of call sequences such that for each call sequence c, EV(c) is in turn a function with the domain A {A} that assigns to each agent a A a set of gossip situations and to the set of agents A a single gossip situation. It is defined by

putting for each agent a A, EV(c)(a) = {d(root) | c a d}, and setting

EV(c)(A) = c(root).

Apt & Wojtczak

So EV(c)(a) is the set of all gossip situations consistent with agent a s observations made throughout c and EV(c)(A) is the actual gossip situation after c takes place. Note that if c a d then EV(c)(a) = EV(d)(a).

Example 15. Consider a model with three agents A = {a, b, c} and let us look at all epistemic views along the call sequence (ab, ac, ab, ac).

EV(ϵ)(A) = {A.B.C}, EV(ϵ)(a) = {A.B.C, A.BC.BC}, EV(ϵ)(b) = {A.B.C, AC.B.AC}, EV(ϵ)(c) = {A.B.C, AB.AB.C}, EV(ab)(A) = {AB.AB.C}, EV(ab)(a) = {AB.AB.C, AB.ABC.ABC}, EV(ab)(b) = {AB.AB.C, ABC.AB.ABC}, EV(ab)(c) = {A.B.C, AB.AB.C}, EV(ab, ac)(A) = {ABC.AB.ABC}, EV(ab, ac)(a) = {ABC.AB.ABC, ABC.ABC.ABC}, EV(ab, ac)(b) = {AB.AB.C, ABC.AB.ABC}, EV(ab, ac)(c) = {ABC.AB.ABC, ABC.ABC.ABC}, EV(ab, ac, ab)(A) = {ABC.ABC.ABC}, EV(ab, ac, ab)(a) = {ABC.ABC.ABC}, EV(ab, ac, ab)(b) = {ABC.ABC.ABC}, EV(ab, ac, ab)(c) = {ABC.AB.ABC, ABC.ABC.ABC}, EV(ab, ac, ab, ac)(A) = {ABC.ABC.ABC}, EV(ab, ac, ab, ac)(a) = {ABC.ABC.ABC}, EV(ab, ac, ab, ac)(b) = {ABC.ABC.ABC}, EV(ab, ac, ab, ac)(c) = {ABC.AB.ABC, ABC.ABC.ABC}.

The last equality holds since by the Equivalence Theorem 3, (ab, ac, ab, ac) c d holds iffd is of the form (ab)+.ac.(ab) .ac.(ab) . In particular (ab, ac, ab, ac) c (ba, ac, ac). We leave the checking of the other equalities to the reader. 2

Consider now the set EV(c)(a) for some call sequence c and agent a. Even though it is defined using infinitely many call sequences, it is finite because the set of gossip situations is finite. In what follows we need a stronger observation.

Lemma 16. For each call sequence c and agent a the set EV(c)(a) is finite and can be effectively constructed.

Proof. Fix an agent a. By Corollary 11 and Equivalence Theorem 3 to construct the set EV(c)(a) it suffices to consider a-redundant free call sequences d and by Lemma 12 there are only finitely many such call sequences d for which d a c.

Our interest in epistemic views stems from the following result.

Lemma 17. Suppose that EV(c) = EV(d). Then for all formulas φ Lwn, (M, c) |= φ iff (M, d) |= φ.

Verification of Gossip Protocols

So to determine whether two call sequences satisfy the same formulas of Lwn it suffices to compare their epistemic views which are finite objects.

Proof. A simple proof by induction shows that for a formula ψ Lpr and arbitrary call sequences c and d ,

c (root) = d (root) implies that (M, c ) |= ψ iff(M, d ) |= ψ. (3)

Since EV(c)(A) = c(root) and EV(d)(A) = d(root), this settles the case for φ = Fap. Now consider φ = Kaψ where ψ Lpr. Recall that

(M, c) |= Kaψ iff c a c, (M, c ) |= ψ.

Due to (3) the last condition can be rewritten as

c for which c such that c a c and c (root) = c (root), (M, c ) |= ψ.

Finally, due to the definition of EV(c)(a) this can be simplified to

c such that c (root) EV(c)(a), (M, c ) |= ψ.

Since EV(c)(a) = EV(d)(a), this settles the case for φ = Kaψ. The remaining cases of negation and conjunction follow directly by the induction.

Next, we provide an inductive definition of EV(c.c)(a) the importance of which will become clear in a moment.

Lemma 18. For any call sequence c, call c, and agent a such that a c

EV(c.c)(a) = {c(s) | s EV(c)(a) and c(s)a = c(c(root))a}.

Proof. Intuitively the condition c(s)a = c(c(root))a states that s is consistent with the observation agent a gets after call c is made in the gossip situation c(root).

( ) Take s EV(c.c)(a). By the definition of EV(c.c)(a) there exists a call sequence d.c such that d.c a c.c and s = d.c(root). So s = c(s), where s = d(root). We also have d a c, so d(root) EV(c)(a). Moreover, c(d(root))a = c(c(root))a, because d.c a c.c.

( ) Take s {c(s) | s EV(c)(a) and c(s)a = c(c(root))a}. So for some gossip situation s we have s = c(s), s EV(c)(a) and c(s)a = c(c(root))a. The second fact implies that there exists a call sequence d such that d a c and s = d(root). Now, this and the third fact imply that d.c a c.c. So d.c(root) EV(c.c)(a). Consequently also s EV(c.c)(a), since s = c(s) = d.c(root).

This brings us to the following important conclusion that the function EV(c.c) can be computed using EV(c) and c only, i.e., without referring to c. Denote the set of epistemic views by f EV and recall that C denotes the set of calls.

Corollary 19. There exists a function f : f EV C f EV such that for any call sequence c and call c EV(c.c) = f(EV(c), c).

Apt & Wojtczak

Proof. By the definition of a we have EV(c.c)(a) = EV(c)(a) if a c. Also EV(c.c)(A) = c(EV(c)(A)). This in conjunction with the above lemma implies the claim.

A crucial role in the subsequent considerations will be played by the following notion. Consider a call sequence c. If for some prefix c1.c2 of c, where c2 is non-empty, we have EV(c1) = EV(c1.c2), then we say that the call subsequence c2 is epistemically redundant in c and that c is epistemically redundant. We say that c is epistemically nonredundant if it is not epistemically redundant. Equivalently, a call sequence c1.c2. . . . .ck is epistemically redundant if the set

{EV(c1.c2. . . . .ci) | i {1, . . . , k}}

has less than k elements and is epistemically non-redundant if it has k elements. In other words, in an epistemically non-redundant call sequence the successive epistemic views along the sequence are all different.

Example 20. Let us return to Example 15. We defined there the EV( ) functions for five call sequences ϵ, ab, (ab, ac), (ab, ac, ab), and (ab, ac, ab, ac). Note that

EV(ϵ) = EV(ab) = EV(ab, ac) = EV(ab, ac, ab) = EV(ab, ac, ab, ac).

This shows that the second call ac in the call sequence (ab, ac, ab, ac) is epistemically redundant and no other call is epistemically redundant in this call sequence. Also, the call sequences ϵ, ab, (ab, ac) and (ab, ac, ab) are all epistemically non-redundant, while (ab, ac, ab, ac) is epistemically redundant. 2

The notions of a redundant call and of an epistemically redundant call differ. Indeed, we noted in Example 10 that in the call sequence (ab, ac, bc, ab) the second call ab is redundant. Further, we also noted there that (M, (ab, ac, bc, ab)) |= Ka Fb C and (M, (ab, ac, bc)) |= Ka Fb C. So by Lemma 17 the second call ab is not epistemically redundant in the call sequence (ab, ac, bc, ab). We now show a counterpart of the Semantic Stuttering Lemma 9 for epistemic views.

Lemma 21 (Epistemic Stuttering). Suppose that c := c1.c2.c3 and d := c1.c3, where c2 is epistemically redundant in c. Then EV(c) = EV(d).

Proof. Let c3 = c1.c2. . . . .ck. First note that thanks to Corollary 19 we have EV(c1.c2.c1) = EV(c1.c1), since EV(c1.c2.c1) = f(EV(c1.c2), c1) = f(EV(c1), c1) = EV(c1.c1) due to the epistemic redundancy of c2 in c. Repeating this argument for all i {1, . . . , k} we get that EV(c1.c2.c1.c2. . . . .ci) = EV(c1.c1.c2. . . . .ci). In particular EV(c) = EV(d).

Corollary 22. For every call sequence c there exists an epistemically non-redundant call sequence d such that for all formulas φ Lwn, (M, c) |= φ iff(M, d) |= φ.

Proof. By the repeated use of the Epistemic Stuttering Lemma 21 and Lemma 17.

Next, we prove the following crucial lemma.

Lemma 23. The set of epistemically non-redundant call sequences is finite.

Verification of Gossip Protocols

Proof. Recall that each epistemic view is a function from A {A} to the set of functions from A to 2|P| (this is an overestimation because for elements of A this set has only one element). There are k = 2(|A|+1) 2|A| |P| such functions, so any call sequence longer than k has an epistemically redundant call subsequence. But there are only finitely many call sequences of length at most k. This concludes the proof.

This brings us to the announced result.

Theorem 24 (Decidability of Truth). For every gossip model and formula φ Lwn, it is decidable whether M |= φ holds.

Proof. Recall that M |= φ iff c (M, c) |= φ. Thanks to Corollary 22 we can rewrite the latter as c s.t. c is epistemically non-redundant, (M, c) |= φ.

But according to Lemma 23 there are only finitely many epistemically non-redundant call sequences and by Lemma 16 their set can be explicitly constructed.

As an easy consequence we obtain the following result.

Corollary 25. It is decidable to determine whether a given gossip situation can be an outcome of a call sequence.

Proof. Let φ(s) be the following formula of Lwn that encodes the gossip situation s:

B Qa Fa B .

Then c(c(root) = s) iff c((M, c) |= φ(s)) iff (M |= φ(s)).

Apt et al. (2017) established that this problem is in fact NP-complete.

9. Decidability of Partial Correctness and Termination

We now explain how to apply the results of the previous section to show decidability of two crucial properties of a gossip protocol: partial correctness and termination. We begin by establishing monotonicity of gossip situations and epistemic views with respect to the call sequence extensions. Intuitively, we claim that as the call sequence gets longer each agent acquires more information. This can be seen as a counterpart of the Monotonicity Theorem 7. First we need to define suitable partial orderings G and EV over gossip situations and epistemic views, respectively.

Definition 5. For any two gossip situations s, s we write s G s if for all a A we have sa s a.

Note 26. For all call sequences c and d such that c d we have c(root) G d(root).

Proof. For any gossip situation s and call c we have by definition s G c(s). By induction this implies that for any call sequence c we have s G c (s). Now c d implies that d = c.c

for some c . Therefore, c(root) G c (c(root)) = d(root).

Apt & Wojtczak

Definition 6. For any two epistemic views V, V f EV we write V EV V if for all a A there exists X V (a) and an surjective (onto) function g : X V (a) such that for all s X we have s G g(s).

Lemma 27. EV is a partial order.

Proof. (Reflexivity) For any epistemic view V , we have V EV V , because for each a A we can pick V (a) as X and the identity function on V (a) as g.

(Transitivity) Suppose V, V , V are three epistemic views such that V EV V and V EV V . Then, from the definition of EV, for any a A there exist X V (a), Y V (a), and surjective functions g : X V (a) and h : Y V (a). Let Z = {s X | g(s) Y }. Note that g|Z : Z Y , i.e., the restriction of g to Z, is surjective. The composition g|Z h : Z V (a) is also surjective and for any gossip situation s Z the following holds s G g|Z(s) G h(g|Z(s)) = (g|Z h)(s).

(Antisymmetry) Suppose V, V are two epistemic views such that V EV V and V EV V . Then, from the definition of EV, for any a A there exist X V (a), Y V (a), and surjective functions g : X V (a) and h : Y V (a). Let Z = {s X | g(s) Y }. Note that g|Z : Z Y , i.e., the restriction of g to Z, is surjective. Moreover, g|Z h : Z V (a) is also surjective, and because Z V (a) is finite, Z = V (a), g|Z = g, and g h is a permutation on V (a). Similarly we can show that Y = V (a). Since (g h) is a permutation on a finite set, there exists k such that (g h)k is the identity function on V (a). Note that for any s V (a), we have s G (g h)(s), because s G g(s) G h(g(s)). Now consider the sequence s G (g h)(s) G (g h)2(s) G . . . G (g h)k(s) = s. In fact, all of the elements in this sequence have to be the same, because G is a partial order. In particular, this shows that (g h)(s) = s. Therefore, g h is the identity function on V (a). Now, for any s V (a) we have that s G g(s) G h(g(s)) = (g h)(s) = s, so g is the identity function as well. This shows that V (a) = V (a) for all a A.

The next lemma formalizes the intuition that epistemic information grows along a call sequence.

Lemma 28. For all two call sequences such that c d we have EV(c) EV EV(d).

Proof. Let d = c.c . Take a A. By a repeated application of Lemma 18 we get that EV(c.c )(a) = {c (s) | s EV(c)(a) and c c c (s)a = c (c(root))a}. It suffices then to pick X = {s EV(c)(a) | c c c (s)a = c (c(root))a} and set g(s) = c (s) for all s X. It is easy to check that such g : X EV(d) is surjective, so EV(c) EV EV(d).

Recall that a call sequence c is epistemically redundant if a prefix c1.c2 of it exists such that EV(c1) = EV(c1.c2). Using the above lemma we can now draw a stronger conclusion.

Lemma 29. Suppose that c is epistemically redundant. Then a prefix c1.c of it exists such that c1 is epistemically non-redundant and EV(c1.c) = EV(c1).

Proof. Let c1.c2 be the shortest prefix of c such that EV(c1) = EV(c1.c2). Then c1 is epistemically non-redundant. Let c2 = c1. . . . .cl. By Lemma 28 we have EV(c1) G EV(c1.c1) G EV(c1.c1.c2) G . . . G EV(c1.c1.c2. . . . .cl) = EV(c1.c2) = EV(c1). Since G is a partial order, EV(c1.c1) = EV(c1) holds.

Verification of Gossip Protocols

Finally, the following lemma allows us to modify computations using the notion of epistemic redundancy. For convenience we identify here and below a computation with the sequence of calls it generates.

Lemma 30. Suppose that c = c1.c2. . . . is a (possibly infinite) computation of a gossip protocol P such that a call ci is epistemically redundant in the prefix c1. . . . .ci. Then c with the call ci removed is also a computation of P.

Proof. By definition for every k i the call ci is epistemically redundant in c1. . . . .ck, so by Lemma 17 for every k i we have EV(c1. . . . .ck) = EV(c1. . . . .ci 1.ci+1. . . . .ck). Thus by the Epistemic Stuttering Lemma 21 for all formulas φ Lwn

(M, c1. . . . .ck) |= φ iff(M, c1. . . . .ci 1.ci+1. . . . .ck) |= φ.

This implies the claim.

We can now establish the desired results.

Theorem 31 (Decidability of Partial Correctness). Partial correctness of gossip protocols that use as guards the formulas from Lwn is decidable.

Proof. Fix a gossip protocol P. We construct in a top down fashion the subtree T of the computation tree for P so that all nodes in are T correspond to epistemically non-redundant call sequences. To this end consider an epistemically non-redundant node c and suppose that for some rule ψa j ca j we have (M, c) |= ψa j . Then we add the call sequence c.ca j as a direct descendant of c only if it is epistemically non-redundant. Consider now a leaf c of the computation tree for P. By a repeated use of Lemma 30 we can transform c into a leaf d of the computation tree for P that is epistemically nonredundant, and thus is also a leaf of T , and moreover is such that EV(c) = EV(d). By Lemma 17 the condition (1) is true after c iffit is true after d. By the above two observations P is partially correct iffthe condition (1) is true after every call sequence corresponding to a leaf of T . But by Lemma 23 T is finite and by Lemma 16 it can be effectively constructed. So the desired conclusion follows by the Decidability of Semantics Theorem 13.

Below by cω mean the infinite call sequence consisting of the infinite repetition of the call c.

Theorem 32 (Decidability of Termination). Given a gossip protocol that uses as guards the formulas from Lwn it is decidable to determine whether it always terminates.

Proof. We first prove that a gossip protocol may fail to terminate iffit can generate a call sequence c.c such that c is epistemically non-redundant and EV(c.c) = EV(c).

( ) Let c be an infinite sequence of calls generated by the protocol. There are only finitely many epistemic views, so some prefix c of c is epistemically redundant. The claim now follows by Lemma 29.

( ) Suppose that the protocol generates a sequence of calls c.c such that c is epistemically non-redundant and EV(c.c) = EV(c).

Apt & Wojtczak

Let φ be the guard associated with the call c, i.e., φ c is a rule used in the considered protocol. By assumption (M, c) |= φ, so by Lemma 17 (M, c.c) |= φ. Hence by the repeated use of the Stuttering Theorem 6, for all i 1, (M, c.ci) |= φ. Consequently, c.cω is an infinite sequence of calls that can be generated by the protocol.

The above equivalence shows that determining whether the protocol always terminates is equivalent to checking that it cannot generate a call sequence c.c such that c is epistemically non-redundant and EV(c.c) = EV(c). But given a call sequence, by the Decidability of Semantics Theorem 13, it is decidable to determine whether it can be generated by the protocol and by Lemma 16 it is decidable to determine whether a call sequence is epistemically non-redundant. Further, by Lemma 23 there are only finitely many epistemically non-redundant call sequences, so the claim follows.

10. Decidability of Fair Termination

In this section we modify the approach of the previous section and show that both forms of fair termination introduced in Section 4 are decidable. First, let us clarify various forms of termination. We say that a gossip protocol can terminate if some computation of it is finite. Obviously the following implications hold for every gossip protocol P:

P terminates P agent-fairly terminates P rule-fairly terminates P can terminate.

We now illustrate by means of examples that none of these implications can be reversed, even for partially correct gossip protocols. The first example exhibits a partially correct gossip protocol that may not terminate but does agent-fairly terminate.

Example 33. Let A = {0, . . . , k 1}, where k 3. Define i 1 = (i + 1) mod k and i 1 = (i 1) mod k. Consider a gossip protocol with the following program for each agent i A:

A P Fi A (i, i 1)].

Informally, the agents form a directed ring. Agent i calls his successor in the ring, agent i 1, if i is not an expert. This gossip protocol is partially correct since its exit condition states that each agent is an expert. However, it does not terminate. Indeed, the call (0, 1) can be infinitely repeated. On the other hand this gossip protocol agent-fairly terminates. Suppose otherwise. Consider an infinite agent-fair computation ξ. We say that an agent i becomes an expert in ξ if for some element c of ξ we have (M, c) |= V A P Fi A. We first show that some agent becomes an expert in ξ. Indeed, otherwise by agentfairness each agent infinitely often calls in ξ his successor. So for every agent i a sequence of calls (i 1, i 2), (i 2, i 3), . . ., (i 1, i), possibly interspersed with other calls, exists in ξ. After the last call agent i becomes an expert in ξ, which is a contradiction. Suppose now that some agent i becomes an expert in ξ. Then also agent i 1 becomes an expert in ξ. Indeed, otherwise by agent-fairness agent i 1 infinitely often calls agent i and eventually, by the Monotonicity Theorem 7, he does become an expert in ξ.

Verification of Gossip Protocols

We conclude that every agent becomes an expert in ξ. Again by the Monotonicity Theorem 7 the exit condition of the protocol is true after some element of ξ. This contradicts the fact that ξ is infinite. 2

In the above gossip protocol each agent has just one rule, so agent-fairness and rulefairness coincide. The next example shows that rule-fair termination and agent-fair termination may differ for partially correct protocols.

Example 34. Consider a gossip protocol with the following program for each agent a A:

C P Fa C ab].

Intuitively, agent a can call any other agent as long as a is not an expert. This protocol is partially correct, since the implication (2) is clearly true. However, it does not agent-fairly terminate when there are more than 3 agents. Indeed, suppose that |A| 4. Partition A into two groups, each consisting of at least two agents, say {a1, . . ., ak} and {b1, . . ., bm}, where k, m 1. Then

(a1, a2), (a2, a3), . . ., (ak, a1), (b1, b2), (b2, b3), . . ., (bm, b1), (a1, a2), . . .

is a sequence of calls in an infinite agent-fair computation of this protocol. Indeed, in this sequence all agents are infinitely often selected. Further, each agent learns only the secrets of the agents in its own group. So prior to each call in the above sequence no agent is an expert and consequently this sequence corresponds to a legal computation. On the other hand, this protocol rule-fairly terminates. Indeed, consider an infinite computation χ. Some agent, say a, is then infinitely selected in χ, so it never becomes an expert and hence by the form of the protocol all the rules of a are always enabled. In χ agent a never becomes familiar with the secret of some agent, say b. So the rule V C P Fa C ab is never selected in χ. Thus χ is not rule-fair. 2

Finally, we exhibit a partially correct gossip protocol that can terminate but does not rule-fairly terminate.

Example 35. This example presents a common situation in networking where each local network has a designed gateway node, which is the only one able to communicate outside of the network (e.g., using a different network communication protocol). Here, we are going to assume just two such local networks of agents A1 = {a0, a1, . . . , ak} and A2 = {b0, . . . , bm}, where k, m 1. So we have A = A1 A2, and a0, b0 are two special gateway agents. Consider the gossip protocol with the following program for each agent a Ai, where i {1, 2}:

C P Fa C ab]

Intuitively, this states that agents can only directly call anyone within their own group Ai as long they are not experts. Agent a0 has the following additional rule: Fa0B0 a0b0 and agent b0 has the following additional rule: Fb0A0 b0a0. Intuitively, these two rules state that agents a0 and b0 can communicate with each other if they do not know each other secrets. This protocol is obviously partially correct, because the implication (2) is clearly true. Further, it can terminate, as the following call sequence shows:

Apt & Wojtczak

1. each agent in A1 calls a0,

2. each agent in A2 calls b0,

3. agent a0 calls agent b0,

4. each agent in A1 calls a0,

5. each agent in A2 calls b0.

The precise order of calls within each step does not matter. Notice that in step 3 all secrets from the A1 network are passed to the A2 network and vice versa. Then in the last two steps all these secrets are propagated to every agent. Finally, it is easily to see that this protocol may not rule-fairly terminate. Indeed, let the first call be between the agents a0 and b0. Note that from that point on no communication between the networks A1 and A2 can take place. Therefore no agent will ever become an expert (for example, no agent in A1 will ever learn the secret B1) and agents will continue to call each other within their own network, even if one ensures that the computation is rule-fair. 2

To establish decidability of both forms of fair termination we shall rely on the results established in the previous section. We start with the rule-fair termination.

Theorem 36 (Decidability of Rule-Fair Termination). Given a gossip protocol that uses as guards the formulas from Lwn it is decidable to determine whether it rule-fairly terminates.

Proof. We first show that a gossip protocol does not rule-fairly terminate iffit can generate an epistemically non-redundant call sequence c such that for every call c, which is part of an enabled rule after the call sequence c, we have that EV(c.c) = EV(c).

( ) Consider an infinite rule-fair computation d = d1.d2. . . . of the considered gossip protocol. By Lemma 28 the sequence EV(d1), EV(d1.d2), . . . , is weakly increasing w.r.t. the partial order EV. As there are only finitely many epistemic views, at some point this sequence stabilizes, i.e., for some l we have EV(d1. . . . .dl) = EV(d1. . . . .dl.dl+1. . . . .dl+i) for all i > 0. Pick the smallest such l and let d = d1. . . . .dl. By Lemma 30 we can repeatedly remove the epistemically redundant calls from d without destroying the property that it is a prefix of an infinite computation. The resulting call sequence c = c1. . . . .ck is epistemically non-redundant and the resulting infinite computation c = c1.c2. . . . of the protocol is rule-fair. Further, by the above choice of l and the Epistemic Stuttering Lemma 21 EV(c) = EV(c.ck+1. . . . .ck+i) for all i > 0. Take a rule ψ c that is enabled after c, i.e., such that (M, c) |= ψ. By Lemma 17 and the choice of c, this rule is enabled after each call sequence c.ck+1. . . . .ck+i, where i > 0, that is, it is enabled infinitely often. By the rule-fairness of c this rule ψ c is infinitely often selected in it. So for some i > 1 we have c = ck+i. By the choice of k the call sequence ck+1. . . . .ck+i 1 is epistemically redundant in the call sequence c1. . . . .ck+i, so by the above equality and the Epistemic Stuttering Lemma 21:

EV(c1. . . . .ck) = EV(c1. . . . .ck.ck+1. . . . .ck+i) = EV(c1. . . . .ck.ck+i),

Verification of Gossip Protocols

i.e., EV(c.c) = EV(c) as required. ( ) Suppose that the protocol generates a sequence of calls c such that c is epistemically non-redundant and EV(c.c) = EV(c) for every call c which is part of a enabled rule after the call sequence c takes place. Let R = {φ1 c1, φ2 c2, . . . , φk ck} be the set of all enabled rules after the call sequence c. We claim that c.(c1.c2. . . . .ck)ω is a rule-fair infinite computation of this protocol. First, due to Epistemic Stuttering Lemma 21 for every 1 j k and 0 i we have EV(c.(c1.c2. . . . .ck)i.c1.c2. . . . .cj) = EV(c). This and Lemma 17 imply that all rules in R are enabled after any call sequence of the form c.(c1.c2. . . . .ck)i.c1.c2. . . . .cj for any j {1, . . ., k} and i 0. This shows that c.(c1.c2. . . . .ck)ω is an infinite computation of this protocol. Also, we know that no other rule can be enabled after c.(c1.c2. . . . .ck)i.c1.c2. . . . .cj, because otherwise such a rule would already be enabled after c and so would belong to R. This shows that c.(c1.c2. . . . .ck)ω is a rule-fair infinite computation of this protocol, because every rule enabled infinitely many times is executed infinitely many times.

Now, due to Lemma 23 there are only finitely many epistemically non-redundant call sequences to try as candidates for c. For each such call sequence, by the Decidability of Semantics Theorem 13 it is decidable to determine whether it can be generated by the protocol. For each such call sequence c we then check which rules, ψ c, are enabled after c. For each such a call c we subsequently compute EV(c) and EV(c.c) using Lemma 16 and check whether they are all equal. By the above equivalence the considered gossip protocol does not rule-fairly terminate ifffor some such call sequence c all just mentioned equalities hold.

Finally, we show that agent-fair termination is decidable, as well.

Theorem 37 (Decidability of Agent-Fair Termination). Given a gossip protocol that uses as guards the formulas from Lwn it is decidable to determine whether it rule-fairly terminates.

Proof. First we show that a gossip protocol does not agent-fairly terminate iffit can generate an epistemically non-redundant call sequence c such that each agent a enabled after c has an enabled rule ψ c such that EV(c.c) = EV(c) holds. The reasoning is completely analogous to the one presented in the proof of the previous theorem, so we omit the details. The rest of the proof is a small modification of the reasoning used in the above proof. As before there are only finitely many epistemically non-redundant call sequences c and for each such call sequence it is decidable to determine whether it can be generated by the protocol. For each such call sequence c we then check which agents are enabled after c. For each such agent we then check whether it has a rule ψ c that is enabled after c and such that EV(c) = EV(c.c), where, again, this test is decidable by Lemma 16. By the initial equivalence the considered gossip protocol does not agent-fairly terminate ifffor some such call sequence c it is possible to choose the rules in such a way that all the equalities hold.

Lehmann, Pnueli, and Stavi (1981) considered in the context of nondeterministic programs a notion related to fairness, called justice (or weak fairness). It can be readily introduced in the context of gossip protocols. An infinite computation is rule-just (resp. agentjust) if all rules (resp. agents) that from a certain moment on are always enabled (in short,

Apt & Wojtczak

eventually always enabled) are selected infinitely often. In the context of the nondeterministic programs the notions of infinite just and fair computations differ. However, this is not the case for the gossip protocols. Indeed, it is straightforward to see that an infinite rule-fair computation is also rule-just. To show the converse consider an infinite rule-just computation c = c1.c2. . . . of a gossip protocol. As in the proof of Theorem 36, on the account of Lemma 28 and the fact that there are only finitely many epistemic views, for some l we have EV(c1 . . . cl)=EV(c1 . . . cl.cl+1 . . . cl+i) for all i > 0. Suppose now that a rule, say ψ c, is infinitely often enabled. By Lemma 17 for all i > 0 (M, c1. . . . .cl) |= ψ iff(M, c1. . . . .cl.cl+1. . . . .cl+i) |= ψ,

so ψ c is eventually always enabled. Since c is rule-just, this rule is selected infinitely often. An analogous argument shows that infinite agent-just and agent-fair computations coincide. Consequently the notions of just computations do not lead to new notions of termination of gossip protocols.

11. Conclusions

In this paper we studied decidability questions concerning distributed epistemic gossip protocols considered by Apt et al. (2016). First we established that these protocols are implementable. We proved it by showing a more general statement, namely that the semantics of the introduced epistemic language Lwn is decidable. We also established that truth of the formulas of Lwn is decidable. We then used the developed apparatus to show that partial correctness of these gossip protocols is decidable, as well. Finally, we showed that the problems of determining termination and fair termination (in two different senses) of a gossip protocol are decidable, as well. The above decidability results deal only with formulas without nested modalities. An interesting open question is whether they can be extended to formulas that admit nested modalities. The main stumbling block in generalizing our proofs is that, as Example 10 shows, the crucial Semantic Stuttering Lemma 9 cannot be extended to arbitrary formulas of L. These considerations lead to another interesting open problem. Gossip protocols studied by Apt et al. (2016) are parametric in the sense that they are formulated in such a way that they do not depend on the underlying graph (for instance a ring). The same is true in the case of the protocol discussed in Section 5. The results we proved here allow us only to consider each specific gossip protocol (for example for a ring formed by 15 agents or for a specific graph with 36 nodes) separately. What is needed is a decision procedure that would allow us to consider all instances of a protocol (for example for all rings or for all graphs) simultaneously. We conjecture that this decision problem is undecidable both for partial correctness and for termination. Finally, it would be interesting to find a sound and complete axiomatization both of the logic L and of its extension that would allow one to carry out the correctness proofs of the gossip protocols axiomatically, in the style of Hoare s logic (1969).

Verification of Gossip Protocols

In the above exposition starting from Section 6 we focused on the push-pull mode of communication. A completely analogous presentation can be given for the push and pull modes. In particular, all decidability results obtained in this paper also hold for the calls in the push mode or the pull mode. The approach is the same. It calls for a modification of the notions of a view and an epistemic view for, respectively, the push and the pull mode and for an appropriate modification of the proofs of the obtained results. The details are straightforward and omitted. The semantics we introduced in Section 3 stipulates through the definition of c(s) that a call ab is not noted by any agent c {a, b}. The same is the case for the calls a b and a b. Attamah et al. (2014b) studied different type of calls, namely

ab , which stipulates that every agent c {a, b} noted that a called b,

ab0, which stipulates that every agent c {a, b} noted that some call took place, though not between whom,

ab+ which stipulates that every agent c {a, b} noted that possibly some call took place, though not between whom.

Each of these types of calls entails a notion of the equivalence relation on the call sequences that differs from the ones considered here for the calls ab, a b and a b. It would be interesting to check whether our decidability results hold for the above types of calls, as well. As a starting point for such considerations Apt, Grossi, and Van der Hoek (2018) recently provided a uniform semantics for these and other types of calls, including the ones considered in this paper. Another issue interesting to study is a natural generalization of the considered setup to conference calls. These are calls that involve two or more agents who exchange all the secrets. As the overview of related work shows, there is no single setup for a study of gossip protocols. Kermarrec and van Steen (2007) identified three crucial aspects of gossip protocols: peer selection, data exchange and data processing. We studied here a specific instance of these three aspects. The peer selection is statically determined by the underlying graph topology, while data exchange is modelled by the introduced three modes of communication: pushpull, push and pull, each considered separately, with a simultaneous communication between more than one pair of agents disallowed. In turn, data processing is realized by exchanging, respectively passing, all available information. This selection, combined with the use of epistemic guards, led to a simple yet expressive framework in which partial correctness, termination and fair termination of the resulting gossip protocols are all decidable. A different selection of the above three aspects changes the framework in a fundamental way. It would be interesting to see for which other realizations of the framework of Kermarrec and van Steen (2007) similar decidability results can be obtained. The semantics considered here can be modified to tailor it to different initial assumptions. For example, in some cases correctness of a gossip protocol may depend on the initial knowledge of the underlying network of the agents (for example that it is a directed ring). One can take this into account by assuming that each agent not only knows its own program, but also the structure of the underlying network. In other words, each agent

Apt & Wojtczak

knows which calls are syntactically correct. This leads (see Apt et al., 2016, 2017), to a modified definition of the gossip model in which instead of C one uses the set CP of valid call sequences in a gossip protocol P. Another natural approach would be to assume that each agent knows only his own network connections. This would lead to a different setup in which each agent i considers as valid a different set of call sequences Ci that he would use to evaluate formulas of the form Kiφ. A final possibility, suggested as a future work by Apt et al. (2018), would be to construct a semantics that takes into account that all agents know the gossip protocol they execute. It would be interesting to check which results remain valid for each of these three alternatives. As a final interesting research topic we would like to mention the synthesis of distributed epistemic gossip protocols from epistemic specifications. For a related work on a synthesis of knowledge-based programs see, e.g., the work of van der Meyden and Wilke (2005).

Acknowledgments

The results established in this paper were originally reported, in a shortened form, by Apt and Wojtczak (2016) and Apt and Wojtczak (2017b). We thank the reviewers of these papers and three reviewers of the present paper for helpful comments. The first author was partially supported by the NCN grant nr 2014/13/B/ST6/01807. He would like to thank Davide Grossi and Wiebe van der Hoek for helpful discussions that led to this paper. The second author was partially supported by the EPSRC grants EP/M027287/1 and EP/P020909/1.

Apt, K. R., Grossi, D., & Van der Hoek, W. (2016). Epistemic protocols for distributed gossiping. In Proc. of the 15th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2015), Vol. 215 of EPTCS, pp. 51 66.

Apt, K. R., Grossi, D., & Van der Hoek, W. (2018). When are two gossips the same? Types of communication in epistemic gossip protocols.. Submitted for publication.

Apt, K. R., Kopczyński, E., & Wojtczak, D. (2017). On the computational complexity of gossip protocols. In Proc. of the 26th International Joint Conference on Artificial Intelligence, (IJCAI 2017), pp. 765 771.

Apt, K. R., & Wojtczak, D. (2016). On decidability of a logic of gossips. In Proc. of the 15th European Conference on Logics in Artificial Intelligence (JELIA 2016), Vol. 10021 of Lecture Notes in Computer Science, pp. 18 33. Springer.

Apt, K. R., & Wojtczak, D. (2017a). Common knowledge in a logic of gossips. In Proc. of the 16th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2017), Vol. 251 of EPTCS, pp. 10 27.

Apt, K. R., & Wojtczak, D. (2017b). Decidability of fair termination of gossip protocols. In Proc. of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 21), Vol. 1 of Kalpa Publications in Computing, pp. 73 85.

Verification of Gossip Protocols

Apt, K. R., Francez, N., & Katz, S. (1988). Appraising fairness in languages for distributed programming. Distributed Computing, 2(4), 226 241.

Attamah, M., van Ditmarsch, H., Grossi, D., & Van der Hoek, W. (2014a). A framework for epistemic gossip protocols. In Proc of the 12th European Conference on Multi-Agent Systems (EUMAS 2014), pp. 193 209.

Attamah, M., van Ditmarsch, H., Grossi, D., & Van der Hoek, W. (2014b). Knowledge and gossip. In Proc. of the 21st European Conference on Artificial Intelligence (ECAI 14), Vol. 263 of Frontiers in Artificial Intelligence and Applications, pp. 21 26. IOS Press.

Cooper, M. C., Herzig, A., Maffre, F., Maris, F., & Régnier, P. (2016a). A simple account of multiagent epistemic planning. In Proc. of the 22nd European Conference on Artificial Intelligence (ECAI 16), Vol. 285 of Frontiers in Artificial Intelligence and Applications, pp. 193 201. IOS Press.

Cooper, M. C., Herzig, A., Maffre, F., Maris, F., & Regnier, P. (2016b). Simple epistemic planning: Generalised gossiping. In Proc. of the 22nd European Conference on Artificial Intelligence (ECAI 16), Vol. 285 of Frontiers in Artificial Intelligence and Applications, pp. 1563 1564. IOS Press.

Dijkstra, E. W. (1975). Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18, 453 457.

Fagin, R., Halpern, J. Y., Moses, Y., & Vardi, M. Y. (1997). Knowledge-based programs. Distributed Computing, 10(4), 199 225.

Francez, N. (1986). Fairness. Springer-Verlag, New York.

Halpern, J. Y., & Zuck, L. D. (1992). A little knowledge goes a long way: Knowledge-based derivations and correctness proofs for a family of protocols. Journal of the ACM, 39(3), 449 478.

Hedetniemi, S. M., Hedetniemi, S. T., & Liestman, A. L. (1988). A survey of gossiping and broadcasting in communication networks. Networks, 18(4), 319 349.

Herzig, A., & Maffre, F. (2015). How to share knowledge by gossiping. In Proc of the 13th European Conference on Multi-Agent Systems (EUMAS 2015), Revised Selected Papers, Vol. 9571, pp. 249 263. Springer.

Herzig, A., & Maffre, F. (2017). How to share knowledge by gossiping. AI Communications, 30(1), 1 17.

Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12, 576 580, 583.

Hoare, C. A. R. (1978). Communicating sequential processes. Communications of the ACM, 21, 666 677.

Hromkovic, J., Klasing, R., Pelc, A., Ruzicka, P., & Unger, W. (2005). Dissemination of Information in Communication Networks - Broadcasting, Gossiping, Leader Election, and Fault-Tolerance. Texts in Theoretical Computer Science. An EATCS Series. Springer.

INMOS Limited (1984). Occam Programming Manual. Prentice-Hall International, Englewood Cliffs, N.J.

Apt & Wojtczak

Kempe, D., Dobra, A., & Gehrke, J. (2003). Gossip-based computation of aggregate information. In Proc. of the 44th Annual IEEE Symposium on Foundations of Computer Science, FOCS 03, pp. 482 491. IEEE.

Kermarrec, A., & van Steen, M. (2007). Gossiping in distributed systems. Operating Systems Review, 41(5), 2 7.

König, D. (1927). Über eine schlußweise aus dem endlichen ins unendliche. Acta Litt. Ac. Sci., 3, 121 130.

Ladin, R., Liskov, B., Shrira, L., & Ghemawat, S. (1992). Providing high availability using lazy replication. ACM Transactions on Computer Systems (TOCS), 10(4), 360 391.

Lehmann, D. J., Pnueli, A., & Stavi, J. (1981). Impartiality, justice, and fairness: the ethics of concurrent termination. In Proc. of the International Colloquium on Automata Languages and Programming (ICALP 81), pp. 264 277, New York. Lecture Notes in Computer Science 115, Springer-Verlag.

Tijdeman, R. (1971). On a telephone problem. Nieuw Archief voor Wiskunde, 3(XIX), 188 192.

van der Meyden, R., & Wilke, T. (2005). Synthesis of distributed systems from knowledgebased specifications. In Proc. of the 16th International Conference CONCUR 2005, Vol. 3653 of Lecture Notes in Computer Science, pp. 562 576. Springer.

van Ditmarsch, H., Grossi, D., Herzig, A., van der Hoek, W., & Kuijer, L. B. (2016). Parameters for epistemic gossip problems. In Proc. of the 12th Conference on Logic and the Foundations of Game and Decision Theory (LOFT 2016). https://pdfs. semanticscholar.org/74b5/2c025f335ba487cac612019e39ce6c818448.pdf.

van Ditmarsch, H., Kokkinis, I., & Stockmarr, A. (2017a). Reachability and expectation in gossiping. In An, B., Bazzan, A., Leite, J., Villata, S., & van der Torre, L. (Eds.), PRIMA 2017: Principles and Practice of Multi-Agent Systems, pp. 93 109, Cham. Springer International Publishing.

van Ditmarsch, H., van Eijck, J., Pardo, P., Ramezanian, R., & Schwarzentruber, F. (2017b). Epistemic protocols for dynamic gossip. J. of Applied Logic, 20(C), 1 31.