Andreas Herzig

Faustine Maffre

How to share knowledge by gossiping

Keywords: gossip protocol, epistemic logic, shared knowledge, common knowledge, theory of mind, dynamic epistemic logic, visibility, observability

We provide a logical investigation of a simple case of communication in a network of agents called the gossip problem. Its classical version is: given n agents each of which has a secret-a fact not known to anybody else-, how many calls does it take to achieve shared knowledge of all secrets, i.e., to reach a state where every agent knows every secret? Several protocols achieving shared knowledge in 2(n-2) calls exist and were proved to be optimal: no shorter sequence of calls exists. We generalize that problem and focus on higherorder shared knowledge: how many calls does it take to obtain that everybody knows that everybody knows all secrets? More generally, how many calls does it take to obtain shared knowledge of order k? This cannot be achieved simply by communicating facts: the agents also have to communicate higher-order knowledge of facts. We give an algorithm that works in (k+1)(n-2) calls. We analyse its properties in a logic that we have investigated in previous work and that is based on the concept of observability of propositional variables by agents: Dynamic Epistemic Logic of Propositional Assignment and Observation DEL-PAO. This enables us in particular to give a formal proof of correctness of the algorithm.

Introduction: the gossip problem and its generalization

The gossip problem is typically introduced in the literature in the following terms [START_REF] Akkoyunlu | Some constraints and tradeoffs in the design of network communications[END_REF][START_REF] Hurkens | Spreading gossip efficiently[END_REF]:

There are six agents each of which knows some secret not known to anybody else. Two agents can make a telephone call and exchange all secrets they know. How many calls does it take to share all secrets, i.e., how many calls have to take place until everybody knows all secrets? call per couple of agents (i, j). This takes n(n-1) calls. But one can do much better.

To warm up consider n=3. Let s i denote agent i's secret. Shared knowledge can be attained in three calls, as can be seen by inspecting the following protocol:

1. 1 calls 2: 1 tells s 1 , and 2 tells s 2 ; 2. 1 calls 3: 1 tells s 1 and s 2 , and 3 tells s 3 ; 3. 1 calls 2: 1 tells s 3 .

After the second call, both 1 and 3 know s 1 ∧s 2 ∧s 3 . So 1 and 3 are both experts. However, 2 is not an expert yet because she does not know 3's secret: she only becomes an expert after the third call.

While the cases n=2 and n=3 are special, for n≥4 there is a general result saying that shared knowledge can be achieved in 2(n-2) calls, and that it is impossible to do better: there is no protocol with less than 2(n-2) calls [START_REF] Baker | Gossips and telephones[END_REF][START_REF] Tijdeman | On a telephone problem[END_REF][START_REF] Hajnal | A cure for the telephone disease[END_REF].

In the present paper we are interested in contexts where the goal is to achieve higher-order shared knowledge: how many calls does it take to obtain that everybody knows that everybody knows all secrets? More generally, how many calls does it take to obtain shared knowledge of order k? Such higher-order knowledge is important for social intelligence: social interaction requires the ability to reason about the other agents' mental states. In other words, an agent should entertain a theory of mind: she should have beliefs about other agents' beliefs, beliefs about what other agents believe about her, etc. Epistemic logic is an interesting tool in the investigation of theory of mind; see e.g. [START_REF] Bolander | Seeing is believing: Formalising false-belief tasks in dynamic epistemic logic[END_REF][START_REF] Ghosh | Human strategic reasoning in dynamic games: Experiments, logics, cognitive models[END_REF] for recent work on the subject.

If we make the hypothesis that there is a global clock and that everybody knows the protocol then things are easy: 2(n-2) calls achieve not only shared knowledge of all secrets, but also common knowledge of all secrets. Here we do not make that hypothesis and investigate asynchronous contexts. In such contexts, for n = 2 it still holds that a single call makes all secrets not only shared knowledge, but also common knowledge; however, for n > 2 common knowledge cannot be achieved by a finite number of calls.

We are therefore more modest and consider the goal of shared knowledge of order k. The original problem

The problem can be generalized to an arbitrary numbers of agents n≥2. A straightforward solution has one is to reach shared knowledge of order k=1. Now consider k=2. There, the agents cannot achieve the goal by communicating facts alone: they also have to communicate what they know about the facts. Let us illustrate this for n=3 agents. We modify the protocol for shared knowledge of order 1 and let the agents communicate knowledge instead of facts:

1. 1 calls 2: 1 tells K 1 s 1 , and 2 tells K 2 s 2 ; 2. 1 calls 3: 1 tells K 1 s 1 , K 1 s 2 , K 2 s 1 and K 2 s 2 , and 3 tells K 3 s 3 ; 3. 1 calls 2: 1 tells K 1 s 3 , K 3 s 1 , K 3 s 2 and K 3 s 3 , where K i ϕ reads "agent i knows that ϕ is true". After the second call, 1 and 3 are both experts of level 1: both know s 1 ∧s 2 ∧s 3 . However, none of them is an expert of level 2 because none of them knows K 2 s 3 (and so for a good reason: K 2 s 3 is not the case yet). The third call makes both 1 and 2 experts of level 2. However, agent 3 is not an expert of level 2 yet: although K 2 s 3 is the case, agent 3 does not know this. To attain that level it takes a further, fourth call between 1 and 3 (or, alternatively, between 2 and 3). This shows that the first three calls are not enough to obtain shared knowledge of order 2.

Our example illustrates that in order to attain shared knowledge of level 2, it is useful to communicate knowledge about facts (that is, knowledge of level 1). It also illustrates that it takes more calls to achieve shared knowledge of level k+1 than it takes to achieve shared knowledge of level k.

We note Gossip(k, n) the instance of the generalized gossip problem with n≥2 agents and the goal to achieve depth k≥1 of shared knowledge. So the original problem corresponds to the instance Gossip [START_REF] Akkoyunlu | Some constraints and tradeoffs in the design of network communications[END_REF][START_REF] Attamah | The pleasure of gossip[END_REF]. A solution to Gossip(k, n) is a sequence of calls between agents resulting in shared knowledge of depth k of all secrets by all agents. We are going to introduce an algorithm solving Gossip(k, n) in (k+1)(n-2) calls, for n ≥ 4. Based on results in [START_REF] Cooper | Simple epistemic planning: generalised gossiping[END_REF], we moreover establish that our algorithm is optimal: at least (k+1)(n-2) calls are necessary to achieve the goal of Gossip(k, n). Our proofs are formally rigorous: they are couched in a dynamic epistemic logic that is called DEL-PAO (Dynamic Epistemic Logic of Propositional Assignment and Observation), with epistemic operators K i , for i an agent, and dynamic operators [Call i j ], for i and j two different agents. Building on previous work on observability-based knowledge [START_REF] Su | Model checking temporal logics of knowledge via OBDDs[END_REF][START_REF] Van Der Hoek | Knowledge and control[END_REF][START_REF] Van Der Hoek | A logic of revelation and concealment[END_REF], we had introduced and studied that logic in [START_REF] Herzig | A poor man's epistemic logic based on propositional assignment and higher-order observation[END_REF].

The paper is organized as follows. Section 2 defines some notation. Section 3 presents our algorithm for n ≥ 4 agents. Section 4 recalls syntax and semantics of the dynamic epistemic logic DEL-PAO. In Section 5 we show how to capture the algorithm as a DEL-PAO program. In Section 6 we prove in DEL-PAO that the algorithm is correct and in Section 7 that our algorithm is optimal. In Section 8 we study the special cases of two and three agents and in Section 9 we briefly discuss a version of the problem with goals involving ignorance. Section 10 concludes.

Notation

In this section we introduce some notation in order to be able to formally talk about the agents' knowledge and about gossip protocols. In Section 4 we are going introduce a full-fledged logical language into which that notation can be embedded.

Let Agt = {1, . . . , n} be the set of all agents. The secret of agent i is denoted by s i . The set of propositional variables is Prop = {s i : i ∈ Agt}. To simplify things we suppose that s i is true. A more general framework where secrets can be true or false can be found in [START_REF] Attamah | Knowledge and gossip[END_REF][START_REF] Attamah | The pleasure of gossip[END_REF].

Notation for knowledge

We write K i ϕ to express that agent i knows that the formula ϕ is true.

The initial situation before the agents start gossiping is expressed by

i∈Agt s i ∧ K i s i ∧ j∈Agt, j =i ¬K j s i ∧ ¬K j ¬s i .
The goal of shared knowledge of level 1 is expressed by the formula i∈Agt K i j∈Agt s j which says that every agent knows every secret. Letting s J abbreviate the conjunction i∈J s i of secrets of agents in J, we can write this more compactly as i∈Agt K i s Agt .

Notation for shared knowledge

Let EK J ϕ denote the conjunction i∈J K i ϕ, for nonempty sets of agents J ⊆ Agt. It describes situations where ϕ is shared knowledge in J: each agent in J knows that ϕ.

We can now describe several situations of shared knowledge in a more convenient way: Let us also introduce an abbreviation for shared knowledge of level m, for m ≥ 0: we inductively define EK 0 J ϕ = ϕ and EK m+1 J ϕ = EK J EK m J ϕ. So the goal of shared knowledge of level k of all agents can be written

-EK Agt

EK k

Agt s Agt .

We drop set parentheses and write s i 1 ,...,i m instead of s {i 1 ,...,i m } and EK i 1 ,...,i m instead of EK {i 1 ,...,i m } .

Notation for calls and gossip protocols

We express calls and their consequences by means of modal operators of action as familiar from dynamic logic. The action Call i j expresses that i and j talk to each other. (It does not matter who initiates the call.)

The formula [Call i j ]ϕ expresses that ϕ is true after i and j talked to each other. So the formula

[Call i j ]EK {i, j} s {i, j}
expresses that the result of Call i j is that the secrets of i and j become shared knowledge of the group {i, j}. With the above convention this can be written [Call i j ]EK i, j s i, j . More generally, a call between i and j achieves common knowledge between i and j: we have

[Call i j ]EK m i, j s i, j
for arbitrary m.

In the sequence of calls

Call i 1 j 1 ; . . . ; Call i m j m , i 1 calls j 1 first, then i 2 calls j 2 , . . . , and finally i m calls j m . The length of the sequence is m. An instance of the generalized gossip problem, written Gossip(k, n), is given by a number of agents n and the level k of shared knowledge to be attained. A solution of Gossip(k, n) is a sequence of calls π such that

i∈Agt s i ∧ K i s i → [π]EK k Agt s Agt holds.
The above statements should be intuitively clear, even we postpone the semantics of our language to Section 4. Readers familiar with dynamic epistemic logics may take the epistemic operators K i to be operators of the standard epistemic logic S5 and may take the actions Call i j as private announcements made to i and j [START_REF] Baltag | The logic of public announcements, common knowledge, and private suspicions[END_REF][START_REF] Gerbrandy | Reasoning about information change[END_REF][START_REF] Gerbrandy | Bisimulations on Planet Kripke[END_REF][START_REF] Baltag | Logics for epistemic programs[END_REF][START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. The semantics we adopt is going to be conceptually and mathematically simpler than those of dynamic epistemic logics.

An algorithm achieving shared knowledge of depth k

Let Gossip(k, n) be an instance of the generalized gossip problem, for some k≥1 and n≥4. The following algorithm generates a sequence of (k+1)(n-2) calls. Throughout the algorithm, two of the agents, called left and right, will play a central, fixed role: each of the other agents only communicates with either left or right. The n-2 remaining agents will be numbered 0, 1, . . ., n-3.

The algorithm is made up of turns. During each turn, left and right collect the secrets of other agents. Together with the last agent they talked to in that turn, they thereby become what we call 'semi-experts'. A further call between complementary semi-experts turns them into full experts. The last agents to which left and right talked also play a crucial role. These two further semi-experts alternate: they are permuted at each turn in a way that will guarantee that the goal is reached.

In words:

-At the first turn (turn 0), agent left calls agent 0, then 1, . . . , then n-4, and finally agent right calls agent n-3; -At the second turn (turn 1), agent left calls agent n-3, then 0, then 4, . . . , then n-5, and finally agent right calls agent n-4; -... and so on.

So each turn involves n-2 calls, and overall the algorithm produces a sequence of (k+1)(n-2) calls.

In the rest of the paper, we assume that every agent index is taken modulo n-2 and omit "(mod n-2)".

Figure 1 gives a visual representation of Algorithm 1: agents 0, 1, . . ., n-3 are put on a wheel which, between each turn, rotates clockwise. Agent left calls everybody in ascending order-his sequence of calls is depicted by an orange arrow-, except the agent at the rightmost position of the wheel, then right (sequence of calls in blue) calls this agent.

Theorem 1. The minimal number of calls needed to solve the instance Gossip(k, n) of the generalized gossip problem, for k ≥ 1 and n ≥ 4, is (k+1)(n-2).

The main part of the paper is devoted to the proof of the above theorem. In sections 6 and 7 we prove that the sequence of calls produced by the algorithm is indeed a solution and that the goal cannot be achieved in less calls. Our proofs will be done in the formal language of the logic DEL-PAO; in the next two sections we introduce the logic and show how to model calls within its language.

Dynamic Epistemic Logic of Propositional

Assignment and Observation DEL-PAO Dynamic Epistemic Logic of Propositional Assignment and Observation DEL-PAO is grounded on the no-tion of observability of propositional variables. It refines a logic that was proposed and studied in a series of papers by van der Hoek, Wooldridge and colleagues under the names Epistemic Coalition Logic of Propositional Control with Partial Observability ECL-PC(PO) [START_REF] Van Der Hoek | Knowledge and control[END_REF] and Logic of Revelation and Concealment LRC [START_REF] Van Der Hoek | A logic of revelation and concealment[END_REF]. These logics stem from languages used in model checkers such as MOCHA in order to compactly describe a distributed system [START_REF] Alur | MOCHA: modularity in model checking[END_REF][START_REF] Su | Model checking temporal logics of knowledge via OBDDs[END_REF][START_REF] Van Benthem | Symbolic model checking for dynamic epistemic logic[END_REF]. The idea is that each agent has a set of propositional variables she can observe: no different truth value is possible for her. The other way round, any combination of truth values of the non-observable variables is possible for her. We recall this logic now; more details are in [START_REF] Herzig | A poor man's epistemic logic based on propositional assignment and higher-order observation[END_REF]. Further developments of our work are reported in [START_REF] Charrier | Building epistemic logic from observations and public announcements[END_REF][START_REF] Charrier | Arbitrary public announcement logic with mental programs[END_REF][START_REF] Herzig | Epistemic boolean games based on a logic of visibility and control[END_REF]. It can also be related to approaches which aim at grounding knowledge on a spatial notion of visibility [START_REF] Balbiani | Agents that look at one another[END_REF][START_REF] Gasquet | Big brother logic: logical modeling and reasoning about agents equipped with surveillance cameras in the plane[END_REF].

Observability atoms

The atomic formulas of DEL-PAO are called visibility atoms and take the form S i 1 S i 2 ...S i m p, where p is a propositional variable from a countable non-empty set Prop and i 1 , i 2 , ..., i m are agents from a finite non-empty set Agt. When m=0 then we have nothing but a propositional variable. For m=1, the atom S i 1 p reads "agent i 1 sees the value of the variable p" or "agent i 1 sees whether p is true or not", and for m=2, the secondorder observation S i 1 S i 2 p reads "agent i 1 sees whether i 2 sees the value of p"; and so on. Beyond individual observability the language of DEL-PAO also accounts for joint observability: the atom JSp reads "all agents jointly see the value of p". Metaphorically, joint attention about p is the case when there is eye contact between the agents when observing p. Joint visibility implies individual visibility: when JS p is true then S i p should also be true.

One can define first-and higher-order knowledge about literals by means of conjunctions of visibility atoms. Indeed, for a propositional variable p we have that agent i knows that p is true when p is true and i sees p. Similarly i knows that p is false when p is false and i sees p. The list below collects some equivalences that will be valid: Formally, the set of observability operators is

K i p ↔ p ∧ S i p K i ¬p ↔ ¬p ∧ S i p ¬K i p ∧ ¬K i ¬p ↔ ¬S i p K j K i p ↔ p ∧ S i p ∧ S j p ∧ S j S i p K j K i ¬p ↔ ¬p ∧ S i p ∧ S j p ∧ S j S i p n-
OBS = {S i : i ∈ Agt} ∪ {JS},
where S i stands for individual visibility of agent i and JS stands for joint visibility of all agents. The set of all sequences of visibility operators is noted OBS * and the set of all non-empty sequences is noted OBS + . We use σ , σ ′ , . . . for elements of OBS * . Finally, the set of atomic formulas is

ATM = {σ p : σ ∈ OBS * , p ∈ Prop}.
The elements of ATM are also called visibility atoms, or atoms for short. For example, JS S 2 q reads "all agents jointly see whether agent 2 sees the value of q"; in other words, there is joint attention in the group of all agents concerning 2's observation of q. The elements of ATM are noted α, α ′ , . . . , β, β ′ , . . ..

Complex formulas

Beyond atomic formulas the language of DEL-PAO has epistemic operators as well as actions, alias programs, assigning truth values to visibility atoms. It is defined by the following grammar:

ϕ ::= α | ¬ϕ | ϕ ∧ ϕ | K i ϕ | CKϕ | [π]ϕ π ::= +α | -α | π; π | π ⊔ π | ϕ?
where α ranges over ATM and i over Agt.

Our atomic programs are assignments of truth values to atoms from ATM: +α makes α true and -α makes α false. Complex programs are constructed with dynamic logic operators: π; π ′ is sequential composition ("first execute π, then π ′ "), π ⊔ π ′ is non-deterministic choice ("execute either π or π ′ , choosing non-deterministically"), and ϕ? is test ("if ϕ is true then continue the execution, else stop"). Just as in dynamic logic, the formula [π]ϕ reads "after every execution of π, ϕ is true". The formula K i ϕ reads "i knows that ϕ is true on the basis of what she observes", and CKϕ reads "all agents jointly know that ϕ is true on the basis of what they jointly observe". These epistemic operators account for forms of individual and common knowledge that are respectively obtained via individual observation and joint observation of facts. They therefore differ conceptually from the classical operators of individual and common knowledge as studied in the area of epistemic logic [START_REF] Fagin | Reasoning about Knowledge[END_REF].

The other boolean operators ⊤, ⊥, ∨, → and ↔ are defined as abbreviations, and π ϕ ("there exists an execution of π after which ϕ is true") abbreviates ¬[π]¬ϕ. Moreover, skip abbreviates ⊤? and fail abbreviates ⊥?. Finally, if ϕ then π abbreviates (ϕ?; π) ⊔ ¬ϕ?.

The set of atomic formulas of ATM occurring in the formula ϕ is noted ATM(ϕ); the set ATM(π) is defined similarly. For example, if π = q?; +S 2 p and ϕ

= [π]S 1 JS p → q, then ATM(π) = {q, S 2 p} and ATM(ϕ) = {q, S 2 p, S 1 JS p}. (So JS p / ∈ ATM(ϕ).)

Introspective valuations

The models of DEL-PAO are simply sets of visibility atoms. In order to guarantee positive and negative introspection we have to ensure that agents are always aware of what they see: for every agent i and propositional variable p, S i S i p has to be in every valuation. More generally, a valuation V is introspective when it contains every visibility atom having two consecutive S i , such as S j S i S i S k p. So in an introspective valuation an agent is aware of what she sees, every agent sees this, and every agent sees that every agent sees this, etc. Formally, a valuation V ∈ 2 ATM is introspective if and only if the following hold, for every α ∈ ATM and i ∈ Agt:

S i S i α ∈ V (C1) JS JS α ∈ V (C2) JS S i S i α ∈ V (C3) if JS α ∈ V , then S i α ∈ V (C4) if JS α ∈ V , then JS S i α ∈ V (C5)
The set of all introspective valuations is noted INTR. (C1) is about introspection of individual sight: an agent always sees whether she sees the value of an atom. (C2) requires the same for joint sight; indeed, if JS α is true then JS JS α should be true by introspection, and if JS α is false then all agents jointly see that at least one of them has broken eye contact. (C3) forces the first to be common knowledge. (C4) guarantees that joint visibility implies individual visibility. Constraints (C4) and (C5) guarantee that JS α ∈ V implies σ α ∈ V for σ ∈ OBS + . This motivates the following relation of introspective consequence between atoms: α ❀ β iff either α = β, or α = JS α ′ and β = σ α ′ for some σ .

Proposition 1 ([26]

). A valuation V ∈ 2 ATM is introspective if and only if, for every α, β ∈ ATM and i ∈ Agt:

σ S i S i α ∈ V for every σ ∈ OBS * (1) σ JS α ∈ V for every σ ∈ OBS + (2) if α ∈ V and α ❀ β then β ∈ V (3) An atom α ∈ ATM is valid in INTR if
V ∼ i V ′ iff S i α ∈ V implies V (α) = V ′ (α) V ∼ Agt V ′ iff JS α ∈ V implies V (α) = V ′ (α)
where we write V (α) = V ′ (α) when α has the same truth value in V and V ′ , i.e., when either α ∈ V and

α ∈ V ′ , or α / ∈ V and α / ∈ V ′ .
It is proven in [START_REF] Herzig | A poor man's epistemic logic based on propositional assignment and higher-order observation[END_REF] that ∼ i and ∼ Agt are equivalence relations on the set of introspective valuations INTR and that no valuation of INTR is ∼ i -or ∼ Agt -related to valuations outside of INTR.

Truth conditions and validity

Given an introspective valuation V , update operations add or remove atoms from V . This requires some care: the resulting valuation should also be introspective. For example, removing S i S i p should be impossible. Another example is when V does not contain S i p: then V ∪ {JS p} would violate (C4). So when adding an atom to V one also has to add all its positive consequences. Symmetrically, when removing an atom one also has to remove its negative consequences. Let us define the following:

Eff + (α) = {β ∈ ATM : α ❀ β} Eff -(α) = {β ∈ ATM : β ❀ α} Clearly, when V is introspective then both V ∪ Eff + (α) and V \ Eff -(α) are so, too (unless α is valid in INTR).
Now the truth conditions are as follows:

V |= α iff α ∈ V V |= ¬ϕ iff V |= ϕ V |= ϕ ∧ ψ iff V |= ϕ and V |= ψ V |= K i ϕ iff V ′ |= ϕ for all V ′ such that V ∼ i V ′ V |= CKϕ iff V ′ |= ϕ for all V ′ such that V ∼ Agt V ′ V |= [π]ϕ iff V ′ |= ϕ for all V ′ such that V R π V ′
where R π is a binary relation on valuations that is defined (by mutual recursion with the definition of |=) by:

V R +α V ′ iff V ′ = V ∪ Eff + (α) V R -α V ′ iff V ′ = V \ Eff -(α) and α is not valid in INTR V R π 1 ;π 2 V ′ iff there is U such that V R π 1 U and UR π 2 V ′ V R π 1 ⊔π 2 V ′ iff V R π 1 V ′ or V R π 2 V ′ V R ϕ? V ′ iff V = V ′ and V |= ϕ
The relation R π is defined just as in PDL for the program operators ;, ⊔ and ?. The interpretation of assignments is designed in a way such that we stay in INTR: the program +α adds all the positive consequences of α; the program -α fails if α is valid in INTR and otherwise removes all the negative consequences of α. For example, we never have V R -S 1 S 1 p V ′ , i.e., the program -S 1 S 1 p always fails.

In contrast, the program -S 1 S 2 p always succeeds, and we have V R -S 1 S 2 p (V \ {S 1 S 2 p, JS S 2 p, JS p}) because the only atoms-beyond S 1 S 2 p itself-whose consequence is S 1 S 2 p are JS S 2 p and JS p. Therefore V |= [-S 1 S 2 p]JS p for every V .

Similarly to the relations ∼ i and ∼ Agt , it is proven in [START_REF] Herzig | A poor man's epistemic logic based on propositional assignment and higher-order observation[END_REF] that each R π only relates valuations in INTR to valuations in INTR. Therefore there is no risk to leave the set of introspective valuations when interpreting a modal operator.

When V |= ϕ we say that V is a model of ϕ. The set of (not necessarily introspective) models of ϕ is noted

ϕ . A formula ϕ is satisfiable in INTR if ϕ has an in- trospective model, i.e., if ϕ ∩ INTR = / 0; it is valid in INTR if INTR ⊆ ϕ .
In this case, we also say that ϕ is a validity of DEL-PAO. A formula ϕ is plainly satisfiable if it has a model, i.e., if ϕ = / 0; it is plainly valid if ϕ is true in all models, i.e., if ϕ = 2 ATM . For example, JS p ∧ ¬S i p is plainly satisfiable but not satisfiable in INTR. On the other hand, ¬[-S 1 S 2 p]JS p is valid in INTR (and even plainly valid).

Relevant atoms

For atoms, the connection between visibility and knowledge is clear: the equivalences

K i α ↔ S i α ∧ α K i ¬α ↔ S i α ∧ ¬α
are plainly valid. This motivates the notion of relevant atoms of a formula ϕ and of a program π, noted RATM(ϕ) and RATM(π), that is defined recursively as follows:

RATM(α) = {α} RATM(¬ϕ) = RATM(ϕ) RATM(ϕ ∧ ϕ ′ ) = RATM(ϕ) ∪ RATM(ϕ ′ ) RATM(K i ϕ) = RATM(ϕ) ∪ {S i α : α ∈ RATM(ϕ)} RATM(CKϕ) = RATM(ϕ) ∪ {JS α : α ∈ RATM(ϕ)} RATM([π]ϕ) = RATM(π) ∪ RATM(ϕ) RATM(+α) = {α} RATM(-α) = {α} RATM(π; π ′ ) = RATM(π) ∪ RATM(π ′ ) RATM(π ⊔ π ′ ) = RATM(π) ∪ RATM(π ′ ) RATM(ϕ?) = RATM(ϕ)
For example,

RATM(q ∧ CKK i p) = {q, p, S i p, JS p, JS S i p}
This illustrates that RATM(ϕ) includes ATM(ϕ): we have ATM(q ∧ CKK i p) = {q, p}.

In the gossip problem, we will mainly be interested in (conjunctions of) formulas of the form K i 1 . . . K i m α.

Here are two useful properties of such formulas.

Lemma 1. The equivalence

K i 1 . . . K i m α ↔ β∈RATM(K i 1 ...K im α) β is plainly valid, for m ≥ 0.
Proof. We use induction on m. For m = 0 we have RATM(α) = α and the equivalence is obvious. For m ≥ 1, suppose

K i 1 . . . K i m α ↔ β∈RATM(K i 1 ...K im α)
β is plainly valid. Take V ∈ 2 ATM . Then:

V |= K i K i 1 . . . K i m α iff V |= K i β∈RATM(K i 1 ...K im α) β iff V |= β∈RATM(K i 1 ...K im α) K i β iff V |= β∈RATM(K i 1 ...K im α) (β ∧ S i β) iff V |= β∈RATM(K i 1 ...K im α) β ∧ β∈RATM(K i 1 ...K im α) S i β iff V |= β∈RATM(K i 1 ...K im α) β ∧ β∈{S i γ:γ∈RATM(K i 1 ...K im α)} β iff V |= β∈RATM(K i 1 ...K im α) ∪ {S i γ:γ∈RATM(K i 1 ...K im α)} β iff V |= β∈RATM(K i K i 1 ...K im α) β ,
hence the result.

We write r 1 , . . . , r p ⊑ 1, . . . , m when r 1 , . . . , r p is a subsequence of {1, . . . , m}. For example, we have 1, 3, 4 ⊑ 1, 2, 3, 4, 5 and ⊑ 1, 2, 3, 4, 5 but not 1, 4, 3 ⊑ 1, 2, 3, 4, 5 .

Lemma 2. We have, for m ≥ 0:

RATM(K i 1 . . . K i m α) = {S i r 1 . . . S i rp α : r 1 , . . . , r p ⊑ 1, . . . , m }
Proof. We use induction on m. The case m = 0 is obvious since RATM(α) = {α} and the only subsequence of is . For m ≥ 1, suppose

RATM(K i 1 . . . K i m α) = {S i r 1 . . . S i rp α : r 1 , . . . , r p ⊑ 1, . . . , m }.
Then:

RATM(K ℓ K i 1 . . . K i m α) = RATM(K i 1 . . . K i m α) ∪ {S ℓ α ′ : α ′ ∈ RATM(K i 1 . . . K i m α)} = {S i r 1 . . . S i rp α : r 1 , . . . , r p ⊑ 1, . . . , m } ∪ {S ℓ α ′ : α ′ ∈ {S i r 1 . . . S i rp α : r 1 , . . . , r p ⊑ 1, . . . , m }} = {S i r 1 . . . S i rp α : r 1 , . . . , r p ⊑ 1, . . . , m } ∪ {S ℓ S i r 1 . . . S i rp α : r 1 , . . . , r p ⊑ 1, . . . , m } = {S i r 1 . . . S i rp α : r 1 , . . . , r p ⊑ ℓ, 1, . . . , m }, hence the result.
Lemma 1 tells us that relevant atoms provide a link between visibility atoms-that are modified by the calls-and epistemic operators. Lemmas 1 and 2 will be useful in the next section when we will study properties of gossip calls.

Expressing calls in the language of DEL-PAO

Our logic provides the resources we need to model calls between agents and to reason about the evolution of their knowledge. Before proving that our algorithm is correct we show how to express calls and we establish their properties.

In the standard version of the gossip problem, agents only communicate their factual knowledge. As we have seen, they also have to tell what they know about others in order to achieve higher-order knowledge: for shared knowledge of level k they have to exchange all their knowledge up to depth k-1.

Let k be the level of shared knowledge to be attained. Let i and j be two agents. For a given integer m, we note {S i , S j } ≤m the set all non-empty sequences of vis-ibility operators S i and S j of length at most m. For example:

{S i , S j } ≤2 = {S i , S j , S i S i , S i S j , S j S i , S j S j }.
Then Call i j is the sequential composition of programs of the form:

if K i K i 1 • • •K i m s ∨ K j K i 1 • • •K i m s then + σ 1 S i 1 • • • S i m s; . . . ; +σ ℓ S i 1 • • • S i m s
for secret s in Prop, integer m ≤ k-1, agents i 1 , . . . , i m ∈ Agt and sequences {S i , S j } ≤k-m = {σ 1 , . . . , σ ℓ }. For example, for k = 3 the following is an element of the sequence:

if K i K ℓ s ∨ K j K ℓ s then + S i S ℓ s; +S j S ℓ s; +S i S i S ℓ s; +S i S j S ℓ s; + S j S i S ℓ s; +S j S j S ℓ s
That piece of program tests whether K ℓ s is known by i or j and if so makes S ℓ s visible for both i and j and i's observation of S ℓ s visible for j, and vice versa. (Observe that the additions +S i S i S k s and +S j S j S k s are trivial because they are introspectively valid.) Some properties of the program Call i j and its interaction with the shared knowledge operator via the relevant atoms will be useful in our proofs.

First of all, the dynamic operators [Call i j ] and the shared knowledge operators EK J are normal modal operators. So in particular

[Call i j ]ϕ ∧ [Call i j ]ψ ↔ [Call i j ](ϕ ∧ ψ)
and

(EK J ϕ ∧ EK J ψ) ↔ EK J (ϕ ∧ ψ)
are plainly valid. Moreover, we can put coalitions together: the schema

(EK J 1 ϕ ∧ EK J 2 ϕ) ↔ EK J 1 ∪J 2 ϕ
is plainly valid for every J 1 , J 2 ⊆ Agt. (To see this reduce EK according to its definition.) Finally, calls preserve positive knowledge and produce shared knowledge, which is a property that we state formally:

Proposition 2. Let s ∈ {s i : i ∈ Agt} and m ≥ 0. Let ϕ be of the form either K i 1 . . . K i m s or EK J 1 . . . EK J m s. Then the formulas:

ϕ → [Call i j ]ϕ (Prsv) K i ϕ → [Call i j ]EK k-m i, j ϕ (Incr)
are plainly valid.

Proof. We prove each implication thanks to properties of DEL-PAO.

The proof of (Prsv) is straightforward: it is plainly valid because ϕ does not contain negations and calls only make atoms true.

The proof of (Incr) is a bit more involved. We only prove the case where ϕ = K i 1 . . . K i m s; the case ϕ = EK J 1 . . . EK J m s is similar since EK J is a conjunction of K i . We have seen in Lemma 1 that

ϕ ↔ β∈RATM(ϕ)
β is plainly valid. Moreover, we have:

RATM(EK m i, j ϕ) = {σα : α ∈ RATM(ϕ), σ ∈ {S i , S j } ≤m }
by the definition of RATM(.). Therefore we want to prove that:

K i ϕ → [Call i j ]
β∈{σα:α∈RATM(ϕ),σ∈{S i ,S j } ≤k-m } β .

We have:

K i K i 1 . . . K i m s → K i K i r 1 . . . K i rp s,
for every r 1 , . . . , r p ⊑ 1, . . . , m , by axiom T of standard epistemic logic. Since K i K i r 1 . . . K i rp s obviously implies K i K i r 1 . . . K i rp s ∨ K j K i r 1 . . . K i rp s, for every subset r 1 , . . . , r p ⊑ 1, . . . , m , we have:

K i K i 1 . . . K i m s → [Call i j ] β∈{σS ir 1 ...S ir p s:σ∈{S i ,S j } ≤k-p } β ,
by the definition of the programs composing Call i j . This means that:

K i K i 1 . . . K i m s → [Call i j ]
β∈{σS ir 1 ...S ir p s:σ∈{S i ,S j } ≤k-m } β , because p ≤ m. Since this is true for any r 1 , . . . , r p ⊑ 1, . . . , m , we can apply Lemma 2 and obtain:

K i K i 1 . . . K i m s → [Call i j ] β∈{σα:α∈RATM(K i 1 ...K im s), σ∈{S i ,S j } ≤k-m } β ,
which is our result.

Formally, the program corresponding to the turn t of Algorithm 1 is therefore:

turn t = Call

Correctness of the algorithm

We now prove that the algorithm returns a solution. Let us write the set of agents as Agt = {left, right, 0, . . . , n-3}.

Remember that Prop = {s i : i ∈ Agt} is the set of propositional variables. The initial state is modelled by the valuation

V 0 = {s i : i ∈ Agt} ∪ {S i s i : i ∈ Agt} ∪ {α : α is valid in INTR}.
So all secrets are true, each agent knows her own secret, and moreover the introspectively valid atoms are true (so V 0 is introspective). We have:

V 0 |= i∈Agt K i s i ∧ j∈Agt, j =i ¬K j s i .
An agent is an expert for depth t if her personal goal for depth t is reached. Precisely, agent i is an expert for depth t ≥ 1 if and only if we have:

K i EK t-1 Agt s Agt .
The dynamic modalities of DEL-PAO nicely allow to express that a further call would turn an agent i into an expert, i.e., that i is a semi-expert. Indeed, two agents i and j are complementary for depth t ('semi-experts'), noted compl t (i, j), if a call between i and j would make them both experts for depth t. More formally:

compl t (i, j) def = [Call i j ]EK i, j EK t-1 Agt s Agt .
Furthermore, two pairs of agents (i 1 , i 2 ) and ( j 1 , j 2 ) are complementary for depth t if and only if we have:

compl t (i 1 , j 1 ) ∧ compl t (i 1 , j 2 ) ∧ compl t (i 2 , j 1 ) ∧ compl t (i 2 , j 2 ).
We will prove that at each turn, two pairs of agents are complementary: the first pair is agent left along with the last agent she called at this turn, and the second is agent right along with the last (and only agent) she called at this turn.

The first turn is a special case where semi-experts of depth 1 are produced.

Lemma 3. We have:

V 0 |= [turn 0 ] EK left,n-4 s left,0,...,n-4 ∧ EK right,n-3 s right,n-3 .
Proof. Let us simply write "i j" for the call between i and j in proofs. The first turn (turn 0) of Algorithm 1 produces the following sequence of calls: left0; left1; . . . ; left(n-4); right(n-3).

By formula (Incr) of Proposition 2 we have:

V 0 |= [Call left 0 ]EK left,0 s left,0
and therefore:

V 0 |= [Call left 0 ]K left s left,0 .
We do the same for the next call:

V 0 |= [Call left 0 ; Call left 1 ]EK left,1 s left,0,1 ⇒ V 0 |= [Call left 0 ; Call left 1 ]K left s left,0,1 .
And so on until:

V 0 |= [Call left 0 ; Call left 1 ; . . . ; Call left n-4 ] EK left,n-4 s left,0,1,...,n-4 .
In the same vein we also have:

V 0 |= [Call right n-3 ]EK right,n-3 s right,n-3 .
By (Prsv) of Proposition 2 we then obtain: We now characterize the turns after turn 0 . Lemma 4. For t ≥ 1, we have:

V 0 |= [Call
V 0 |= [turn 0 ; . . . ; turn t ] EK left,n-4-t EK left,0-t,...,n-4-t EK t-1 Agt s Agt ∧ EK right,n-3-t EK right,n-3-t EK t-1 Agt s Agt .
Proof. We use induction on t. Both cases resemble the proof of Lemma 3.

Base case: t = 1. Turn 1 of Algorithm 1 produces the following sequence: left(n-3); left0; left1; . . . ; left(n-5); right(n-4).

By Lemma 3 and (Incr) of Proposition 2 we have:

V 0 |= [turn 0 ][Call left n-3 ]EK left,n-3 EK left,n-3 s Agt ⇒ V 0 |= [turn 0 ][Call left n-3 ]K left EK left,n-3 s Agt .
Then again by (Incr):

V 0 |= [turn 0 ][Call left n-3 ; Call left 0 ]EK left,0 EK left,n-3,0 s Agt ⇒ V 0 |= [turn 0 ][Call left n-3 ; Call left 0 ]K left EK left,n-3,0 s Agt ,
and for the next call:

V 0 |= [turn 0 ][Call left n-3 ; Call left 0 ; Call left 1 ] EK left,1 EK left,n-3,0,1 s Agt ⇒ V 0 |= [turn 0 ][Call left n-3 ; Call left 0 ; Call left 1 ] K left EK left,n-3,0,1 s Agt ,
and so on until: Similarly we have:

V 0 |= [turn 0 ][Call
V 0 |= [turn 0 ][Call right n-4 ]EK right,n-4 EK right,n-4 s Agt .
Finally we obtain the result by (Prsv) of Proposition 2:

V 0 |= [turn 0 ][Call
V 0 |= [turn 0 ; turn 1 ] EK left,n-5 EK left,n-3,0,1,...,n-5 s Agt ∧ EK right,n-4 EK right,n-4 s Agt .
Inductive case. The reasoning is similar, but generalized to turn t+1. Suppose the formula is true for turn t. The turn t + 1 is: left(n-3-t); left(0-t); . . . ; left(n-5-t); right(n-4-t).

By our induction hypothesis and (Incr) of Proposition 2 we have:

V 0 |= [turn 0 ; . . . ; turn t ][Call left n-3-t ] EK left,n-3-t EK left,n-3-t EK Agt EK t-1 Agt s Agt ,
that is:

V 0 |= [turn 0 ; . . . ; turn t ][Call left n-3-t ] EK left,n-3-t EK left,n-3-t EK t
Agt s Agt , which implies:

V 0 |= [turn 0 ; . . . ; turn t ][Call left n-3-t ] K left EK left,n-3-t EK t Agt s Agt .
Then by (Prsv) of Proposition 2:

V 0 |= [turn 0 ; . . . ; turn t ][Call left n-3-t ; Call left 0-t ] EK left,0-t EK left,n-3-t,0-t EK t Agt s Agt ⇒ V 0 |= [turn 0 ; . . . ; turn t ][Call left n-3-t ; Call left 0-t ] K left EK left,n-3-t,0-t EK t Agt s Agt ,
. . . and so on until:

V 0 |= [turn 0 ; . . . ; turn t ][Call left n-3-t ; Call left 0-t ; . . . ; Call left n-5-t ] EK left,n-5-t EK left,n-3-t,0-t,...,n-5-t EK t Agt s Agt .
Moreover, by (Incr):

V 0 |= [turn 0 ; . . . ; turn t ][Call right n-4-t ] EK right,n-4-t EK right,n-4-t EK Agt EK t-1 Agt s Agt ,
that is:

V 0 |= [turn 0 ; . . . ; turn t ][Call right n-4-t ] EK right,n-4-t EK right,n-4-t EK t Agt s Agt .
We end as usual with (Prsv):

V 0 |= [turn 0 ; . . . ; turn t ][Call left n-3-t ; . . . ; Call left n-5-t ; Call right n-4-t ] EK left,n-5-t EK left,n-3-t,...,n-5-t EK t Agt s Agt ∧ EK right,n-4-t EK right,n-4-t EK t Agt s Agt ⇔ V 0 |= [turn 0 ; . . . ; turn t ; turn t+1 ] EK left,n-5-t EK left,n-3-t,...,n-5-t EK t Agt s Agt ∧ EK right,n-4-t EK right,n-4-t EK t Agt s Agt ,
which is our result for t+1.

Lemma 5. After turn t-1 of Algorithm 1, the pairs (left, n-3-t) and (right, 0-t) are complementary for depth t.

Proof. From Lemma 4 we can deduce:

V 0 |= [turn 0 ; . . . ; turn t-1 ] K left EK left,1-t,...,n-3-t EK t-2 Agt s Agt ∧ K right EK right,0-t EK t-2 Agt s Agt .
Applying (Incr) of Proposition 2 we obtain:

V 0 |= [turn 0 ; . . . ; turn t-1 ][Call left right ] EK left,right EK Agt EK t-2 Agt s Agt ,
that is:

V 0 |= [turn 0 ; . . . ; turn t-1 ][Call left right ] EK left,right EK t-1 Agt s Agt ,
which is equivalent to:

V 0 |= [turn 0 ; . . . ; turn t-1 ]compl t (left, right).
By the same reasoning for left and 0-t, right and n-3-t, and finally n-3-t and 0-t, we obtain that each of them are complementary, hence the result. Proof. By Lemma 6, the goal for depth t is reached after turn t of Algorithm 1. Thus the goal for depth k is reached after turn k (k+1 turns), i.e., at the end of the algorithm.

Proposition 3 implies that at most (k+1)(n-2) calls are required to solve the instance Gossip(k, n) of the generalized gossip problem.

Optimality of the algorithm

In this section, we prove that the sequence of calls returned by our algorithm has an optimal length. Our optimality result is derived from that of [START_REF] Cooper | Simple epistemic planning: generalised gossiping[END_REF].

We first prove a property of the gossip problem that may seem obvious but that we prefer to clarify. Lemma 7. Suppose m agents know a fact ϕ not known to the remaining agents. Then it takes at least n-m calls for the remaining agents to learn ϕ.

Proof. It suffices to prove that a call Call i j increases the knowledge on a fact ϕ of at most one agent. We distinguish four cases, depending on the knowledge of i and j about ϕ.

-Neither i nor j know ϕ. Then K i ϕ ∨ K j ϕ is false and no agent knows ϕ after Call i j .

i knows ϕ but j does not know ϕ. Then K i ϕ ∨ K j ϕ is true and both agents know ϕ after Call i j , but only j learned it.

i does not know ϕ but j knows ϕ. Then K i ϕ ∨ K j ϕ is true and both agents know ϕ after Call i j , but only i learned it.

i and j know ϕ. Then K i ϕ ∨ K j ϕ is true and both agents know ϕ after Call i j , but no one learned it. Therefore n-m calls are necessary to spread a piece of gossip to n-m agents.

Proposition 4. The minimal number of calls needed to solve the instance Gossip(k, n) of the generalized gossip problem, for k≥1 and n≥4, is at least (k+1)(n-2).

Proof. We use induction on k.

Base case: k=1. As we have seen, for k=1 the lower bound 2(n-2) was established in the literature [START_REF] Baker | Gossips and telephones[END_REF][START_REF] Tijdeman | On a telephone problem[END_REF][START_REF] Hajnal | A cure for the telephone disease[END_REF].

Inductive case. Suppose that at least (k+1)(n-2) calls are needed to achieve the goal for depth k. This implies that after (k+1)(n-2) -1 calls, at least one agent, let us call her i, does not know a piece of information of depth k-1:

V 0 |= [Call i 1 j 1 ; . . . ; Call i (k+1)(n-2)-1 j (k+1)(n-2)-1 ]¬K i K ℓ 1 • • • K ℓ k-1 s.
Remark that i could also ignore facts of a lower depth; in this case she would also ignore facts of depth k-1 by the truth axiom T. For example, suppose that i does not know the secret of 1; then she cannot know that 2 knows the secret of 1, and that 1 knows that 2 knows the secret of 1, and so on.

Then the (k+1)(n-2)-th call involves i (otherwise her knowledge does not evolve) and another agent, say j. It establishes not only

K i K ℓ 1 • • • K ℓ k-1 s
and thus the goal for depth k:

V 0 |= Call i 1 j 1 ; . . . ; Call i (k+1)(n-2)-1 j (k+1)(n-2)-1 Call i j EK k Agt s Agt ,
but also the fact that i and j both know this:

V 0 |= Call i 1 j 1 ; . . . ; Call i (k+1)(n-2)-1 j (k+1)(n-2)-1 Call i j EK i, j EK k Agt s Agt ,
while no other agent does:

V 0 |= [Call i 1 j 1 ; . . . ; Call i (k+1)(n-2)-1 j (k+1)(n-2)-1 ][Call i j ] ℓ∈Agt\{i, j} ¬K ℓ EK k Agt s Agt .
To establish the goal for depth k+1, i.e., to establish EK Agt EK k Agt s Agt , it is necessary to distribute EK k Agt s Agt from i and j to all other agents. By Lemma 7, we know that this takes at least n-2 calls. Therefore, we need (k+1)(n-2)+n-2 = (k+2)(n-2) calls to achieve the goal for depth k+1.

Propositions 3 and 4 together ensure Theorem 1, i.e., that the minimal number of calls needed to solve the instance Gossip(k, n) of the generalized gossip problem, for k ≥ 1 and n ≥ 4, is exactly (k+1)(n-2).

The case of two and three agents

Our algorithm only works when four or more agents are involved; it cannot be applied when there are only two and three agents.

The former case is easy: only one call is necessary for two agents to reach knowledge on their secrets of level k, whatever k is. (This is ensured by formula (Incr) of Proposition 2.) Obviously, less calls are not sufficient given the agents' initial ignorance about the other's secret.

Consider the case of three agents, say 0, 1 and 2. We give an algorithm that takes k+2 turns of one call each.

Algorithm 2. For t = 0..k do agent 0 calls agent (t (mod 2)) + 1.

The algorithm consists in sequences of the form Call 0 1 ; Call 0 2 ; Call 0 1 ; Call 0 2 ; . . ., k+2 times. Hence each turn contains one call: turn 0 = Call 0 1 , turn 1 = Call 0 2 , turn 2 = Call 0 1 , and so on. We prove that the algorithm is correct and optimal.

Theorem 2. The minimal number of calls to solve the instance Gossip(k, 3) of the generalized gossip problem, for k ≥ 1, is k+2. Proposition 5. The sequence resulting from Algorithm 2 gives a solution to the generalized gossip problem for k≥1 and n=3.

Proof. We use induction on k.

Base case: k=1. It is easy to check that the sequence Call 0 1 ; Call 0 2 ; Call 0 1 establishes the goal for depth 1.

Inductive case. Suppose k+2 turns of the algorithm achieve the goal for depth k:

V 0 |= [turn 0 ; turn 1 ; . . . ; turn k+2 ]EK k Agt s Agt .

Because turn k+2 = Call 0 (k+2 (mod 2))+1 , we also have: Proof. This proof is similar to the proof of optimality for n ≥ 4 (see Proposition 4).

V 0 |= [
Base case: k=1. It was proven-and it is easy to check-that 3 calls are necessary, in the original problem, when three agents are involved [START_REF] Baker | Gossips and telephones[END_REF][START_REF] Tijdeman | On a telephone problem[END_REF][START_REF] Hajnal | A cure for the telephone disease[END_REF].

Inductive case. Suppose that at least k+2 calls are necessary to achieve the goal for depth k. Then after k+1 calls, at least one agent i does not know a piece of information of depth k-1. The k+2-th call, between i and j, makes i know this piece of information, and i and j be aware of this. At least one call is necessary to inform the third agent that the goal for depth k was reached, establishing the goal for depth k+1 in k+3 calls.

This establishes Theorem 2, i.e., the minimal number of calls needed to solve the instance Gossip(k, 3) of the generalized gossip problem is exactly k+2.

Gossiping with ignorance goals

In the gossip problem, we aim at full knowledge of every agent. We could also consider scenarios where we want that some agents do not learn some secrets. Assuming agents are obliged to tell all the secrets they know (say, for example, because they do not know the goal), the ordering of calls might be influenced by these 'ignorance goals.' This section discusses some aspects of this variant which, to the best of our knowledge, was not investigated before. Unlike the version with the 'full knowledge' goal, we do not provide a result on the number of calls or a generic algorithm, but rather protocols for some specific cases and general remarks.

Let us start with the original gossip problem where the goal is to achieve shared knowledge of order k=1. Suppose we do not want agent 1 to know the secret of 2, and full knowledge otherwise. Our goal is:

EK Agt\{1} s Agt ∧ K 1 s Agt\{2} ∧ ¬K 1 s 2 .
While this is obviously unsolvable for 2 agents, for at least 3 agents a successful protocol is one where 1 calls every other agent but 2, and then all agents but 1 call each other until their knowledge is shared. Slightly more generally, if 1 must not know the secret of 2, . . ., m then she should call m+1, . . ., n before they call any of 2, . . ., m, then 2, . . ., m, m+1, . . ., n can freely share their knowledge.

Things get quickly complicated, even for k=1, when we require several agents to be ignorant. For example, suppose n=4 and suppose agent 1 should not know the secret of agent 3, while 2 should not know the secret of 4. Then 1 should call 2 first, before she calls 4 and before 2 calls 3. Then 1 can call 4, 2 can call 3 and 3 can call 4. Now suppose that 1 should not know the secret of 3, while 3 should not know the secret of 1. Then no sequence of calls leads to a solution, since every agent that 1 calls cannot be called by 3 and conversely. Now consider higher-order order goals. Take k=2 and suppose we want 1 not to know whether 2 knows the secret of 3 (but we do want 2 to know the secret of 3). This means that the goal is:

EK Agt\{1} EK Agt s Agt ∧ (K 1 EK Agt\{2} s Agt ∧ K 1 K 2 s Agt\{3} ) ∧ ¬K 1 K 2 s 3 .
Then the following protocol is a solution:

1. Agent 2 calls every agent but 3; 2. All agents but 2 call each other until full knowledge of depth 2 is acquired; 3. Agent 2 calls every agent but 1.

After the second step, every agent i different from 2 has almost reached her goal, except that she does not know whether 2 knows the secret of 3 (because it is not the case yet). At the third step, 2 calls everyone but 1 in order to learn 3's secret, acquire the required depth of knowledge and inform every other agent.

Remark that if we increase the depth k, the goal that only 1 does not know whether 2 knows the secret of 3 becomes unsolvable. Indeed, by the truth axiom T of epistemic logic, we have, for example:

K 1 K 4 K 2 s 3 → K 1 K 2 s 3 ,
and hence the latter cannot be false without the former being false. Therefore for k>2, the correct specification will be that every goal of the form:

K 1 K i 1 . . . K i m K 2 K j 1 . . . K j p s 3
is false, for m+p+2 ≤ k.

Conclusion

We have provided a logical analysis of the gossip problem, focusing on how higher-order shared knowledge can be obtained. We did so in a particular dynamic epistemic logic: Dynamic Epistemic Logic of Propositional Assignment and Observation DEL-PAO. Its integration of knowledge modalities and dynamic modalities provides a handy language in order to reason about concepts such as an agent being a semiexpert, which is pivotal in our algorithm. With DEL-PAO, we were able to prove both the correctness and optimality of our algorithm, generalizing the results from [START_REF] Baker | Gossips and telephones[END_REF][START_REF] Tijdeman | On a telephone problem[END_REF][START_REF] Hajnal | A cure for the telephone disease[END_REF] on the minimal number of calls.

The gossip problem recently attracted quite some attention in the dynamic epistemic logic community [START_REF] Attamah | A framework for epistemic gossip protocols[END_REF][START_REF] Attamah | Knowledge and gossip[END_REF][START_REF] Van Ditmarsch | Dynamic gossip[END_REF]. The version that we have studied here has a central scheduler telling each agent when to act and what to do. Other versions where the protocol is distributed were investigated recently [START_REF] Apt | Epistemic protocols for distributed gossiping[END_REF][START_REF] Ditmarsch | Parameters for epistemic gossip problems[END_REF]. We believe that our generalization-as well as further variations where e.g. calls can only be made according to some graph structure-provide interesting, canonical multiagent planning problems that can be compared to the blocksworld in classical planning. This is the subject of ongoing work; first steps are reported in [START_REF] Cooper | A simple account of multi-agent epistemic planning[END_REF][START_REF] Maffre | Ignorance is bliss: observability-based dynamic epistemic logics and their applications[END_REF]. We believe that our visibility-based approach is an interesting alternative to dynamic epistemic logic-based planning that was proposed in [START_REF] Bolander | Epistemic planning for single and multi-agent systems[END_REF]: indeed, it was shown that such planning problems are undecidable [START_REF] Aucher | Undecidability in epistemic planning[END_REF], and so even for simple instances [START_REF] Charrier | On the impact of modal depth in epistemic planning[END_REF].

2 Fig. 1 .

 21 Fig. 1. Graphical representation of the first three turns of Algorithm 1.

3 ]

 3 EK left,n-4 s left,0,...,n-4 ∧ EK right,n-3 s right,n-3 which is the same as: V 0 |= [turn 0 ] EK left,n-4 s left,0,...,n-4 ∧ EK right,n-3 s right,n-3 , hence the result.

5 ]

 5 EK left,n-5 EK left,n-3,0,1,...,n-5 s Agt .

4 ]

 4 EK left,n-5 EK left,n-3,0,1,...,n-5 s Agt ∧ EK right,n-4 EK right,n-4 s Agt , that is:

  s Agt expresses that all secrets are shared knowledge; -EK Agt EK Agt s Agt expresses that every agent knows that all secrets are shared knowledge; -EK Agt . . . EK Agt k times s Agt expresses that all secrets are shared knowledge up to depth k ≥ 1.

  and only if α belongs to every valuation in INTR. By Proposition 1, α is valid in INTR if and only if α is of the form either σ S i S i α with σ ∈ OBS * , or σ JS α with σ ∈ OBS + . 4.3.1. Indistinguishability relations between valuations Two valuations are related by the indistinguishability relation for agent i, noted ∼ i , if every α that i sees has the same value. Similarly, we have a relation ∼ Agt for joint indistinguishability. They are defined as follows:

  turn 0 ; turn 1 ; . . . ; turn k+2 ]

	EK 0,(k+2 (mod 2))+1 EK k Agt s Agt ,
	which implies:
	V 0 |= [turn 0 ; turn 1 ; . . . ; turn k+2 ]
	K 0 EK k Agt s Agt ,
	and hence by (Incr) of Proposition 2:
	since turn k+3 = Call 0 (k+3 (mod 2))+1 . Therefore, be-
	cause 0, (k+2 (mod 2)) + 1 and k+3 (mod 2)) + 1
	are all different, we obtain by formula (Prsv) of Propo-
	sition 2:
	V 0 |=[turn 0 ; turn 1 ; . . . ; turn k+2 ][turn k+3 ]
	EK Agt EK k Agt s Agt ,
	that is:
	V 0 |=[turn 0 ; turn 1 ; . . . ; turn k+2 ; turn k+3 ]
	EK k+1 Agt s Agt ,
	which is our goal for depth k+1.
	Proposition 6. The minimal number of calls needed to
	solve the instance Gossip(k, 3) of the generalized gos-
	sip problem, for k≥1, is at least k+2.

V 0 |= [turn 0 ; turn 1 ; . . . ; turn k+2 ][turn k+3 ] EK 0,(k+3 (mod 2))+1 EK k Agt s Agt .

Acknowledgements

We would like to thank the reviewers of AT'2015 for their comments which hopefully helped to improve the presentation of the paper. We also acknowledge several discussions about the gossip problem at the inspiring August 2015 Lorentz Center workshop "To be announced" in Leiden, in particular with Hans van Ditmarsch, Jan van Eijck, Malvin Gattinger, Louwe Kuijer, Christian Muise, Pere Pardo, Rahim Ramezanian and Francois Schwarzentruber. We are also grateful to Thomas Bolander, Davide Grossi, Emiliano Lorini, Frédéric Maris, Martin Cooper, and Pierre Regnier for many discussions about the gossip problem.