# A Lightweight Epistemic Logic and its Application to Planning

Martin Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, Elise

Perrotin, Pierre Régnier

► To cite this version:

Martin Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, Elise Perrotin, et al.. A Lightweight Epistemic Logic and its Application to Planning. Artificial Intelligence, 2021, Special issue: SI: Ethics for Autonomous Systems, 298, pp.103437. 10.1016/j.artint.2020.103437. hal-03147798

HAL Id: hal-03147798

https://hal.science/hal-03147798

Submitted on 15 Feb 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# A Lightweight Epistemic Logic and its Application to Planning

Martin Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, Elise

Perrotin, Pierre Régnier

► To cite this version:

Martin Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, Elise Perrotin, et al.. A Lightweight Epistemic Logic and its Application to Planning. Artificial Intelligence (AIJ), 2021, Special issue: Epistemic Planning, 298, pp.103437. 10.1016/j.artint.2020.103437. hal-03147798v2

HAL Id: hal-03147798

https://hal.science/hal-03147798v2

Submitted on 8 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Lightweight Epistemic Logic and its Application to Planning

Martin C. Cooperª, Andreas Herzigª, Faustine Maffreª, Frédéric Marisª, Elise Perrotinª, Pierre Régnierª

ªIRIT, CNRS, Univ. Paul Sabatier, 118 Route de Narbonne, F-31062 Toulouse Cedex 9, France

## Abstract

We study multiagent epistemic planning with a simple epistemic logic whose language is a restriction of that of standard epistemic logic. Its formulas are boolean combinations of observability atoms: sequences of 'knowing whether' operators followed by propositional variables. This compares favourably with other restricted languages where formulas are boolean combinations of epistemic literals: sequences of 'knowing that' epistemic operators and negations followed by propositional variables; or in other terms: epistemic formulas without conjunctions or disjunctions. The reason is that our language enables a richer theory of mind: we can express statements such as "I don't know whether *p*, but I know that you know whether *p*" which are important in communication and more generally in interaction and which cannot be expressed with epistemic literals. Going beyond previous work, we also introduce a 'common knowledge whether' operator. We show that satisfiability is nevertheless NP-complete. We then define simple epistemic planning tasks as generalisations of classical planning tasks: action descriptions have sets of observability atoms as add-and-delete-lists, initial states are sets of observability atoms, and goals are boolean combinations of observability atoms. We show that simple epistemic planning tasks can be polynomially translated into classical planning tasks. It follows that checking solvability of simple epistemic planning

<footnote>ªCorresponding author: Andreas Herzig, Andreas.Herzig@irit.fr</footnote>
# A Lightweight Epistemic Logic and its Application to Planning

Martin C. Cooperª, Andreas Herzigª, Faustine Maffreª, Frédéric Marisª, Elise Perrotinª, Pierre Régnierª

ªIRIT, CNRS, Univ. Paul Sabatier, 118 Route de Narbonne, F-31062 Toulouse Cedex 9, France

## Abstract

We study multiagent epistemic planning with a simple epistemic logic whose language is a restriction of that of standard epistemic logic. Its formulas are boolean combinations of observability atoms: sequences of 'knowing whether' operators followed by propositional variables. This compares favourably with other restricted languages where formulas are boolean combinations of epistemic literals: sequences of 'knowing that' epistemic operators and negations followed by propositional variables; or in other terms: epistemic formulas without conjunctions or disjunctions. The reason is that our language enables a richer theory of mind: we can express statements such as "I don't know whether *p*, but I know that you know whether *p*" which are important in communication and more generally in interaction and which cannot be expressed with epistemic literals. Going beyond previous work, we also introduce a 'common knowledge whether' operator. We show that satisfiability is nevertheless NP-complete. We then define simple epistemic planning tasks as generalisations of classical planning tasks: action descriptions have sets of observability atoms as add-and-delete-lists, initial states are sets of observability atoms, and goals are boolean combinations of observability atoms. We show that simple epistemic planning tasks can be polynomially translated into classical planning tasks. It follows that checking solvability of simple epistemic planning

<footnote>ªCorresponding author: Andreas Herzig, Andreas.Herzig@irit.fr</footnote>
tasks is PSPACE-complete. We present some application examples such as
the gossip problem and some experimental results and clarify the relation-
ship with Dynamic Epistemic Logic-based planning.

***Keywords:*** Epistemic planning; multiagent planning; epistemic logic; 
gossip problem

# 1. Introduction

Suppose there are *n* agents, each of which knows some secret: a piece of
information that is not known to the others. They communicate by phone
calls, and whenever one person calls another they tell each other all they
know at that time. How many calls are required before each item of gossip
is known to everyone? This is known as the gossip problem. It is of great
interest in the conception of communication networks and in parallel and
distributed computing, but there are other less obvious applications like the
management of data on storage devices [1], or the computation of the syn-
tenic distance between two genomes (minimum number of fusions, fissions,
and translocations required to transform one into the other) [2]. Several
variants have been studied in the literature, and a survey of these alterna-
tives and the associated results has been published [3]. The gossip problem
can be viewed as a multiagent epistemic planning task where the goal is
shared knowledge: everybody knows all secrets. It is a purely epistemic
planning task because it is only the agents’ knowledge that evolves, while
the facts of the world remain unchanged. There are numerous variations
of such a planning task; see e.g. [4] for an overview. The goal may in par-
ticular be to achieve higher-order shared knowledge: everybody knows that
everybody knows all secrets, and so on. We believe that generalised gos-
siping is a paradigmatic epistemic planning task, much in the same way
as the blocksworld is a paradigmatic classical planning task: (1) it is mul-
tiagent; (2) it is ‘truly epistemic’, in the sense that it involves higher-order
knowledge; (3) it is as simple as it could be, in the sense that there are no
tasks is PSPACE-complete. We present some application examples such as
the gossip problem and some experimental results and clarify the relation-
ship with Dynamic Epistemic Logic-based planning.

***Keywords:*** Epistemic planning; multiagent planning; epistemic logic; 
gossip problem

# 1. Introduction

Suppose there are *n* agents, each of which knows some secret: a piece of
information that is not known to the others. They communicate by phone
calls, and whenever one person calls another they tell each other all they
know at that time. How many calls are required before each item of gossip
is known to everyone? This is known as the gossip problem. It is of great
interest in the conception of communication networks and in parallel and
distributed computing, but there are other less obvious applications like the
management of data on storage devices [1], or the computation of the syn-
tenic distance between two genomes (minimum number of fusions, fissions,
and translocations required to transform one into the other) [2]. Several
variants have been studied in the literature, and a survey of these alterna-
tives and the associated results has been published [3]. The gossip problem
can be viewed as a multiagent epistemic planning task where the goal is
shared knowledge: everybody knows all secrets. It is a purely epistemic
planning task because it is only the agents’ knowledge that evolves, while
the facts of the world remain unchanged. There are numerous variations
of such a planning task; see e.g. [4] for an overview. The goal may in par-
ticular be to achieve higher-order shared knowledge: everybody knows that
everybody knows all secrets, and so on. We believe that generalised gos-
siping is a paradigmatic epistemic planning task, much in the same way
as the blocksworld is a paradigmatic classical planning task: (1) it is mul-
tiagent; (2) it is ‘truly epistemic’, in the sense that it involves higher-order
knowledge; (3) it is as simple as it could be, in the sense that there are no
ontic actions; (4) it has many variations.

30

35

40

45

50

55

The aim of the present paper is to introduce a simple logical approach within which we can account for centralised epistemic planning tasks such as the above. We could have chosen Dynamic Epistemic Logic (DEL) for this purpose, as done by [5]: its event models allow us to model telephone calls as private announcements. However, we take inspiration from a simpler framework: the Dynamic Epistemic Logic of Propositional Assignment and Observation (DEL-PAO), introduced in [6] and further developed in [7, 8, 9]. It is based on observability atoms, that are recursively defined as either propositional variables or atomic pieces of information about whether or not an agent sees the truth value of an observability atom. DEL-PAO was applied to epistemic planning in [10]. We here simplify this account by disregarding the dynamic aspects and concentrating on the epistemic logic underlying DEL-PAO. That logic is consequently called the Epistemic Logic of Observation, abbreviated as EL-O. The present paper improves over [10] by simplifying the semantics (models are no longer infinite), by integrating a form of common knowledge into planning, and by a complexity analysis: satisfiability is NP-complete. Our EL-O-based definition of simple epistemic planning tasks parallels that of classical planning tasks, with actions, initial state, and goal described by means of observability atoms. This allows us to polynomially translate the former into the latter. It follows that deciding the solvability of a simple epistemic planning task is PSPACE-complete (just as DEL-PAO satisfiability, validity and model checking are).

The paper is organised as follows. In Section 2 we provide a detailed motivation of our approach and briefly overview related work. In Section 3 we introduce EL-O and in Section 4 we establish that it is a fragment of the standard epistemic logic S5 with an NP-complete satisfiability problem. In Section 5 we give a formal definition of action descriptions and simple epistemic planning tasks within our framework and polynomially translate them into classical planning tasks, from which PSPACE membership of deciding plan existence follows. In Section 6 we apply our framework
ontic actions; (4) it has many variations.

30

35

40

45

50

55

The aim of the present paper is to introduce a simple logical approach within which we can account for centralised epistemic planning tasks such as the above. We could have chosen Dynamic Epistemic Logic (DEL) for this purpose, as done by [5]: its event models allow us to model telephone calls as private announcements. However, we take inspiration from a simpler framework: the Dynamic Epistemic Logic of Propositional Assignment and Observation (DEL-PAO), introduced in [6] and further developed in [7, 8, 9]. It is based on observability atoms, that are recursively defined as either propositional variables or atomic pieces of information about whether or not an agent sees the truth value of an observability atom. DEL-PAO was applied to epistemic planning in [10]. We here simplify this account by disregarding the dynamic aspects and concentrating on the epistemic logic underlying DEL-PAO. That logic is consequently called the Epistemic Logic of Observation, abbreviated as EL-O. The present paper improves over [10] by simplifying the semantics (models are no longer infinite), by integrating a form of common knowledge into planning, and by a complexity analysis: satisfiability is NP-complete. Our EL-O-based definition of simple epistemic planning tasks parallels that of classical planning tasks, with actions, initial state, and goal described by means of observability atoms. This allows us to polynomially translate the former into the latter. It follows that deciding the solvability of a simple epistemic planning task is PSPACE-complete (just as DEL-PAO satisfiability, validity and model checking are).

The paper is organised as follows. In Section 2 we provide a detailed motivation of our approach and briefly overview related work. In Section 3 we introduce EL-O and in Section 4 we establish that it is a fragment of the standard epistemic logic S5 with an NP-complete satisfiability problem. In Section 5 we give a formal definition of action descriptions and simple epistemic planning tasks within our framework and polynomially translate them into classical planning tasks, from which PSPACE membership of deciding plan existence follows. In Section 6 we apply our framework
to examples, in particular the gossip problem, and in Section 7 we report
on some experiments that were done via an encoding of simple epistemic
planning tasks into PDDL. Section 8 discusses related work, where we ar-
gue in particular that our action descriptions are a more appropriate way
to describe the behaviour of actions than with DEL event models. Section 9
concludes.

## 2. Background and motivation

Reasoning in epistemic logic as introduced by Hintikka [11] and popu-
larised in AI by Halpern and colleagues [12] is strictly more complex than
in classical logic: the satisfiability problem is at least in PSPACE, and is
EXPTIME-complete if common knowledge is involved [13]. The complexity
gap widens for planning tasks: while the solvability problem is PSPACE-
complete for classical planning [14], it is undecidable for planning with
DEL-based event models [15]. The latter provide rather expressive mod-
els for the agents' perception of actions. They parallel the standard epis-
temic logic modelling of uncertainty by indistinguishability relations be-
tween possible states: uncertainty in the perception of actions is modelled
by indistinguishability relations between possible events. As explored by
several authors in a series of papers, undecidability of DEL planning is
already the case under very weak hypotheses about these event models
[16, 17, 18, 19]. Basically, DEL planning tasks are only decidable when the
event model is a singleton, i.e., when all actions are public. However, ac-
tions in the gossip problem are not public, nor are they in many real world
applications.

We propose to base epistemic planning on an epistemic logic that is sim-
pler than Hintikka's: epistemic information is restricted to the atomic for-
mulas of the language. We are not the first to do this: several previous
approaches have proposed languages where the scope of the epistemic oper-
ator $K_i$ is restricted to literals, or literals that are preceded by a sequence of
to examples, in particular the gossip problem, and in Section 7 we report
on some experiments that were done via an encoding of simple epistemic
planning tasks into PDDL. Section 8 discusses related work, where we ar-
gue in particular that our action descriptions are a more appropriate way
to describe the behaviour of actions than with DEL event models. Section 9
concludes.

## 2. Background and motivation

Reasoning in epistemic logic as introduced by Hintikka [11] and popu-
larised in AI by Halpern and colleagues [12] is strictly more complex than
in classical logic: the satisfiability problem is at least in PSPACE, and is
EXPTIME-complete if common knowledge is involved [13]. The complexity
gap widens for planning tasks: while the solvability problem is PSPACE-
complete for classical planning [14], it is undecidable for planning with
DEL-based event models [15]. The latter provide rather expressive mod-
els for the agents' perception of actions. They parallel the standard epis-
temic logic modelling of uncertainty by indistinguishability relations be-
tween possible states: uncertainty in the perception of actions is modelled
by indistinguishability relations between possible events. As explored by
several authors in a series of papers, undecidability of DEL planning is
already the case under very weak hypotheses about these event models
[16, 17, 18, 19]. Basically, DEL planning tasks are only decidable when the
event model is a singleton, i.e., when all actions are public. However, ac-
tions in the gossip problem are not public, nor are they in many real world
applications.

We propose to base epistemic planning on an epistemic logic that is sim-
pler than Hintikka's: epistemic information is restricted to the atomic for-
mulas of the language. We are not the first to do this: several previous
approaches have proposed languages where the scope of the epistemic oper-
ator $K_i$ is restricted to literals, or literals that are preceded by a sequence of
85

epistemic operators [20, 21, 22, 23], possibly with negations [24, 25]. Such restrictions however exclude formulas such as $K_i(K_jp \lor K_j\neg p)$ expressing that agent $i$ knows that agent $j$ knows whether the propositional variable $p$ is true. This is a major drawback because such formulas are fundamental in communication and more generally in any form of interaction: a situation where agent $i$ does not know whether $p$ is the case or not $(\neg K_i p \land \neg K_j \neg p)$ but knows that $j$ knows $(K_i(K_jp \lor K_j\neg p))$ may lead agent $i$ to ask $j$ about $p$.

90

We here make a similar restriction, but move from the primitive 'knowing-that' operator $K_i$ to the less standard 'knowing-whether' or 'knowing-if' operator $Kif_i$. In the unrestricted language these two operators are interdefinable: we have $Kif_i\varphi \leftrightarrow K_i\varphi \lor K_i\neg\varphi$ and $K_i\varphi \leftrightarrow \varphi \land Kif_i\varphi$, for arbitrary formulas $\varphi$ [26]. However, the situation changes when we restrict the language to sequences of 'knowing-whether' operators followed by propositional variables. On the one hand, any sequence of 'knowing-that' operators followed by a literal can be expressed by a sequence of 'knowing-whether' operators:

95

100

* $K_i p$ is equivalent to $p \land Kif_i p$;

* $K_i\neg p$ is equivalent to $\neg p \land Kif_i p$;

* $K_i K_j p$ is equivalent to $p \land Kif_i p \land Kif_j p \land Kif_i Kif_j p$;

* and so on.

105

On the other hand and as we will prove in Section 8.2, from $n \ge 2$ on sequences $Kif_{i_1} \dots Kif_{i_n} p$ of 'knowing-whether' operators followed by propositional variables cannot be expressed by means of boolean combinations of 'knowing-that' operators followed by literals. In particular, no such boolean combination is equivalent to $Kif_i Kif_j p$. Such increased expressivity makes a difference. For example, consider the above situation where $i$ does not know whether $p$ but knows whom to ask, as expressed by the formula $\neg K_i p \land \neg K_j \neg p \land K_i(K_jp \lor K_j\neg p)$; this can be expressed in our language by $\neg Kif_i p \land Kif_j p \land Kif_i Kif_j p$.

110
85

epistemic operators [20, 21, 22, 23], possibly with negations [24, 25]. Such restrictions however exclude formulas such as $K_i(K_jp \lor K_j\neg p)$ expressing that agent $i$ knows that agent $j$ knows whether the propositional variable $p$ is true. This is a major drawback because such formulas are fundamental in communication and more generally in any form of interaction: a situation where agent $i$ does not know whether $p$ is the case or not $(\neg K_i p \land \neg K_j \neg p)$ but knows that $j$ knows $(K_i(K_jp \lor K_j\neg p))$ may lead agent $i$ to ask $j$ about $p$.

90

We here make a similar restriction, but move from the primitive 'knowing-that' operator $K_i$ to the less standard 'knowing-whether' or 'knowing-if' operator $Kif_i$. In the unrestricted language these two operators are interdefinable: we have $Kif_i\varphi \leftrightarrow K_i\varphi \lor K_i\neg\varphi$ and $K_i\varphi \leftrightarrow \varphi \land Kif_i\varphi$, for arbitrary formulas $\varphi$ [26]. However, the situation changes when we restrict the language to sequences of 'knowing-whether' operators followed by propositional variables. On the one hand, any sequence of 'knowing-that' operators followed by a literal can be expressed by a sequence of 'knowing-whether' operators:

95

100

* $K_i p$ is equivalent to $p \land Kif_i p$;

* $K_i\neg p$ is equivalent to $\neg p \land Kif_i p$;

* $K_i K_j p$ is equivalent to $p \land Kif_i p \land Kif_j p \land Kif_i Kif_j p$;

* and so on.

105

On the other hand and as we will prove in Section 8.2, from $n \ge 2$ on sequences $Kif_{i_1} \dots Kif_{i_n} p$ of 'knowing-whether' operators followed by propositional variables cannot be expressed by means of boolean combinations of 'knowing-that' operators followed by literals. In particular, no such boolean combination is equivalent to $Kif_i Kif_j p$. Such increased expressivity makes a difference. For example, consider the above situation where $i$ does not know whether $p$ but knows whom to ask, as expressed by the formula $\neg K_i p \land \neg K_j \neg p \land K_i(K_jp \lor K_j\neg p)$; this can be expressed in our language by $\neg Kif_i p \land Kif_j p \land Kif_i Kif_j p$.

110
Instead of Kif<sub>i</sub> we prefer to write S<sub>i</sub>, and we read S<sub>i</sub> p as "agent i sees whether p is true or not". This highlights that when we define K<sub>i</sub> p as p ∧ S<sub>i</sub> p, we consider that i's knowledge comes from what i sees. More generally, an observability atom takes the form S<sub>i<sub>1</sub></sub> ... S<sub>i<sub>n</sub></sub> p of a sequence of observability operators prefixing a propositional variable. Then propositional variables are the special case where n = 0. We are going to consider that every such observability atom is an atomic formula and that complex formulas are boolean combinations of such atomic formulas. Technically S<sub>i</sub> is therefore not a modal operator, as opposed to Kif<sub>i</sub>, and our move in notation also aims at stressing that. This comes with a move away from Kripke models with accessibility relations: a model is simply a valuation over the set of observability atoms, alias a state. We identify such valuations with sets of observability atoms. The only delicate point is that the interpretation of formulas has to be arranged such that introspection is guaranteed.

A semantic counterpart of observability atoms S<sub>i</sub> p of depth 1 were introduced in the model checking literature in order to represent epistemic models in a compact way [27, 28, 29]. As argued there, such compact models are more attractive than Kripke models when it comes to model checking. It is shown in [29] how any Kripke model can be captured by means of observability information, possibly by adding new propositional variables. Our observability atoms S<sub>i</sub> p capture their semantic concept in the syntax.

Simplifications of epistemic logic typically lack a modal operator of common knowledge. (It is however present in [29].) We here consider an operator JS, reading JS p as "all agents jointly see the value of p", or "all agents jointly see whether p is true or not". Metaphorically, joint attention about a propositional variable p can be understood as eye contact between the agents when observing p. JS is a powerful operator that allows us to model common knowledge obtained through co-presence. One may think of JS p as implying the infinite set of propositions of the form S<sub>i<sub>1</sub></sub> ... S<sub>i<sub>n</sub></sub> p for all i<sub>1</sub>,..., i<sub>n</sub> and all n ≥ 1. Suppose p stands for 'the door is open'. We can imagine that JS p is true when all agents are present in the same room and not only
Instead of Kif<sub>i</sub> we prefer to write S<sub>i</sub>, and we read S<sub>i</sub> p as "agent i sees whether p is true or not". This highlights that when we define K<sub>i</sub> p as p ∧ S<sub>i</sub> p, we consider that i's knowledge comes from what i sees. More generally, an observability atom takes the form S<sub>i<sub>1</sub></sub> ... S<sub>i<sub>n</sub></sub> p of a sequence of observability operators prefixing a propositional variable. Then propositional variables are the special case where n = 0. We are going to consider that every such observability atom is an atomic formula and that complex formulas are boolean combinations of such atomic formulas. Technically S<sub>i</sub> is therefore not a modal operator, as opposed to Kif<sub>i</sub>, and our move in notation also aims at stressing that. This comes with a move away from Kripke models with accessibility relations: a model is simply a valuation over the set of observability atoms, alias a state. We identify such valuations with sets of observability atoms. The only delicate point is that the interpretation of formulas has to be arranged such that introspection is guaranteed.

A semantic counterpart of observability atoms S<sub>i</sub> p of depth 1 were introduced in the model checking literature in order to represent epistemic models in a compact way [27, 28, 29]. As argued there, such compact models are more attractive than Kripke models when it comes to model checking. It is shown in [29] how any Kripke model can be captured by means of observability information, possibly by adding new propositional variables. Our observability atoms S<sub>i</sub> p capture their semantic concept in the syntax.

Simplifications of epistemic logic typically lack a modal operator of common knowledge. (It is however present in [29].) We here consider an operator JS, reading JS p as "all agents jointly see the value of p", or "all agents jointly see whether p is true or not". Metaphorically, joint attention about a propositional variable p can be understood as eye contact between the agents when observing p. JS is a powerful operator that allows us to model common knowledge obtained through co-presence. One may think of JS p as implying the infinite set of propositions of the form S<sub>i<sub>1</sub></sub> ... S<sub>i<sub>n</sub></sub> p for all i<sub>1</sub>,..., i<sub>n</sub> and all n ≥ 1. Suppose p stands for 'the door is open'. We can imagine that JS p is true when all agents are present in the same room and not only
observe the door, but also mutually observe each other. In this concrete
example, if an agent leaves the room and closes the door behind her, *JS p*
becomes false because the agents no longer mutually observe each other
(even if the agent who has left can see the closed door from the outside).
In order to guarantee that joint observability of *p* implies individual ob-
servability of *p*, we require in our semantics that states containing *JS p* also
contain every *S*<sub>*i*</sub>*p*, and more generally every *p* preceded by any sequence of
*S*<sub>*i*</sub> and *JS*. Defining *CKp* as *p* ∧ *JS p*, we obtain a common knowledge oper-
ator that satisfies all the standard properties except the induction axiom
*CK(p → ∧<sub>*i*∈*A*</sub> *K*<sub>*i*</sub>*p*) → (*p* → *CKp*). We will discuss this issue in Section 4
(Remark 4).

It is generally assumed in the AI literature that a reasonable epistemic
logic should satisfy introspection: the formulas $K_i\varphi \rightarrow K_i K_i\varphi$ and $\neg K_i\varphi \rightarrow K_i\neg K_i\varphi$ should both be valid.<fnref n="1" /> In terms of observability this means that
states should contain $S_i S_i p$ for every agent $i$ and propositional variable $p$,
and more generally every $S_i S_i S_j p$, $S_j S_i S_i p$, etc. Similarly, they should also
contain *JS p*. Moreover, whenever a state contains some *JS p* then it should
also contain $S_i p$, for every agent $i$. Clearly, these closure conditions make
states infinite. We are going to avoid this by integrating closure into the
truth condition for observability atoms.

All we have said up to now was about how to describe the agents’ static
knowledge. We complete the picture by adding actions that may modify
both the state of the world and the agents’ vision: we simply add and
delete atoms. This requires some care: we have to guarantee that the
above properties of introspection and ‘joint sight implies individual sight’
are preserved. We do so by requiring action descriptions to be consistent:
they cannot delete introspective atoms such as $S_i S_i p$, they cannot add *JS* *p*

<footnote n="1">¹We are aware that negative introspection was criticised in the literature as being too strong [30, 31]. One may however argue with Holliday [32, footnote 4] that these criticisms do not apply to observability-based knowledge.</footnote>
observe the door, but also mutually observe each other. In this concrete
example, if an agent leaves the room and closes the door behind her, *JS p*
becomes false because the agents no longer mutually observe each other
(even if the agent who has left can see the closed door from the outside).
In order to guarantee that joint observability of *p* implies individual ob-
servability of *p*, we require in our semantics that states containing *JS p* also
contain every *S*<sub>*i*</sub>*p*, and more generally every *p* preceded by any sequence of
*S*<sub>*i*</sub> and *JS*. Defining *CKp* as *p* ∧ *JS p*, we obtain a common knowledge oper-
ator that satisfies all the standard properties except the induction axiom
*CK(p → (∧<sub>*i*∈A<sub>Δ</sub></sub> *K*<sub>*i*</sub>*p*) → (*p* → *CKp*)*. We will discuss this issue in Section 4
(Remark 4).

It is generally assumed in the AI literature that a reasonable epistemic
logic should satisfy introspection: the formulas $K_i\varphi \rightarrow K_i K_i\varphi$ and $\neg K_i\varphi \rightarrow K_i\neg K_i\varphi$ should both be valid.<fnref n="1" /> In terms of observability this means that
states should contain $S_i S_i p$ for every agent $i$ and propositional variable $p$,
and more generally every $S_i S_i S_j p$, $S_j S_i S_i p$, etc. Similarly, they should also
contain *JS p*. Moreover, whenever a state contains some *JS p* then it should
also contain $S_i p$, for every agent $i$. Clearly, these closure conditions make
states infinite. We are going to avoid this by integrating closure into the
truth condition for observability atoms.

All we have said up to now was about how to describe the agents’ static
knowledge. We complete the picture by adding actions that may modify
both the state of the world and the agents’ vision: we simply add and
delete atoms. This requires some care: we have to guarantee that the
above properties of introspection and ‘joint sight implies individual sight’
are preserved. We do so by requiring action descriptions to be consistent:
they cannot delete introspective atoms such as $S_i S_i p$, they cannot add *JS* *p*

<footnote n="1">¹We are aware that negative introspection was criticised in the literature as being too strong [30, 31]. One may however argue with Holliday [32, footnote 4] that these criticisms do not apply to observability-based knowledge.</footnote>
and delete $S_i p$ at the same time, etc. A further issue that arises when describing epistemic actions is that the description of effects should cater for conditional effects: whether or not an action changes the knowledge of some agent $i$ depends on what $i$ observes when the action is performed. For example, when agent $i$ switches the light on then the effect of that action on agent $j$'s knowledge depends on whether the latter is in the room or not. Another example is a call between two agents in the gossip problem where the agents share all the secrets they know: what is learned is conditional on the agents' prior knowledge. Based on such action descriptions, a simple epistemic planning task is going to be made up of:

175

180

* a vocabulary;

* a set of consistent descriptions of actions with conditional effects which add and delete observability atoms;

* an initial state which is an EL-O valuation;

* a goal formula which is an EL-O formula.

185

Classical planning tasks are particular cases of simple epistemic planning tasks; therefore the existence of a solution to a simple epistemic planning task is PSPACE-hard. It is actually PSPACE-complete: as we will show in Section 5.5, simple epistemic planning tasks can be polynomially reduced to classical planning tasks.

190

### 3. EL-O: Epistemic Logic of Observation

We introduce the Epistemic Logic of Observation, abbreviated to EL-O. Its language consists of formulas over a vocabulary of observability atoms: propositional variables prefixed by sequences of observability operators $S_i$ and $\mathcal{J}S$. Models of EL-O are sets of such observability atoms. The interpretation of formulas is defined in a way such that introspection principles become valid. We show that the EL-O satisfiability problem is NP-complete.

195
and delete $S_i p$ at the same time, etc. A further issue that arises when describing epistemic actions is that the description of effects should cater for conditional effects: whether or not an action changes the knowledge of some agent $i$ depends on what $i$ observes when the action is performed. For example, when agent $i$ switches the light on then the effect of that action on agent $j$'s knowledge depends on whether the latter is in the room or not. Another example is a call between two agents in the gossip problem where the agents share all the secrets they know: what is learned is conditional on the agents' prior knowledge. Based on such action descriptions, a simple epistemic planning task is going to be made up of:

175

180

* a vocabulary;

* a set of consistent descriptions of actions with conditional effects which add and delete observability atoms;

* an initial state which is an EL-O valuation;

* a goal formula which is an EL-O formula.

185

Classical planning tasks are particular cases of simple epistemic planning tasks; therefore the existence of a solution to a simple epistemic planning task is PSPACE-hard. It is actually PSPACE-complete: as we will show in Section 5.5, simple epistemic planning tasks can be polynomially reduced to classical planning tasks.

190

### 3. EL-O: Epistemic Logic of Observation

We introduce the Epistemic Logic of Observation, abbreviated to EL-O. Its language consists of formulas over a vocabulary of observability atoms: propositional variables prefixed by sequences of observability operators $S_i$ and $J_S$. Models of EL-O are sets of such observability atoms. The interpretation of formulas is defined in a way such that introspection principles become valid. We show that the EL-O satisfiability problem is NP-complete.

195
### 3.1. Boolean languages and Classical Propositional Calculus CPC

The language $\mathcal{L}_{bool}(\mathbb{V})$ of boolean formulas over some vocabulary $\mathbb{V}$ combines the elements of $\mathbb{V}$ by means of the boolean operators. It is defined by the grammar

$$ \mathcal{L}_{bool}(\mathbb{V}) : \varphi ::= p \mid \neg\varphi \mid (\varphi \land \varphi) $$

where $p$ ranges over $\mathbb{V}$. The boolean operators $\top$, $\bot$, $\vee$, $\rightarrow$, and $\leftrightarrow$ are defined in the standard way. The vocabulary of $\varphi$ is defined inductively by: $\mathrm{Voc}(p) = \{p\}$, for $p \in \mathbb{V}$; $\mathrm{Voc}(\neg\varphi) = \mathrm{Voc}(\varphi)$; $\mathrm{Voc}(\varphi \land \varphi') = \mathrm{Voc}(\varphi) \cup \mathrm{Voc}(\varphi')$.

The vocabulary $\mathbb{V}$ is usually supposed to be a countable set of propositional variables $\mathbb{P}$ that are not analysed further. However, in our lightweight epistemic logic $\mathbb{V}$ has some structure: its observability atoms involve propositional variables and agents. Related to that, instead of defining the length of an atomic formula to be 1 we suppose in this paper that each $p \in \mathbb{P}$ has some length $\ell(p) \ge 1$. The length of complex formulas is then defined inductively from the length of atomic formulas by: $\ell(\neg\varphi) = \ell(\varphi) + 1$ and $\ell(\varphi \land \varphi') = \ell(\varphi) + \ell(\varphi') + 1$. For example, if $\ell(p) = 1$ then $\ell(\top) = 5$ because $\top$ abbreviates $\neg(p \land \neg p)$.

A state is a subset of the vocabulary $\mathbb{V}$. We denote states by $s$, $s'$, etc. In *Classical Propositional Calculus* CPC the formulas of $\mathcal{L}_{bool}(\mathbb{V})$ are interpreted in the set of all states $2^{\mathbb{V}}$ according to the following truth conditions: $s \models p$ iff $p \in s$, for every $p \in \mathbb{V}$; $s \models \neg\varphi$ iff $s \not\models \varphi$; and $s \models \varphi \land \varphi'$ iff $s \models \varphi$ and $s \models \varphi'$. A formula $\varphi$ is *CPC satisfiable* iff $s \models \varphi$ for every $s \in 2^{\mathbb{V}}$, and it is *CPC valid* iff $s \models \varphi$ for some $s \in 2^{\mathbb{V}}$. It is known that CPC-satisfiability of a formula is NP-complete and that CPC-validity of a formula is coNP-complete.

### 3.2. Observability atoms and introspection

We now define the vocabulary we will be using in our epistemic logic. Let $\mathbb{P}$ be a countable set of propositional variables and let $\mathbb{A}$ be a finite set of agents. The set of observability operators is $\mathrm{OBS} = \{S_i : i \in \mathbb{A}\} \cup \{\mathcal{J}\mathcal{S}\}$, where $S_i$ stands for individual observability of agent $i$ and $\mathcal{J}\mathcal{S}$ stands for
### 3.1. Boolean languages and Classical Propositional Calculus CPC

The language $\mathcal{L}_{bool}(\mathbb{V})$ of boolean formulas over some vocabulary $\mathbb{V}$ combines the elements of $\mathbb{V}$ by means of the boolean operators. It is defined by the grammar

$$ \mathcal{L}_{bool}(\mathbb{V}) : \varphi ::= p \mid \neg\varphi \mid (\varphi \land \varphi) $$

where $p$ ranges over $\mathbb{V}$. The boolean operators $\top$, $\bot$, $\vee$, $\rightarrow$, and $\leftrightarrow$ are defined in the standard way. The vocabulary of $\varphi$ is defined inductively by: $\mathrm{Voc}(p) = \{p\}$, for $p \in \mathbb{V}$; $\mathrm{Voc}(\neg\varphi) = \mathrm{Voc}(\varphi)$; $\mathrm{Voc}(\varphi \land \varphi') = \mathrm{Voc}(\varphi) \cup \mathrm{Voc}(\varphi')$.

The vocabulary $\mathbb{V}$ is usually supposed to be a countable set of propositional variables $\mathbb{P}$ that are not analysed further. However, in our lightweight epistemic logic $\mathbb{V}$ has some structure: its observability atoms involve propositional variables and agents. Related to that, instead of defining the length of an atomic formula to be 1 we suppose in this paper that each $p \in \mathbb{P}$ has some length $\ell(p) \ge 1$. The length of complex formulas is then defined inductively from the length of atomic formulas by: $\ell(\neg\varphi) = \ell(\varphi) + 1$ and $\ell(\varphi \land \varphi') = \ell(\varphi) + \ell(\varphi') + 1$. For example, if $\ell(p) = 1$ then $\ell(\top) = 5$ because $\top$ abbreviates $\neg(p \land \neg p)$.

A state is a subset of the vocabulary $\mathbb{V}$. We denote states by $s$, $s'$, etc. In *Classical Propositional Calculus* CPC the formulas of $\mathcal{L}_{bool}(\mathbb{V})$ are interpreted in the set of all states $2^{\mathbb{V}}$ according to the following truth conditions: $s \models p$ iff $p \in s$, for every $p \in \mathbb{V}$; $s \models \neg\varphi$ iff $s \not\models \varphi$; and $s \models \varphi \land \varphi'$ iff $s \models \varphi$ and $s \models \varphi'$. A formula $\varphi$ is *CPC satisfiable* iff $s \models \varphi$ for every $s \in 2^{\mathbb{V}}$, and it is *CPC valid* iff $s \models \varphi$ for some $s \in 2^{\mathbb{V}}$. It is known that CPC-satisfiability of a formula is NP-complete and that CPC-validity of a formula is coNP-complete.

### 3.2. Observability atoms and introspection

We now define the vocabulary we will be using in our epistemic logic. Let $\mathbb{P}$ be a countable set of propositional variables and let $\mathbb{A}$ be a finite set of agents. The set of *observability operators* is $\mathrm{OBS} = \{S_i : i \in \mathbb{A}\} \cup \{\mathcal{JS}\}$, where $S_i$ stands for individual observability of agent $i$ and $\mathcal{JS}$ stands for
joint observability of all agents. The set of all sequences of observability operators is noted OBS\* and the set of all non-empty sequences is noted OBS\+. We use $\sigma$, $\sigma'$, etc. to denote elements of OBS\* and reserve **nil** for the empty sequence. The length of a sequence of observability operators is defined inductively by: $\ell(\mathbf{nil}) = 0$; $\ell(S_i \sigma) = \ell(\sigma) + 1$; and $\ell(JS \sigma) = \ell(\sigma) + 1$.

*Observability atoms*, or atoms for short, are finite sequences of observability operators followed by a propositional variable. The set

$$ OA = \{\sigma p : \sigma \in \text{OBS}^*, p \in \mathbb{P}\}. $$

is the set of all atoms. (It depends on the set of propositional variables $\mathbb{P}$ and on the set of agents $A$; we however leave these arguments implicit.) We use the small Greek letters $\alpha, \alpha', \beta, \dots$ to denote atoms. Here are some examples: $S_1 p$ reads “1 sees the value of $p$”. Hence 1 knows whether $p$ is true or false. $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$: agent 2 may or may not see the value of $q$, and in both cases this is jointly observed. $S_1 S_2 S_3 p$ reads “1 sees whether 2 sees whether 3 sees $p$”. The length of an observability atom is $\ell(\sigma p) = \ell(\sigma) + 1$. Therefore an atom of length 1 is nothing but a propositional variable. For example, $\ell(JS S_2 p) = 3$. As $\vdash$ abbreviates $\neg(p \lor \neg p)$, it is of length $\ell(\vdash) = 2 \times \ell(p) + 3$.

**Example 1.** In the initial states $s_0^{G_1}$ of the gossip problem (in which secrets may or may not be true) each agent only knows her own secret. Therefore $s_0^{G_1} = \{S_i s_i : i \in A\} \cup S$ where $S$ is some subset of $\{s_i : i \in A\}$.

As explained in the introduction, individual introspection is expressed with our ‘knowing-whether’ operator as $S_i S_i \alpha$. Joint introspection is expressed by $JSJS\alpha$. The latter implies $\sigma JS\alpha$ for every non-empty $\sigma$ because joint observability implies any nesting of individual observability. We therefore call an atom *interspective* if it contains two consecutive $S_i$, or a $JS$ that is preceded by a non-empty sequence of observability operators. In other words, an atom is introspective if it is of the form $\sigma S_i S_i \alpha$ for some $\sigma \in \text{OBS}^*$,
joint observability of all agents. The set of all sequences of observability operators is noted OBS\* and the set of all non-empty sequences is noted OBS\+. We use $\sigma$, $\sigma'$, etc. to denote elements of OBS\* and reserve **nil** for the empty sequence. The length of a sequence of observability operators is defined inductively by: $\ell(\mathbf{nil}) = 0$; $\ell(S_i \sigma) = \ell(\sigma) + 1$; and $\ell(JS \sigma) = \ell(\sigma) + 1$.

*Observability atoms*, or atoms for short, are finite sequences of observability operators followed by a propositional variable. The set

$$ OA = \{\sigma p : \sigma \in \text{OBS}^*, p \in \mathbb{P}\}. $$

is the set of all atoms. (It depends on the set of propositional variables $\mathbb{P}$ and on the set of agents $A$; we however leave these arguments implicit.) We use the small Greek letters $\alpha, \alpha', \beta, \dots$ to denote atoms. Here are some examples: $S_1 p$ reads “1 sees the value of $p$”. Hence 1 knows whether $p$ is true or false. $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$: agent 2 may or may not see the value of $q$, and in both cases this is jointly observed. $S_1 S_2 S_3 p$ reads “1 sees whether 2 sees whether 3 sees $p$”. The length of an observability atom is $\ell(\sigma p) = \ell(\sigma) + 1$. Therefore an atom of length 1 is nothing but a propositional variable. For example, $\ell(JS S_2 p) = 3$. As $\top$ abbreviates $\neg(p \lor \neg p)$, it is of length $\ell(\top) = 2 \times \ell(p) + 3$.

**Example 1.** In the initial states $s_0^{G_1}$ of the gossip problem (in which secrets may or may not be true) each agent only knows her own secret. Therefore $s_0^{G_1} = \{S_i s_i : i \in A\} \cup S$ where $S$ is some subset of $\{s_i : i \in A\}$.

As explained in the introduction, individual introspection is expressed with our ‘knowing-whether’ operator as $S_i S_i \alpha$. Joint introspection is expressed by $JSJS\alpha$. The latter implies $\sigma JS\alpha$ for every non-empty $\sigma$ because joint observability implies any nesting of individual observability. We therefore call an atom *interspective* if it contains two consecutive $S_i$, or a $JS$ that is preceded by a non-empty sequence of observability operators. In other words, an atom is introspective if it is of the form $\sigma S_i S_i \alpha$ for some $\sigma \in \text{OBS}^*$,
or of the form $\sigma \mathcal{J}S\alpha$ for some $\sigma \in \text{OBS}^+$. The set of all introspective atoms is
$\mathbf{l-OA} = \{\sigma S_i S_i \alpha : \sigma \in \text{OBS}^+ \text{ and } \alpha \in \text{OA}\} \cup \{\sigma \mathcal{J}S\alpha : \sigma \in \text{OBS}^+ \text{ and } \alpha \in \text{OA}\}$.

The set l-OA is infinite and is a proper subset of OA.

### 3.3. Atomic consequence and introspectively closed states

We define a relation of *atomic consequence* between observability atoms
as follows:

$\alpha \Rightarrow \beta \text{ iff } \alpha = \beta, \text{ or } \alpha = \mathcal{J}\mathcal{S}\alpha' \text{ and } \beta = \sigma\alpha' \text{ for some } \sigma \in \text{OBS}^+.$

If this is the case then we say that $\alpha$ is a *cause* of $\beta$ and that $\beta$ is a *consequence* of $\alpha$. For example, $\mathcal{J}S p \Rightarrow S_i p$ and $\mathcal{J}S p \Rightarrow \mathcal{J}S S_i p$. The relation $\Rightarrow$ is clearly reflexive and transitive. Moreover, the set of introspective atoms is closed under atomic consequence: if $\alpha \in \text{l-OA}$ and $\alpha \Rightarrow \beta$ then $\beta \in \text{l-OA}$.

255

We let $\alpha \Rightarrow$ denote the set of consequences of $\alpha$ and $\alpha \Leftarrow$ the set of its causes:

$\alpha \Rightarrow = \{\beta : \alpha \Rightarrow \beta\}, \quad \alpha \Leftarrow = \{\beta : \beta \Rightarrow \alpha\}.$

Here are some examples:

$$
\begin{align*}
(p) \Rightarrow &= \{p\}, & (p) \Leftarrow &= \{p\}, \\
(S_i p) \Rightarrow &= \{S_i p\}, & (S_i p) \Leftarrow &= \{S_i p, \mathcal{J}S p\}, \\
(\mathcal{J}S p) \Rightarrow &= \{\sigma p : \sigma \in \text{OBS}^+\}, & (\mathcal{J}S p) \Leftarrow &= \{\mathcal{J}S p\}, \\
(S_i S_j p) \Rightarrow &= \{S_i S_j p\}, & (S_i S_j p) \Leftarrow &= \{S_i S_j p, \mathcal{J}S S_j p, \mathcal{J}S p\}.
\end{align*}
$$

260

Observe that $\alpha \Leftarrow$ is always finite while $\alpha \Rightarrow$ is either infinite (namely when $\alpha$ starts by $\mathcal{J}S$) or the singleton $\{\alpha\}$ (namely when $\alpha$ is a propositional variable or starts by some $S_i$). When $\beta \Rightarrow \alpha$ then the length of $\beta$ is less than or equal to the length of $\alpha$. Moreover, the set of causes of $\alpha$ has at most $\ell(\alpha)$ elements: $|\alpha \Leftarrow| \le \ell(\alpha)$. It follows that the sum of the lengths of all causes of $\alpha$ is at most quadratic in the length of $\alpha$:

**Proposition 1.** For every $\alpha$, $\sum_{\beta:\beta\Rightarrow\alpha} \ell(\beta) \le (\ell(\alpha))^2$.
We generalize atomic consequence to sets of atoms $s \in 2^{\text{OA}}$, alias states: $s \Rightarrow = \bigcup_{\alpha \in s} \alpha \Rightarrow$. When $s$ contains all its atomic consequences and all introspective atoms then we say that $s$ is *introspectively closed* or, for short, *introspective*. The set of all introspective states is

$$ I-\text{STATES} = \{s \Rightarrow \cup \text{I-OA} : s \in 2^{\text{OA}}\}. $$

This is an infinite set. Each of its elements is infinite due to infinity of I-OA.

### 3.4. Language and semantics of EL-O

The language of EL-O is the set $\mathcal{L}_{\text{bool}}(\text{OA})$ of boolean formulas built from the set of observability atoms OA. We recall that the length of formulas is determined by the definition of length of atoms from Section 3.2. For example, $l(\mathcal{J}S S_1 p \wedge \neg S_2 q) = 7$. Note that the vocabulary of formulas such as $\mathcal{J}S S_1 p$ does not contain the ‘sub-atoms’ $p$ and $S_1 p$: we have $\text{Voc}(\mathcal{J}S S_1 p) = \{\mathcal{J}S S_1 p\}$. Note also that the language $\mathcal{L}_{\text{bool}}(\mathbb{P})$ is the fragment of $\mathcal{L}_{\text{bool}}(\text{OA})$ without observability operators.

**Example 2.** The goal of the original gossip problem is $\text{Goal}^{G_1} = \bigwedge_{i,j \in A} S_j s_i$. The goal of obtaining shared knowledge of depth 2 is expressed by $\text{Goal}^{G_2} = \bigwedge_{i,j,r \in A} (S_j s_i \wedge S_r S_j s_i)$, i.e., every agent $r$ knows that every $S_j s_i$ is true.

We recall that a state is a subset of the vocabulary OA. A way of guaranteeing introspection was proposed in [6] where formulas are interpreted exclusively in the set of introspectively closed states *I-STATES*. As such states are always infinite, it is not immediately clear how to define model checking (which requires finite states). One way out is to work with ‘sufficiently introspective states’, as done in [9, Chapter 2]. Here we work with finite models and instead interpret formulas in such a way that introspection is simulated. The EL-O truth conditions are just as those for CPC of Section 3.1, except that for atomic formulas we stipulate:

$$ s \models \alpha \text{ iff } \alpha \in s \Rightarrow \cup \text{I-OA}. $$
We generalize atomic consequence to sets of atoms $s \in 2^{\text{OA}}$, alias states: $s \Rightarrow = \cup_{\alpha \in s} \alpha \Rightarrow$. When $s$ contains all its atomic consequences and all introspective atoms then we say that $s$ is *introspectively closed* or, for short, *introspective*. The set of all introspective states is

$$ I-\text{STATES} = \{s \Rightarrow \cup \text{I-OA} : s \in 2^{\text{OA}}\}. $$

This is an infinite set. Each of its elements is infinite due to infinity of I-OA.

### 3.4. Language and semantics of EL-O

The language of EL-O is the set $\mathcal{L}_{\text{bool}}(\text{OA})$ of boolean formulas built from the set of observability atoms OA. We recall that the length of formulas is determined by the definition of length of atoms from Section 3.2. For example, $l(\mathcal{J}S S_1 p \wedge \neg S_2 q) = 7$. Note that the vocabulary of formulas such as $\mathcal{J}S S_1 p$ does not contain the ‘sub-atoms’ $p$ and $S_1 p$: we have $\text{Voc}(\mathcal{J}S S_1 p) = \{\mathcal{J}S S_1 p\}$. Note also that the language $\mathcal{L}_{\text{bool}}(\mathbb{P})$ is the fragment of $\mathcal{L}_{\text{bool}}(\text{OA})$ without observability operators.

**Example 2.** The goal of the original gossip problem is $\text{Goal}^{G_1} = \bigwedge_{i,j \in A} S_j s_i$. The goal of obtaining shared knowledge of depth 2 is expressed by $\text{Goal}^{G_2} = \bigwedge_{i,j,r \in A} (S_j s_i \wedge S_r S_j s_i)$, i.e., every agent $r$ knows that every $S_j s_i$ is true.

We recall that a state is a subset of the vocabulary OA. A way of guaranteeing introspection was proposed in [6] where formulas are interpreted exclusively in the set of introspectively closed states *I-STATES*. As such states are always infinite, it is not immediately clear how to define model checking (which requires finite states). One way out is to work with ‘sufficiently introspective states’, as done in [9, Chapter 2]. Here we work with finite models and instead interpret formulas in such a way that introspection is simulated. The EL-O truth conditions are just as those for CPC of Section 3.1, except that for atomic formulas we stipulate:

$$ s \models \alpha \text{ iff } \alpha \in s \Rightarrow \cup \text{I-OA}. $$
Hence $\alpha$ is true in $s$ if and only if $\alpha$ is introspective or $\beta \Rightarrow \alpha$ for some $\beta \in s$.

The EL-O semantics coincides with the CPC semantics for the fragment $\mathcal{L}_{bool}(\mathbb{P})$ of $\mathcal{L}_{bool}(OA)$:

280

**Proposition 2.** Let $\varphi \in \mathcal{L}_{bool}(\mathbb{P})$. Then $s \models \varphi$ iff $s \models^{CPC} \varphi$.

**Example 3.** Let $s_0^{G_1}$ be the initial state of the gossip problem from Example 1) Then $s_0^{G_1} \models S_i s_i \wedge \bigwedge_{j \neq i} \neg S_i s_j$ for every $i \in A$.

285

A formula $\varphi \in \mathcal{L}_{bool}(OA)$ is EL-O satisfiable iff $s \models \varphi$ for some $s \in 2^{OA}$; it is EL-O valid iff $s \models \varphi$ for every $s \in 2^{OA}$. Clearly, an atom $\alpha$ is EL-O valid if and only if it is introspective. Moreover, for atoms $\alpha, \beta \in OA$ we have that $\alpha \rightarrow \beta$ is EL-O valid iff $\alpha \Rightarrow \beta$ or $\beta$ is introspective.

**Proposition 3.** Let $A, B \subseteq OA$ be such that $(\bigwedge_{\alpha \in A} \alpha) \wedge (\bigwedge_{\beta \in B} \neg \beta)$ is EL-O unsatisfiable. Then $B$ contains some introspective $\beta$, or there are $\alpha \in A, \beta \in B$ such that $\alpha \Rightarrow \beta$.

290

*Proof.* We prove the contraposition: suppose $B$ contains no introspective atom and there are no $\alpha \in A$ and $\beta \in B$ such that $\alpha \Rightarrow \beta$. We show that the state $s = A$ satisfies $(\bigwedge_{\alpha \in A} \alpha) \wedge (\bigwedge_{\beta \in B} \neg \beta)$. First, $s$ satisfies every element of $A$. Second, $s$ does not satisfy any $\beta \in B$: otherwise $\beta$ would be introspective, or we would have $\alpha \Rightarrow \beta$ for some $\alpha \in A$. $\square$

295

*Remark 1.* When $\mathcal{A}$ is a singleton then $S_i p \wedge \neg \mathcal{J}S p$ is satisfiable. While this anomaly could be taken care of by a modification of the semantics, we do not do so for the sake of readability and content ourselves with the observation that the $\mathcal{J}S$ operator is superfluous when there is only one agent.

*Remark 2.* It would be interesting to generalise joint observability from $\mathcal{A}$ to arbitrary subsets of $\mathcal{A}$. For instance, after a gossiping phone call between agents $i$ and $j$ all secrets previously known by one of them become jointly observable by the group $\{i, j\}$. Such an extension was proposed in [33]; however, the solution turned out to be unsatisfactory. The problem is that joint visibilities of subgroups interact in complex ways, in particular when observability evolves.

300

305
Hence $\alpha$ is true in $s$ if and only if $\alpha$ is introspective or $\beta \Rightarrow \alpha$ for some $\beta \in s$.

The EL-O semantics coincides with the CPC semantics for the fragment $\mathcal{L}_{bool}(\mathbb{P})$ of $\mathcal{L}_{bool}(OA)$:

280

**Proposition 2.** Let $\varphi \in \mathcal{L}_{bool}(\mathbb{P})$. Then $s \models \varphi \iff s \models^{CPC} \varphi$.

**Example 3.** Let $s_0^{G_1}$ be the initial state of the gossip problem from Example 1) Then $s_0^{G_1} \models S_i s_i \wedge \bigwedge_{j \neq i} \neg S_i s_j$ for every $i \in A$.

285

A formula $\varphi \in \mathcal{L}_{bool}(OA)$ is EL-O satisfiable iff $s \models \varphi$ for some $s \in 2^{OA}$; it is EL-O valid iff $s \models \varphi$ for every $s \in 2^{OA}$. Clearly, an atom $\alpha$ is EL-O valid if and only if it is introspective. Moreover, for atoms $\alpha, \beta \in OA$ we have that $\alpha \rightarrow \beta$ is EL-O valid iff $\alpha \Rightarrow \beta$ or $\beta$ is introspective.

**Proposition 3.** Let $A, B \subseteq OA$ be such that $(\bigwedge_{\alpha \in A} \alpha) \wedge (\bigwedge_{\beta \in B} \neg \beta)$ is EL-O unsatisfiable. Then $B$ contains some introspective $\beta$, or there are $\alpha \in A, \beta \in B$ such that $\alpha \Rightarrow \beta$.

290

*Proof.* We prove the contraposition: suppose $B$ contains no introspective atom and there are no $\alpha \in A$ and $\beta \in B$ such that $\alpha \Rightarrow \beta$. We show that the state $s = A$ satisfies $(\bigwedge_{\alpha \in A} \alpha) \wedge (\bigwedge_{\beta \in B} \neg \beta)$. First, $s$ satisfies every element of $A$. Second, $s$ does not satisfy any $\beta \in B$: otherwise $\beta$ would be introspective, or we would have $\alpha \Rightarrow \beta$ for some $\alpha \in A$. $\square$

295

*Remark 1.* When $\mathcal{A}$ is a singleton then $S_i p \wedge \neg \mathcal{J}S p$ is satisfiable. While this anomaly could be taken care of by a modification of the semantics, we do not do so for the sake of readability and content ourselves with the observation that the $\mathcal{J}S$ operator is superfluous when there is only one agent.

*Remark 2.* It would be interesting to generalise joint observability from $\mathcal{A}$ to arbitrary subsets of $\mathcal{A}$. For instance, after a gossiping phone call between agents $i$ and $j$ all secrets previously known by one of them become jointly observable by the group $\{i, j\}$. Such an extension was proposed in [33]; however, the solution turned out to be unsatisfactory. The problem is that joint visibilities of subgroups interact in complex ways, in particular when observability evolves.

300

305
In the rest of the section we establish finite model property, given an axiomatisation, and prove NP-completeness of EL-O satisfiability.

### 3.5. Finite model property

A standard property of CPC is that $s \models^{CPC} \varphi$ iff $s \cap \text{Voc}(\varphi) \models^{CPC} \varphi$. The non-standard truth condition for atoms in EL-O makes that this does not hold in EL-O. (It suffices to consider $s = \{JS p\}$ and $\varphi = S_i p$ to see this.) Notwithstanding, we obtain a finite model property by closing the state $s$.

First of all, let us say that two states $s$ and $s'$ agree on the set of atoms $A \subseteq \text{OA}$ when they assign the same truth value to every element of $A$, i.e., when for every $\alpha \in A$, $s \models \alpha$ iff $s' \models \alpha$. This is not enough to guarantee that $s \cap A = s' \cap A$. To witness, consider $s = \{JS p\}$, $s' = \{S_i p\}$, and $A = \{S_i p\}$: $s$ and $s'$ agree on $A$, but $s \cap A = \emptyset$ while $s' \cap A = \{S_i p\}$. However by straightforward induction on the structure of formulas we get:

**Proposition 4.** Let $\varphi \in \mathcal{L}_{\text{bool}}(\text{OA})$ be a formula and $s, s' \in 2^{\text{OA}}$ two states agreeing on $\text{Voc}(\varphi)$. Then $s \models \varphi$ iff $s' \models \varphi$.

**Proposition 5.** Let $\varphi \in \mathcal{L}_{\text{bool}}(\text{OA})$ be a formula and $s \in 2^{\text{OA}}$ a state. Then $s \models \varphi$ iff $(s \models \bigcup \text{I-OA}) \cap \text{Voc}(\varphi) \models \varphi$.

*Proof.* The proof is by induction on the structure of $\varphi$. The only non-trivial case is the induction base. We have $s \models \alpha$ iff $s \models \bigcup \text{I-OA} \models \alpha$ iff $(s \models \bigcup \text{I-OA}) \cap \text{Voc}(\varphi) \models \alpha$. The last equivalence holds thanks to Proposition 4. $\square$

### 3.6. Complexity of EL-O satisfiability

**Proposition 6.** Let $s \in 2^{\text{OA}}$ be a state and $\varphi \in \mathcal{L}_{\text{bool}}(\text{OA})$ a formula. Then $s \models \varphi$ iff $s \models \bigcup \text{I-OA} \models^{CPC} \varphi$.

*Proof.* The proof is by induction on the structure of $\varphi$. The only non-trivial case is the induction base. If $\alpha \in \text{I-OA}$ then both $s \models \alpha$ and $\text{I-OA} \models^{CPC} \alpha$ hold. Otherwise, for $\alpha \notin \text{I-OA}$ we have $s \models \alpha$ iff $\alpha \in s \models$ iff $s \models^{CPC} \alpha$. $\square$

**Proposition 7.** The problem of deciding satisfiability of $\mathcal{L}_{\text{bool}}(\text{OA})$ formulas is NP-complete.
In the rest of the section we establish finite model property, given an axiomatisation, and prove NP-completeness of EL-O satisfiability.

### 3.5. Finite model property

A standard property of CPC is that $s \models^{CPC} \varphi$ iff $s \cap \text{Voc}(\varphi) \models^{CPC} \varphi$. The non-standard truth condition for atoms in EL-O makes that this does not hold in EL-O. (It suffices to consider $s = \{JS p\}$ and $\varphi = S_i p$ to see this.) Notwithstanding, we obtain a finite model property by closing the state $s$.

First of all, let us say that two states $s$ and $s'$ agree on the set of atoms $A \subseteq \text{OA}$ when they assign the same truth value to every element of $A$, i.e., when for every $\alpha \in A$, $s \models \alpha$ iff $s' \models \alpha$. This is not enough to guarantee that $s \cap A = s' \cap A$. To witness, consider $s = \{JS p\}$, $s' = \{S_i p\}$, and $A = \{S_i p\}$: $s$ and $s'$ agree on $A$, but $s \cap A = \emptyset$ while $s' \cap A = \{S_i p\}$. However by straightforward induction on the structure of formulas we get:

**Proposition 4.** Let $\varphi \in \mathcal{L}_{\text{bool}}(\text{OA})$ be a formula and $s, s' \in 2^{\text{OA}}$ two states agreeing on $\text{Voc}(\varphi)$. Then $s \models \varphi$ iff $s' \models \varphi$.

**Proposition 5.** Let $\varphi \in \mathcal{L}_{\text{bool}}(\text{OA})$ be a formula and $s \in 2^{\text{OA}}$ a state. Then $s \models \varphi$ iff $(s \models \bigcup \text{I-OA}) \cap \text{Voc}(\varphi) \models \varphi$.

*Proof.* The proof is by induction on the structure of $\varphi$. The only non-trivial case is the induction base. We have $s \models \alpha$ iff $s \models \bigcup \text{I-OA} \models \alpha$ iff $(s \models \bigcup \text{I-OA}) \cap \text{Voc}(\varphi) \models \alpha$. The last equivalence holds thanks to Proposition 4. $\square$

### 3.6. Complexity of EL-O satisfiability

**Proposition 6.** Let $s \in 2^{\text{OA}}$ be a state and $\varphi \in \mathcal{L}_{\text{bool}}(\text{OA})$ a formula. Then $s \models \varphi$ iff $s \models \bigcup \text{I-OA} \models^{CPC} \varphi$.

*Proof.* The proof is by induction on the structure of $\varphi$. The only non-trivial case is the induction base. If $\alpha \in \text{I-OA}$ then both $s \models \alpha$ and $\text{I-OA} \models^{CPC} \alpha$ hold. Otherwise, for $\alpha \notin \text{I-OA}$ we have $s \models \alpha$ iff $\alpha \in s \models$ iff $s \models^{CPC} \alpha$. $\square$

**Proposition 7.** The problem of deciding satisfiability of $\mathcal{L}_{\text{bool}}(\text{OA})$ formulas is NP-complete.
$$S_i S_i \alpha \qquad (Vis_1)$$

$$JS JS \alpha \qquad (Vis_2)$$

$$JS S_i S_i \alpha \qquad (Vis_3)$$

$$JS \alpha \rightarrow S_i \alpha \qquad (Vis_4)$$

$$JS \alpha \rightarrow JS S_i \alpha \qquad (Vis_5)$$

<caption>Table 1: Axioms of EL-O</caption>

*Proof.* Hardness is the case because EL-O satisfiability and CPC satisfiability coincide for the $\mathcal{L}_{bool}(\mathbb{P})$ fragment of $\mathcal{L}_{bool}(OA)$ (Proposition 2). For membership, guess some subset $s \in 2^{\text{Voc}(\varphi)}$ and check in polynomial time:

1. that $s$ contains all its relevant consequences: for every $\alpha \in \text{Voc}(\varphi)$ and $\beta \in s$, check that if $\beta \Rightarrow \alpha$ then $\alpha \in s$;

2. that $s$ contains all introspective atoms from $\text{Voc}(\varphi)$: for every $\alpha \in \text{Voc}(\varphi)$, check that if $\alpha \in \text{OA}$ then $\alpha \in s$;

3. that $s \models^{\text{CPC}} \varphi$.

Checking that $s \models^{\text{CPC}} \varphi$ is tantamount to checking that $s \models \varphi$ because: (a) thanks to the first and second check, $s$ equals ($s \Rightarrow \cup \text{I-OA}) \cap \text{Voc}(\varphi)$, and therefore $s \models^{\text{CPC}} \varphi$ iff ($s \Rightarrow \cup \text{I-OA}) \cap \text{Voc}(\varphi) \models^{\text{CPC}} \varphi$; (b) in CPC, the latter is the same as $s \Rightarrow \cup \text{I-OA} \models^{\text{CPC}} \varphi$ (contrarily to EL-O, in CPC irrelevant atoms outside $\text{Voc}(\varphi)$ can be dropped from valuations); finally, (c) Proposition 6 applies. $\square$

### 3.7. Axiomatisation of EL-O validities

The EL-O validities of our language $\mathcal{L}_{bool}(OA)$ are axiomatised by the schemas of Table 1 together with CPC. We prove its completeness via CPC.

**Proposition 8.** Let $\varphi \in \mathcal{L}_{bool}(OA)$ be a formula. Then $\varphi$ is EL-O valid iff $\varphi$ is provable in CPC from the axiom schemas $Vis_1-Vis_5$ of Table 1.
$$S_i S_i \alpha \qquad (Vis_1)$$

$$JS JS \alpha \qquad (Vis_2)$$

$$JS S_i S_i \alpha \qquad (Vis_3)$$

$$JS \alpha \rightarrow S_i \alpha \qquad (Vis_4)$$

$$JS \alpha \rightarrow JS S_i \alpha \qquad (Vis_5)$$

<caption>Table 1: Axioms of EL-O</caption>

*Proof.* Hardness is the case because EL-O satisfiability and CPC satisfiability coincide for the $\mathcal{L}_{bool}(\mathbb{P})$ fragment of $\mathcal{L}_{bool}(OA)$ (Proposition 2). For membership, guess some subset $s \in 2^{\text{Voc}(\varphi)}$ and check in polynomial time:

1. that $s$ contains all its relevant consequences: for every $\alpha \in \text{Voc}(\varphi)$ and $\beta \in s$, check that if $\beta \Rightarrow \alpha$ then $\alpha \in s$;

2. that $s$ contains all introspective atoms from $\text{Voc}(\varphi)$: for every $\alpha \in \text{Voc}(\varphi)$, check that if $\alpha \in \text{OA}$ then $\alpha \in s$;

3. that $s \models^{\text{CPC}} \varphi$.

Checking that $s \models^{\text{CPC}} \varphi$ is tantamount to checking that $s \models \varphi$ because: (a) thanks to the first and second check, $s$ equals ($s \Rightarrow \cup \text{I-OA}) \cap \text{Voc}(\varphi)$, and therefore $s \models^{\text{CPC}} \varphi$ iff ($s \Rightarrow \cup \text{I-OA}) \cap \text{Voc}(\varphi) \models^{\text{CPC}} \varphi$; (b) in CPC, the latter is the same as $s \Rightarrow \cup \text{I-OA} \models^{\text{CPC}} \varphi$ (contrarily to EL-O, in CPC irrelevant atoms outside $\text{Voc}(\varphi)$ can be dropped from valuations); finally, (c) Proposition 6 applies. $\square$

### 3.7. Axiomatisation of EL-O validities

The EL-O validities of our language $\mathcal{L}_{bool}(OA)$ are axiomatised by the schemas of Table 1 together with CPC. We prove its completeness via CPC.

**Proposition 8.** Let $\varphi \in \mathcal{L}_{bool}(OA)$ be a formula. Then $\varphi$ is EL-O valid iff $\varphi$ is provable in CPC from the axiom schemas $Vis_1-Vis_5$ of Table 1.
*Proof.* We again take advantage of Proposition 6 and show that $Vis_1-Vis_5$ characterise the set of introspectively closed states {$s \Rightarrow \cup \text{I-OA} : s \in 2^{\text{OA}}$}. The right-to-left direction is clear: each of the five axiom schemas is valid in introspectively closed states. For the left-to-right direction, we show that every $s$ satisfying $Vis_1-Vis_5$ is introspectively closed.

For closure under atomic consequence, let $s \models \alpha$. The interesting case is when $\alpha = JS\alpha'$. Then $s \models JS S_{i_1} \alpha'$ by axiom $Vis_5$, and also $s \models JS S_{i_2} S_{i_1} \alpha'$, and so on: we can generate any $s \models JS S_{i_m} \dots S_{i_1} \alpha'$ and then, by $Vis_4$, we can obtain $s \models S_{i_m} \dots S_{i_1} \alpha'$. Moreover, we have $s \models JS \alpha'$ by $Vis_2$, and in the same way, we can generate $s \models S_{i_m} \dots S_{i_1} JS\alpha'$ for any agents $i_1, \dots, i_m$ and $i$. We therefore obtain that $s$ satisfies any sequence whose strict postfix is $\alpha'$, that is, every $\sigma \alpha'$ for any $\sigma \in \text{OBS}^+$.

We use the same technique to show that a state $s$ satisfying $Vis_1-Vis_5$ satisfies every $\sigma S_i S_i \alpha$ for $\sigma \in \text{OBS}^+$ and every $\sigma JS\alpha$ for $\sigma \in \text{OBS}^+$: we obtain the first with $Vis_1$ (for $\sigma$ empty) and $Vis_3$, $Vis_4$, and $Vis_5$ (for $\sigma$ non-empty), and the second with $Vis_2$, $Vis_4$, and $Vis_5$. $\square$

*Remark 3.* We do not require states to satisfy the infinitary constraint “if $\sigma \alpha \in s$ for every $\sigma \in \{S_i : i \in A\}^+$ then $JS\alpha \in s$”, which is the EL-O counterpart of the transitive closure constraint on Kripke models (see Remark 4 in Section 4.2). The reason is technical: it is not obvious how to extend the axiomatisation of EL-O in a finitary way to account for that constraint. Our recent axiomatisation of ‘common knowledge whether’ of [34] might provide a solution; we however do not pursue this further here.

## 4. EL-O as a fragment of epistemic logic S5

We now situate our lightweight epistemic logic w.r.t. the standard epistemic logic S5 with ‘knowing-that’ operators $CK$ and $K_i$. We are going to exploit that $S_i\varphi$ can be viewed as an abbreviation of $K_i\varphi \lor K_i\neg\varphi$ and $JS\varphi$ as an abbreviation of $CK\varphi \lor CK\neg\varphi$. Then the language $\mathcal{L}_{\text{bool}}(\text{OA})$ of EL-O becomes as a fragment of $\mathcal{L}_{\text{EL}}$. When we make this identification we are going
*Proof.* We again take advantage of Proposition 6 and show that $Vis_1-Vis_5$ characterise the set of introspectively closed states $\{s \Rightarrow \cup \text{I-OA} : s \in 2^{\text{OA}}\}$. The right-to-left direction is clear: each of the five axiom schemas is valid in introspectively closed states. For the left-to-right direction, we show that every $s$ satisfying $Vis_1-Vis_5$ is introspectively closed.

For closure under atomic consequence, let $s \models \alpha$. The interesting case is when $\alpha = JS\alpha'$. Then $s \models JS S_{i_1} \alpha'$ by axiom $Vis_5$, and also $s \models JS S_{i_2} S_{i_1} \alpha'$, and so on: we can generate any $s \models JS S_{i_m} \dots S_{i_1} \alpha'$ and then, by $Vis_4$, we can obtain $s \models S_{i_m} \dots S_{i_1} \alpha'$. Moreover, we have $s \models JS \alpha'$ by $Vis_2$, and in the same way, we can generate $s \models S_{i_m} \dots S_{i_1} JS\alpha'$ for any agents $i_1, \dots, i_m$ and $i$. We therefore obtain that $s$ satisfies any sequence whose strict postfix is $\alpha'$, that is, every $\sigma \alpha'$ for any $\sigma \in \text{OBS}^+$.

We use the same technique to show that a state $s$ satisfying $Vis_1-Vis_5$ satisfies every $\sigma S_i S_i \alpha$ for $\sigma \in \text{OBS}^*$ and every $\sigma JS\alpha$ for $\sigma \in \text{OBS}^+$: we obtain the first with $Vis_1$ (for $\sigma$ empty) and $Vis_3$, $Vis_4$, and $Vis_5$ (for $\sigma$ non-empty), and the second with $Vis_2$, $Vis_4$, and $Vis_5$. $\square$

*Remark 3.* We do not require states to satisfy the infinitary constraint “if $\sigma \alpha \in s$ for every $\sigma \in \{S_i : i \in A\}^+$ then $JS\alpha \in s$”, which is the EL-O counterpart of the transitive closure constraint on Kripke models (see Remark 4 in Section 4.2). The reason is technical: it is not obvious how to extend the axiomatisation of EL-O in a finitary way to account for that constraint. Our recent axiomatisation of ‘common knowledge whether’ of [34] might provide a solution; we however do not pursue this further here.

## 4. EL-O as a fragment of epistemic logic S5

We now situate our lightweight epistemic logic w.r.t. the standard epistemic logic S5 with ‘knowing-that’ operators $CK$ and $K_i$. We are going to exploit that $S_i\varphi$ can be viewed as an abbreviation of $K_i\varphi \lor K_i\neg\varphi$ and $JS\varphi$ as an abbreviation of $CK\varphi \lor CK\neg\varphi$. Then the language $\mathcal{L}_{\text{bool}}(\text{OA})$ of EL-O becomes as a fragment of $\mathcal{L}_{\text{EL}}$. When we make this identification we are going
to talk about the EL-O fragment of $\mathcal{L}_{EL}$.

Our main result is that for the EL-O fragment of $\mathcal{L}_{EL}$, the axioms of Table 1 are sound and complete w.r.t. validity in S5 models (Proposition11). It follows by Proposition 7 that our lightweight epistemic logic is a fragment of standard epistemic logic with an NP-complete satisfiability problem. This is an important result because satisfiability of $\mathcal{L}_{EL}$ formulas is PSPACE-complete as soon as there are two agents, and this is the case even without the common knowledge operator [35]. But first of all we recall the standard epistemic language $\mathcal{L}_{EL}$ and the models in which its formulas are interpreted.

### 4.1. The standard epistemic language

The grammar of the standard language $\mathcal{L}_{EL}$ is:

$$ \mathcal{L}_{EL}: \varphi ::= p \mid \neg \varphi \mid \varphi \land \varphi \mid K_i \varphi \mid CK \varphi $$

where $p$ ranges over the set of propositional variables $\mathbb{P}$. The formula $K_i\varphi$ reads “$i$ knows that $\varphi$” and $CK\varphi$ reads “it is common knowledge that $\varphi$”. Hence there are no observability atoms: the vocabulary of $\mathcal{L}_{EL}$ is just the set of propositional variables $\mathbb{P}$, of which we suppose that it is identical to the set $\mathbb{P}$ from which the observability atoms of Section 3.2 were built.

**Example 4.** The goal of the original gossip problem is to obtain shared knowledge of all secrets. This is expressed in the standard epistemic language $\mathcal{L}_{EL}$ by $\bigwedge_{i,j \in \mathcal{A}} (K_j s_i \lor K_j \neg s_i)$. If we take $K_i\varphi$ to be an abbreviation of $p \land S_i p$ (see Section 2) then this goal reduces to the $\mathcal{L}_{bool}(OA)$ formula $\text{Goal}^{G_1} = \bigwedge_{i,j \in \mathcal{A}} S_j s_i$. Shared knowledge up to depth 2 is expressed by $\bigwedge_{i,j,r \in \mathcal{A}} (K_r K_j s_i \lor K_r K_j \neg s_i)$; reducing $K_j$ and $K_r$ we get $\bigwedge_{i,j,r \in \mathcal{A}} (S_j s_i \land S_r s_i \land S_r S_j s_i)$, which in CPC is equivalent to $\text{Goal}^{G_2} = \bigwedge_{i,j,r \in \mathcal{A}} (S_j s_i \land S_r S_j s_i)$. We have already seen these two $\mathcal{L}_{bool}(OA)$ formulas in Example 2. In the generalised gossip problem [6, 36] the goal is shared knowledge up to depth $k$, written $\bigwedge_{i \in \mathcal{A}} \bigwedge_{\vec{K} \in \{K_j : j \in \mathcal{A}\}^k} (\vec{K} s_i \lor \vec{K} \neg s_i)$ in $\mathcal{L}_{EL}$, where $\{K_j : j \in \mathcal{A}\}^k$ is the set of all sequences of individual 'knowing-that' operators of length $k$. It reduces to the $\mathcal{L}_{bool}(OA)$ formula
to talk about the EL-O fragment of $\mathcal{L}_{EL}$.

Our main result is that for the EL-O fragment of $\mathcal{L}_{EL}$, the axioms of Table 1 are sound and complete w.r.t. validity in S5 models (Proposition 11). It follows by Proposition 7 that our lightweight epistemic logic is a fragment of standard epistemic logic with an NP-complete satisfiability problem. This is an important result because satisfiability of $\mathcal{L}_{EL}$ formulas is PSPACE-complete as soon as there are two agents, and this is the case even without the common knowledge operator [35]. But first of all we recall the standard epistemic language $\mathcal{L}_{EL}$ and the models in which its formulas are interpreted.

### 4.1. The standard epistemic language

The grammar of the standard language $\mathcal{L}_{EL}$ is:

$$ \mathcal{L}_{EL} : \varphi ::= p \mid \neg \varphi \mid \varphi \land \varphi \mid K_i \varphi \mid CK \varphi $$

where $p$ ranges over the set of propositional variables $\mathbb{P}$. The formula $K_i\varphi$ reads “$i$ knows that $\varphi$” and $CK\varphi$ reads “it is common knowledge that $\varphi$”. Hence there are no observability atoms: the vocabulary of $\mathcal{L}_{EL}$ is just the set of propositional variables $\mathbb{P}$, of which we suppose that it is identical to the set $\mathbb{P}$ from which the observability atoms of Section 3.2 were built.

**Example 4.** The goal of the original gossip problem is to obtain shared knowledge of all secrets. This is expressed in the standard epistemic language $\mathcal{L}_{EL}$ by $\bigwedge_{i,j \in A}(K_j s_i \lor K_j \neg s_i)$. If we take $K_i\varphi$ to be an abbreviation of $p \land S_i p$ (see Section 2) then this goal reduces to the $\mathcal{L}_{bool}(OA)$ formula $Goal^{G_1} = \bigwedge_{i,j \in A} S_j s_i$. Shared knowledge up to depth 2 is expressed by $\bigwedge_{i,j,r \in A}(K_r K_j s_i \lor K_r K_j \neg s_i)$; reducing $K_j$ and $K_r$ we get $\bigwedge_{i,j,r \in A}(S_j s_i \land S_r s_i \land S_r S_j s_i)$, which in CPC is equivalent to $Goal^{G_2} = \bigwedge_{i,j,r \in A}(S_j s_i \land S_r S_j s_i)$. We have already seen these two $\mathcal{L}_{bool}(OA)$ formulas in Example 2. In the generalised gossip problem [6, 36] the goal is shared knowledge up to depth $k$, written $\bigwedge_{i \in A} \bigwedge_{\vec{K} \in \{K_j : j \in A\}^k} (\vec{K} s_i \lor \vec{K} \neg s_i)$ in $\mathcal{L}_{EL}$, where $\{K_j : j \in A\}^k$ is the set of all sequences of individual 'knowing-that' operators of length $k$. It reduces to the $\mathcal{L}_{bool}(OA)$ formula
$$ Goal^{G_k} = \bigwedge_{i \in A} \bigwedge_{\sigma \in \{S_j : j \in A\}^{\le k}} \sigma s_i $$

410 where $\{S_j : j \in A\}^{\le k}$ is the set of all sequences of individual observability operators up to length $k$.

## 4.2. S5 Kripke models and the canonical model for EL-O

We suppose that CK and the $K_i$ are S5 modal operators and that common knowledge implies individual knowledge. Semantically, an S5 Kripke model [35] is a tuple $M = (W, \sim_A, \{\sim_i\}_{i \in A}, V)$ where W is a nonempty set of possible worlds; $\sim_A$ and every $\sim_i$ are equivalence relations on W such that every $\sim_i$ is a subset of $\sim_A$; and $V: W \to 2^P$ is a valuation. The interpretation of $\mathcal{L}_{EL}$ formulas in a pointed Kripke model $(M, w)$ is:

$$ M, w \models K_i \varphi \text{ iff } M, w' \models \varphi \text{ for every } w' \text{ such that } w \sim_i w'; $$

$$ M, w \models CK\varphi \text{ iff } M, w' \models \varphi \text{ for every } w' \text{ such that } w \sim_A w'; $$

and as usual for the boolean operators. Formula $\varphi$ is valid in $M$ if $M, s \models \varphi$ for every $s \in W$; $\varphi$ is valid in S5 Kripke models if $\varphi$ is valid in every S5 Kripke model.

415

**Remark 4.** Every $\sim_i$ being included in $\sim_A$, the accessibility relation for common knowledge contains the transitive closure of the union of the individual accessibility relations $(\cup_{i \in A} \sim_i)^*$, but does not necessarily equal it. The former property corresponds to the fact that in introspective states, $JS\alpha \in s$ implies that $\sigma\alpha \in s$ for any non-empty sequence $\sigma$ while the other direction fails to hold, as already discussed in Remark 3. Our notion of common knowledge is therefore weaker than standard common knowledge in that the induction axiom $CK(\varphi \rightarrow \bigwedge_{i \in A} K_i \varphi) \rightarrow (\varphi \rightarrow CK\varphi)$ is not valid. A similar notion was called ‘fictitious knower’ or ‘any fool’ by Genesereth and Nilsson [37] and was used in modal extensions of logic programming in the 90s [38, 39]. We have argued elsewhere that the induction axiom is too strong for a logic of common knowledge [40, 41].

Let us establish that every EL-O valuation $s$ can be identified with a particular pointed S5 Kripke model ($M^{EL-O}, s$). The first thing we do is to define
$$ Goal^{G_k} = \bigwedge_{i \in A} \bigwedge_{\sigma \in \{S_j : j \in A\}^{\le k}} \sigma s_i $$

where $\{S_j : j \in A\}^{\le k}$ is the set of all sequences of individual observability operators up to length $k$.

## 4.2. S5 Kripke models and the canonical model for EL-O

We suppose that CK and the $K_i$ are S5 modal operators and that common knowledge implies individual knowledge. Semantically, an S5 Kripke model [35] is a tuple $M = (W, \sim_A, \{\sim_i\}_{i \in A}, V)$ where W is a nonempty set of possible worlds; $\sim_A$ and every $\sim_i$ are equivalence relations on W such that every $\sim_i$ is a subset of $\sim_A$; and $V: W \to 2^P$ is a valuation. The interpretation of $\mathcal{L}_{EL}$ formulas in a pointed Kripke model $(M, w)$ is:

$$ M, w \models K_i \varphi \text{ iff } M, w' \models \varphi \text{ for every } w' \text{ such that } w \sim_i w'; $$

$$ M, w \models CK\varphi \text{ iff } M, w' \models \varphi \text{ for every } w' \text{ such that } w \sim_A w'; $$

and as usual for the boolean operators. Formula $\varphi$ is valid in $M$ if $M, s \models \varphi$ for every $s \in W$; $\varphi$ is valid in S5 Kripke models if $\varphi$ is valid in every S5 Kripke model.

**Remark 4.** Every $\sim_i$ being included in $\sim_A$, the accessibility relation for common knowledge contains the transitive closure of the union of the individual accessibility relations $(\cup_{i \in A} \sim_i)^*$, but does not necessarily equal it. The former property corresponds to the fact that in introspective states, $JS\alpha \in s$ implies that $\sigma\alpha \in s$ for any non-empty sequence $\sigma$ while the other direction fails to hold, as already discussed in Remark 3. Our notion of common knowledge is therefore weaker than standard common knowledge in that the induction axiom $CK(\varphi \rightarrow \bigwedge_{i \in A} K_i\varphi) \rightarrow (\varphi \rightarrow CK\varphi)$ is not valid. A similar notion was called 'fictitious knower' or 'any fool' by Genesereth and Nilsson [37] and was used in modal extensions of logic programming in the 90s [38, 39]. We have argued elsewhere that the induction axiom is too strong for a logic of common knowledge [40, 41].

Let us establish that every EL-O valuation $s$ can be identified with a particular pointed S5 Kripke model $(M^{EL-O}, s)$. The first thing we do is to define
how the states' observability information determines equivalence relations between states. For every $s, s' \in 2^{\text{OA}}$ we define:

$$sR_i s' \text{ iff } s \text{ and } s' \text{ agree on every } \alpha \text{ such that } s \models S_i \alpha;$$

$$sR_A s' \text{ iff } s \text{ and } s' \text{ agree on every } \alpha \text{ such that } s \models \mathcal{J}S \alpha.$$

(Remember that agreement is defined in Section 3.5.) While these relations are clearly reflexive, it is not immediately clear that they are also symmetric and transitive; so let us prove that.

**Proposition 9.** All relations $R_i$ and $R_A$ are equivalence relations.

*Proof.* We prove symmetry and transitivity of $R_i$ for an arbitrary $i$; the proof for $R_A$ is analogous. For symmetry, suppose $sR_i s'$. Then for every $\alpha$, if $s \models S_i \alpha$ then $s$ and $s'$ agree on $\alpha$. Take an arbitrary $\beta$ such that $s' \models S_i \beta$. $s'$ agrees with $s$ on $S_i \beta$ because $s \models S_i S_i \beta$. Hence $s \models S_i \beta$, and $s$ and $s'$ agree on $\beta$, and therefore $s'R_i s$. For transitivity, suppose $sR_i s'$ and $s'R_i s''$ and suppose $s \models S_i \alpha$. We show that $s$ and $s''$ agree on $\alpha$. By hypothesis, $s$ and $s'$ agree on $\alpha$. As observed above, $s$ and $s'$ also agree on $S_i \alpha$ because $s \models S_i S_i \alpha$. Hence $s' \models S_i \alpha$, and so $s'$ and $s''$ agree on $\alpha$. Therefore $s$ and $s''$ agree on $\alpha$. $\square$

We are ready to define the canonical Kripke model for EL-O as the tuple $M^{\text{EL-O}} = (W^{\text{EL-O}}, \sim_{\mathcal{A}}^{\text{EL-O}}, \{\sim_i^{\text{EL-O}}\}_{i \in \mathcal{A}}, V^{\text{EL-O}})$ with

$$W^{\text{EL-O}} = I-\text{STATES} = \{s \Rightarrow \bigcup \text{I-OA} : s \in 2^{\text{OA}}\},$$

$$\sim_{\mathcal{A}}^{\text{EL-O}} = R_{\mathcal{A}} \cap (W^{\text{EL-O}} \times W^{\text{EL-O}}),$$

$$\sim_i^{\text{EL-O}} = R_i \cap (W^{\text{EL-O}} \times W^{\text{EL-O}}),$$

$$V^{\text{EL-O}}(w) = w \cap \mathbb{P} \text{ for every } w \in W^{\text{EL-O}}.$$

Hence the possible worlds of $M^{\text{EL-O}}$ are the introspectively closed states $I-\text{STATES}$ that we have defined in Section 3.3.

*Remark 5.* In EL-O, the empty initial state $s_0 = \emptyset$ models maximal ignorance: the agents do not know anything beyond tautologies. The simplicity of this modelling contrasts with the corresponding pointed Kripke model
how the states' observability information determines equivalence relations between states. For every $s, s' \in 2^{\text{OA}}$ we define:

$$sR_i s' \text{ iff } s \text{ and } s' \text{ agree on every } \alpha \text{ such that } s \models S_i \alpha;$$

$$sR_A s' \text{ iff } s \text{ and } s' \text{ agree on every } \alpha \text{ such that } s \models \mathcal{J}S \alpha.$$

(Remember that agreement is defined in Section 3.5.) While these relations are clearly reflexive, it is not immediately clear that they are also symmetric and transitive; so let us prove that.

**Proposition 9.** All relations $R_i$ and $R_A$ are equivalence relations.

*Proof.* We prove symmetry and transitivity of $R_i$ for an arbitrary $i$; the proof for $R_A$ is analogous. For symmetry, suppose $sR_i s'$. Then for every $\alpha$, if $s \models S_i \alpha$ then $s$ and $s'$ agree on $\alpha$. Take an arbitrary $\beta$ such that $s' \models S_i \beta$. $s'$ agrees with $s$ on $S_i \beta$ because $s \models S_i S_i \beta$. Hence $s \models S_i \beta$, and $s$ and $s'$ agree on $\beta$, and therefore $s'R_i s$. For transitivity, suppose $sR_i s'$ and $s'R_i s''$ and suppose $s \models S_i \alpha$. We show that $s$ and $s''$ agree on $\alpha$. By hypothesis, $s$ and $s'$ agree on $\alpha$. As observed above, $s$ and $s'$ also agree on $S_i \alpha$ because $s \models S_i S_i \alpha$. Hence $s' \models S_i \alpha$, and so $s'$ and $s''$ agree on $\alpha$. Therefore $s$ and $s''$ agree on $\alpha$. $\square$

We are ready to define the canonical Kripke model for EL-O as the tuple $M^{\text{EL-O}} = \langle W^{\text{EL-O}}, \sim_{\mathcal{A}}^{\text{EL-O}}, \{\sim_i^{\text{EL-O}}\}_{i \in \mathcal{A}}, V^{\text{EL-O}} \rangle$ with

$$W^{\text{EL-O}} = I-\text{STATES} = \{s \Rightarrow \bigcup \text{I-OA} : s \in 2^{\text{OA}}\},$$

$$\sim_{\mathcal{A}}^{\text{EL-O}} = R_{\mathcal{A}} \cap (W^{\text{EL-O}} \times W^{\text{EL-O}}),$$

$$\sim_i^{\text{EL-O}} = R_i \cap (W^{\text{EL-O}} \times W^{\text{EL-O}}),$$

$$V^{\text{EL-O}}(w) = w \cap \mathbb{P} \text{ for every } w \in W^{\text{EL-O}}.$$

Hence the possible worlds of $M^{\text{EL-O}}$ are the introspectively closed states $I-\text{STATES}$ that we have defined in Section 3.3.

*Remark 5.* In EL-O, the empty initial state $s_0 = \emptyset$ models maximal ignorance: the agents do not know anything beyond tautologies. The simplicity of this modelling contrasts with the corresponding pointed Kripke model
(M^EL-O, s₀): in that model, every agent can access infinitely many possible worlds from s₀. Actually the classical examples in introductory textbooks and articles about epistemic logic (such as the muddy children puzzle) are all modelled by finite Kripke models. As recently observed by Artemov [42], such finite models presuppose more or less tacitly a lot of common knowledge, which is too strong an assumption in many situations.

**Proposition 10.** Let $\varphi \in \mathcal{L}_{bool}(OA)$ and $s \in W^{EL-O}$. Then $s \models \varphi$ iff $M^{EL-O}, s \models \varphi$.

*Proof.* The proof is by induction on the structure of $\varphi$. The only interesting case is the base case of atoms $\alpha \in OA$. We use induction on the length of $\alpha$. When $\alpha = p$ then $M, s \models p$ iff $s \models p$ for any $s \in W^{EL-O}$ by definition of $V^{EL-O}$. When $\alpha = S_i\beta$ we prove the two directions of the equivalence.

* If $s \models S_i\beta$ for some $\beta \in OA$ and some $s \in W^{EL-O}$: consider $s' \in W^{EL-O}$ such that $s \sim_i^{EL-O} s'$. By definition of $\sim_i^{EL-O}$, $s$ and $s'$ agree on all $\alpha$ such that $s \models S_i\alpha$. Therefore if $s \models \beta$ then $s' \models \beta$, and by the induction hypothesis, $M^{EL-O}, s' \models \beta$; hence $M^{EL-O}, s \models K_i\beta$. If $s \models \neg\beta$, by the same argument, we have that $M^{EL-O}, s \models K_i\neg\beta$. Therefore $M^{EL-O}, s \models S_i\beta$.

* If $M^{EL-O}, s \models S_i\beta$ for some $\beta \in OA$ and some $s \in W^{EL-O}$, then either $M^{EL-O}, s \models K_i\beta$ or $M^{EL-O}, s \models K_i\neg\beta$. Suppose that $s \not\models S_i\beta$. In particular $\beta \notin I-OA$. If $s \models \beta$, consider $s' = s \setminus \beta^=$, and if $s \not\models \beta$, consider $s' = s \cup \beta^=$. In both cases $s' \in W^{EL-O}$, and $s$ and $s'$ agree on all $\alpha$ such that $s \models S_i\alpha$. Therefore $s \sim_i^{EL-O} s'$, but by the induction hypothesis, $M^{EL-O}, s' \models \beta$ iff $s' \models \beta$ iff $s' \models \neg\beta$ iff $M^{EL-O}, s \models \neg\beta$: this contradicts the hypothesis that $M^{EL-O}, s \models S_i\beta$.

For the case $\alpha = JS\beta$ we proceed similarly. $\square$

### 4.3. Completeness of the EL-O fragment of $\mathcal{L}_{EL}$ w.r.t. S5 validity

We now show that the EL-O semantics in terms of observability and the standard Kripke semantics have the same validities as far as the EL-O fragment is concerned.
(M^EL-O, s₀): in that model, every agent can access infinitely many possible worlds from s₀. Actually the classical examples in introductory textbooks and articles about epistemic logic (such as the muddy children puzzle) are all modelled by finite Kripke models. As recently observed by Artemov [42], such finite models presuppose more or less tacitly a lot of common knowledge, which is too strong an assumption in many situations.

**Proposition 10.** Let $\varphi \in \mathcal{L}_{bool}(OA)$ and $s \in W^{EL-O}$. Then $s \models \varphi$ iff $M^{EL-O}, s \models \varphi$.

*Proof.* The proof is by induction on the structure of $\varphi$. The only interesting case is the base case of atoms $\alpha \in OA$. We use induction on the length of $\alpha$. When $\alpha = p$ then $M, s \models p$ iff $s \models p$ for any $s \in W^{EL-O}$ by definition of $V^{EL-O}$. When $\alpha = S_i\beta$ we prove the two directions of the equivalence.

* If $s \models S_i\beta$ for some $\beta \in OA$ and some $s \in W^{EL-O}$: consider $s' \in W^{EL-O}$ such that $s \sim_i^{EL-O} s'$. By definition of $\sim_i^{EL-O}$, $s$ and $s'$ agree on all $\alpha$ such that $s \models S_i\alpha$. Therefore if $s \models \beta$ then $s' \models \beta$, and by the induction hypothesis, $M^{EL-O}, s' \models \beta$; hence $M^{EL-O}, s \models K_i\beta$. If $s \models \neg\beta$, by the same argument, we have that $M^{EL-O}, s \models K_i\neg\beta$. Therefore $M^{EL-O}, s \models S_i\beta$.

* If $M^{EL-O}, s \models S_i\beta$ for some $\beta \in OA$ and some $s \in W^{EL-O}$, then either $M^{EL-O}, s \models K_i\beta$ or $M^{EL-O}, s \models K_i\neg\beta$. Suppose that $s \not\models S_i\beta$. In particular $\beta \notin I-OA$. If $s \models \beta$, consider $s' = s \setminus \beta^=$, and if $s \not\models \beta$, consider $s' = s \cup \beta^=$. In both cases $s' \in W^{EL-O}$, and $s$ and $s'$ agree on all $\alpha$ such that $s \models S_i\alpha$. Therefore $s \sim_i^{EL-O} s'$, but by the induction hypothesis, $M^{EL-O}, s' \models \beta$ iff $s' \models \beta$ iff $s' \models \neg\beta$ iff $M^{EL-O}, s \models \neg\beta$: this contradicts the hypothesis that $M^{EL-O}, s \models S_i\beta$.

For the case $\alpha = JS\beta$ we proceed similarly. $\square$

### 4.3. Completeness of the EL-O fragment of $\mathcal{L}_{EL}$ w.r.t. S5 validity

We now show that the EL-O semantics in terms of observability and the standard Kripke semantics have the same validities as far as the EL-O fragment is concerned.
**Proposition 11.** Let $\varphi \in \mathcal{L}_{\text{bool}}(\text{OA})$ be a formula. Then $\varphi$ is valid in the S5 Kripke models of Section 4.2 iff $\varphi$ is provable in CPC from the EL-O axioms of Table 1.

475

*Proof.* For soundness we show that the schemas $S_i, S_i \alpha, JS, JS \alpha, JS, S_i, S_i \alpha, JS \alpha \to S_i \alpha, JS \alpha \to JS, S_i \alpha$ are valid in S5 Kripke models. For the first it suffices to observe that $S_i, S_i \alpha$ is equivalent to $K_i(K_i \alpha \lor K_i \neg \alpha) \lor K_i \neg (K_i \alpha \lor K_i \neg \alpha)$. The latter is equivalent in S5 to the propositionally valid $K_i \alpha \lor K_i \neg \alpha \lor \neg (K_i \alpha \lor K_i \neg \alpha)$. Validity of the other axiom schemas can be proved in a similar manner.

480

For completeness suppose that $\varphi$ is not provable from the EL-O axioms. By Proposition 8 there exists $s \subseteq \text{OA}$ such that $s \not\models \varphi$. Hence $s \models \bigcup \text{OA} \not\models^{\text{CPC}} \varphi$ by Proposition 6 and, as $s \models \bigcup \text{OA} \in W^{\text{EL-O}}, M^{\text{EL-O}}, s \models \bigcup \text{OA} \not\models \varphi$ by Proposition 10. Hence $\varphi$ cannot be valid in S5 Kripke models. $\square$

485

## 4.4. Axiomatisation of the $M^{\text{EL-O}}$ validities in $\mathcal{L}_{\text{EL}}$

It follows from Proposition 11 that in order to check satisfiability in S5 Kripke models of a formula in the EL-O fragment it suffices to take the canonical Kripke model $M^{\text{EL-O}}$ and go through its states. In other words, there is no formula in the EL-O fragment that is valid in $M^{\text{EL-O}}$ without being valid in the set of all S5 Kripke models. This fails to hold for the full language $\mathcal{L}_{\text{EL}}$. This can be seen from the axiomatisation of the $\mathcal{L}_{\text{EL}}$ validities in $M^{\text{EL-O}}$ of [43] and [9, Chapter 2].<fnref n="2" /> It is made up of: the EL-O axioms of Table 1; the axioms

$$K_i \alpha \leftrightarrow \alpha \wedge S_i \alpha,$$

$$K_i \neg \alpha \leftrightarrow \neg \alpha \wedge S_i \alpha,$$

$$CK \alpha \leftrightarrow \alpha \wedge JS \alpha,$$

$$CK \neg \alpha \leftrightarrow \neg \alpha \wedge JS \alpha$$

<footnote n="2">²Our semantics differs from the semantics in these papers in that it is finitary. The only thing that changes is the soundness proof, which is routine.</footnote>
**Proposition 11.** Let $\varphi \in \mathcal{L}_{\mathbf{bool}}(\mathbf{OA})$ be a formula. Then $\varphi$ is valid in the S5 Kripke models of Section 4.2 iff $\varphi$ is provable in CPC from the EL-O axioms of Table 1.

475

*Proof.* For soundness we show that the schemas $S_i \ S_i \alpha$, $JS \ S \alpha$, $JS \ S_i \ S_i \alpha$, $JS \ \alpha \to S_i \ \alpha$, $JS \ \alpha \to JS \ S_i \ \alpha$ are valid in S5 Kripke models. For the first it suffices to observe that $S_i \ S_i \ \alpha$ is equivalent to $K_i(K_i \alpha \lor K_i \neg \alpha) \lor K_i \neg (K_i \alpha \lor K_i \neg \alpha)$. The latter is equivalent in S5 to the propositionally valid $K_i \alpha \lor K_i \neg \alpha \lor \neg (K_i \alpha \lor K_i \neg \alpha)$. Validity of the other axiom schemas can be proved in a similar manner.

480

For completeness suppose that $\varphi$ is not provable from the EL-O axioms. By Proposition 8 there exists $s \subseteq \mathbf{OA}$ such that $s \not\models \varphi$. Hence $s \models \bigcup \mathbf{OA} \not\models^{\mathrm{CPC}} \varphi$ by Proposition 6 and, as $s \models \bigcup \mathbf{OA} \in W^{\mathrm{EL-O}}$, $M^{\mathrm{EL-O}}$, $s \models \bigcup \mathbf{OA} \not\models \varphi$ by Proposition 10. Hence $\varphi$ cannot be valid in S5 Kripke models. $\square$

485

**4.4. Axiomatisation of the $M^{\mathrm{EL-O}}$ validities in $\mathcal{L}_{\mathrm{EL}}$**

It follows from Proposition 11 that in order to check satisfiability in S5 Kripke models of a formula in the EL-O fragment it suffices to take the canonical Kripke model $M^{\mathrm{EL-O}}$ and go through its states. In other words, there is no formula in the EL-O fragment that is valid in $M^{\mathrm{EL-O}}$ without being valid in the set of all S5 Kripke models. This fails to hold for the full language $\mathcal{L}_{\mathrm{EL}}$. This can be seen from the axiomatisation of the $\mathcal{L}_{\mathrm{EL}}$ validities in $M^{\mathrm{EL-O}}$ of [43] and [9, Chapter 2].<fnref n="2" /> It is made up of: the EL-O axioms of Table 1; the axioms

$$K_i \alpha \leftrightarrow \alpha \wedge S_i \alpha,$$

$$K_i \neg \alpha \leftrightarrow \neg \alpha \wedge S_i \alpha,$$

$$CK \alpha \leftrightarrow \alpha \wedge JS \alpha,$$

$$CK \neg \alpha \leftrightarrow \neg \alpha \wedge JS \alpha$$

<footnote n="2">²Our semantics differs from the semantics in these papers in that it is finitary. The only thing that changes is the soundness proof, which is routine.</footnote>
relating $K_i$ to $S_i$ and CK to JS; all S5 principles for $K_i$ and CK; plus two
axioms distributing $K_i$ and CK over clauses:

$$
K_i(\bigvee_{\alpha \in A^+} \alpha \vee \bigvee_{\alpha \in A^-} \neg \alpha) \leftrightarrow \left\{ \begin{array}{l} (\bigvee_{\alpha \in A^+} K_i \alpha) \vee (\bigvee_{\alpha \in A^-} K_i \neg \alpha) \quad \text{if } (A^+)^{\equiv} \cap A^- = \emptyset, \\ \top \quad \text{otherwise;} \end{array} \right.
$$

$$
CK(\bigvee_{\alpha \in A^+} \alpha \vee \bigvee_{\alpha \in A^-} \neg \alpha) \leftrightarrow \left\{ \begin{array}{l} (\bigvee_{\alpha \in A^+} CK\alpha) \vee (\bigvee_{\alpha \in A^-} CK\neg\alpha) \quad \text{if } (A^+)^{\equiv} \cap A^- = \emptyset, \\ \top \quad \text{otherwise.} \end{array} \right.
$$

The last two axioms resort to a generalisation of the ‘caused-by’ function
from atoms to sets of atoms $A \subseteq \text{OA}$, in the obvious way: $A^{\equiv} = \bigcup_{\alpha \in A} \alpha^{\equiv}$.
They are specific to observability-based knowledge and are typically invalid
in normal modal logics. An instance of the first one is $K_i(p \lor q) \leftrightarrow (K_i p \lor K_i q)$,
for different $p$ and $q$. This is a strong principle: to give an example, if it
is known that the butler or the gardener was the murderer then it is also
known who of them it was. The reason is that our logic is built on atomic ob-
servability information: what is modelled in $M^{\text{EL-O}}$ are forms of individual
and common knowledge that are respectively obtained via individual ob-
servation and joint observation of facts. This differs conceptually from the
classical operators of individual and common knowledge as studied in epis-
temic logic [12]. The property of distribution over falsifiable disjunctions
of literals is common in epistemic logics that are based on observability of
propositional variables. It is shown in [29] that it can be avoided if one
introduces new propositional variables.

The axiomatics allows us to reduce every $\mathcal{L}_{\text{EL}}$ formula to an equivalent
$\mathcal{L}_{\text{bool}}(\text{OA})$ formula. For example, positive introspection $K_i p \rightarrow K_i K_i p$ reduces
to $(p \wedge S_i p) \rightarrow (p \wedge S_i p \wedge S_i S_i p)$. Observe that the latter is EL-O valid.

5. Epistemic planning with conditional effects

We now define actions and planning tasks within our framework. We
assume deterministic actions with conditional effects whose preconditions
relating $K_i$ to $S_i$ and CK to JS; all S5 principles for $K_i$ and CK; plus two
axioms distributing $K_i$ and CK over clauses:

$$
K_i(\bigvee_{\alpha \in A^+} \alpha \vee \bigvee_{\alpha \in A^-} \neg \alpha) \leftrightarrow \begin{cases} (\bigvee_{\alpha \in A^+} K_i \alpha) \vee (\bigvee_{\alpha \in A^-} K_i \neg \alpha) & \text{if } (A^+)^{\equiv} \cap A^- = \emptyset, \\ \top & \text{otherwise;} \end{cases}
$$

$$
CK(\bigvee_{\alpha \in A^+} \alpha \vee \bigvee_{\alpha \in A^-} \neg \alpha) \leftrightarrow \begin{cases} (\bigvee_{\alpha \in A^+} CK\alpha) \vee (\bigvee_{\alpha \in A^-} CK\neg\alpha) & \text{if } (A^+)^{\equiv} \cap A^- = \emptyset, \\ \top & \text{otherwise.} \end{cases}
$$

The last two axioms resort to a generalisation of the ‘caused-by’ function
from atoms to sets of atoms $A \subseteq \text{OA}$, in the obvious way: $A^{\equiv} = \bigcup_{\alpha \in A} \alpha^{\equiv}$.
They are specific to observability-based knowledge and are typically invalid
in normal modal logics. An instance of the first one is $K_i(p \lor q) \leftrightarrow (K_i p \lor K_i q)$,
for different $p$ and $q$. This is a strong principle: to give an example, if it
is known that the butler or the gardener was the murderer then it is also
known who of them it was. The reason is that our logic is built on atomic ob-
servability information: what is modelled in $M^{\text{EL-O}}$ are forms of individual
and common knowledge that are respectively obtained via individual ob-
servation and joint observation of facts. This differs conceptually from the
classical operators of individual and common knowledge as studied in epis-
temic logic [12]. The property of distribution over falsifiable disjunctions
of literals is common in epistemic logics that are based on observability of
propositional variables. It is shown in [29] that it can be avoided if one
introduces new propositional variables.

The axiomatics allows us to reduce every $\mathcal{L}_{\text{EL}}$ formula to an equivalent
$\mathcal{L}_{\text{bool}}(\text{OA})$ formula. For example, positive introspection $K_i p \rightarrow K_i K_i p$ reduces
to $(p \wedge S_i p) \rightarrow (p \wedge S_i p \wedge S_i S_i p)$. Observe that the latter is EL-O valid.

5. Epistemic planning with conditional effects

We now define actions and planning tasks within our framework. We
assume deterministic actions with conditional effects whose preconditions
are described by EL-O formulas and whose positive and negative effects are sets of observability atoms. We have already argued in Section 2 that conditional effects are important in epistemic planning: the effects of an action on agent i's epistemic state typically depend on whether i sees the variables that are modified by the action or not.

510

We start by defining classical planning tasks [44] and then introduce our simple epistemic planning tasks. The name 'simple' will be justified by our translation to classical planning of Section 5.5.

515

## 5.1. Action descriptions and planning tasks

Just as for the definition of boolean formulas in Section 3.1, we consider an abstract vocabulary $V$ with which actions are described. An action description over $V$ (or action for short) is a pair $a = \langle pre(a), eff(a) \rangle$ where $pre(a) \in \mathcal{L}_{bool}(V)$ and $eff(a) \subseteq \mathcal{L}_{bool}(V) \times 2^V \times 2^V$. The formula $pre(a)$ is the pre-condition of a, describing when the action may be applied, and $eff(a)$ are the conditional effects of a, describing which atomic formulas the action may add or remove from the current state under additional conditions. For each conditional effect

$$ce = \langle \mathrm{cnd}(ce), \mathrm{ceff}^{+}(ce), \mathrm{ceff}^{-}(ce) \rangle$$

in $eff(a)$, $cnd(ce)$ is the condition of $ce$, $ceff^{+}(ce)$ are the added and $ceff^{-}(ce)$ are the deleted atomic formulas. The vocabulary and the length of an action description are defined by:

$$\mathrm{Voc}(a) = \mathrm{Voc}(pre(a)) \cup \bigcup_{ce \in eff(a)} (\mathrm{Voc}(cnd(ce)) \cup ceff^{+}(ce) \cup ceff^{-}(ce));$$

$$\ell(a) = \ell(pre(a)) + \sum_{ce \in eff(a)} \left( \ell(cnd(ce)) + \left( \sum_{p \in ceff^{+}(ce)} \ell(p) \right) + \left( \sum_{p \in ceff^{-}(ce)} \ell(p) \right) \right).$$

Remember that each $p \in V$ has its length $\ell(p) \ge 1$, for some integer.

A planning task over $V$ is a tuple $\mathcal{P} = \langle V, \mathrm{Act}, s_0, \mathrm{Goal} \rangle$ where $V$ is some vocabulary, $\mathrm{Act}$ is a set of action descriptions, $s_0 \in 2^V$ is the initial state, and
are described by EL-O formulas and whose positive and negative effects are sets of observability atoms. We have already argued in Section 2 that conditional effects are important in epistemic planning: the effects of an action on agent i's epistemic state typically depend on whether i sees the variables that are modified by the action or not.

We start by defining classical planning tasks [44] and then introduce our simple epistemic planning tasks. The name ‘simple’ will be justified by our translation to classical planning of Section 5.5.

510

515

## 5.1. Action descriptions and planning tasks

Just as for the definition of boolean formulas in Section 3.1, we consider an abstract vocabulary $V$ with which actions are described. An action description over $V$ (or action for short) is a pair $a = \langle pre(a), eff(a) \rangle$ where $pre(a) \in \mathcal{L}_{bool}(V)$ and $eff(a) \subseteq \mathcal{L}_{bool}(V) \times 2^V \times 2^V$. The formula $pre(a)$ is the pre-condition of $a$, describing when the action may be applied, and $eff(a)$ are the conditional effects of $a$, describing which atomic formulas the action may add or remove from the current state under additional conditions. For each conditional effect

$$ce = \langle \text{cnd}(ce), \text{ceff}^{+}(ce), \text{ceff}^{-}(ce) \rangle$$

in $eff(a)$, $cnd(ce)$ is the condition of $ce$, $ceff^{+}(ce)$ are the added and $ceff^{-}(ce)$ are the deleted atomic formulas. The vocabulary and the length of an action description are defined by:

$$\mathrm{Voc}(a) = \mathrm{Voc}(pre(a)) \cup \bigcup_{ce \in eff(a)} (\mathrm{Voc}(cnd(ce)) \cup ceff^{+}(ce) \cup ceff^{-}(ce));$$

$$\ell(a) = \ell(pre(a)) + \sum_{ce \in eff(a)} \left( \ell(cnd(ce)) + \left( \sum_{p \in ceff^{+}(ce)} \ell(p) \right) + \left( \sum_{p \in ceff^{-}(ce)} \ell(p) \right) \right).$$

Remember that each $p \in V$ has its length $\ell(p) \ge 1$, for some integer.

A planning task over $V$ is a tuple $\mathcal{P} = \langle V, \mathcal{Act}, s_0, \mathcal{Goal} \rangle$ where $V$ is some vocabulary, $\mathcal{Act}$ is a set of action descriptions, $s_0 \in 2^V$ is the initial state, and
Goal ∈ L$_{bool}$ (V) is the goal formula. Its relevant vocabulary and length are:

$$
\mathrm{Voc}(\mathcal{P}) = \left( \bigcup_{a \in \mathrm{Act}} \mathrm{Voc}(a) \right) \cup s_0 \cup \mathrm{Voc}(\mathrm{Goal});
$$

$$
\ell(\mathcal{P}) = |s_0| + \ell(\text{Goal}) + \sum_{a \in \text{Act}} \ell(a).
$$

The solutions of a planning task depend on the interpretation of formu-
las and actions. We have already seen the classical EL-O interpretation
of formulas (Section 3.1) and the EL-O interpretation of formulas (Section
3.4). As to actions, we are going to define their classical and their EL-O
interpretation. Both are relations on the set of states 2$^V$. Given some set of
action-interpreting relations $\mathcal{R}$, we say that the state $s$ is reachable from the
state $s_0$ via $\mathcal{R}$ if there exists an integer $m \ge 0$, a sequence of states $t_0, \dots, t_m$
from $2^V$, and a sequence of relations $R_1, \dots, R_m$ from $\mathcal{R}$ such that $s_0 = t_0$,
$s = t_m$, and $t_{k-1} R_k t_k$ for every $k$ such that $1 \le k \le m$. Solvability of a planning
task amounts to reachability of a state satisfying the goal from the initial
state $s_0$ via the relations interpreting the actions.

5.2. *Classical planning*

When an action description a has a precondition and two (not neces-
sarily different) conditional effects whose preconditions are jointly satis-
fiable with pre(a) then there is a conflict. The other way round, we say
that a is classically consistent if and only if for every ce₁, ce₂ ∈ eff(a), if
pre(a) ∧ cnd(ce₁) ∧ cnd(ce₂) is CPC satisfiable then ceff⁺(ce₁) and ceff⁻(ce₂) are
disjoint.

**Example 5.** For an example of inconsistency consider the following de-
scription of the action swap<sub>p,q</sub> swapping the truth values of *p* and *q*. Suppose
this action can always be executed, so its precondition is pre(swap<sub>p,q</sub>) = ⊤,
and suppose its conditional effects are naively described by eff(swap<sub>p,q</sub>) =
{⟨*p*, {*q*}, {*p*}⟩, ⟨*q*}, {*p*}, {*q*}⟩}.
These two conditional effects conflict because ⊤ ∧ *p* ∧ *q*
is CPC-satisfiable. Observe that we can make the description classically
Goal ∈ L$_{bool}$ (V) is the goal formula. Its relevant vocabulary and length are:

$$
\mathrm{Voc}(\mathcal{P}) = \left( \bigcup_{a \in \mathrm{Act}} \mathrm{Voc}(a) \right) \cup s_0 \cup \mathrm{Voc}(\mathrm{Goal});
$$

$$
\ell(\mathcal{P}) = |s_0| + \ell(\mathit{Goal}) + \sum_{a \in \mathit{Act}} \ell(a).
$$

The solutions of a planning task depend on the interpretation of formu-
las and actions. We have already seen the classical EL-O interpretation
of formulas (Section 3.1) and the EL-O interpretation of formulas (Section
3.4). As to actions, we are going to define their classical and their EL-O
interpretation. Both are relations on the set of states 2$^V$. Given some set of
action-interpreting relations $\mathcal{R}$, we say that the state $s$ is reachable from the
state $s_0$ via $\mathcal{R}$ if there exists an integer $m \ge 0$, a sequence of states $t_0, \dots, t_m$
from $2^V$, and a sequence of relations $R_1, \dots, R_m$ from $\mathcal{R}$ such that $s_0 = t_0$,
$s = t_m$, and $t_{k-1} R_k t_k$ for every $k$ such that $1 \le k \le m$. Solvability of a planning
task amounts to reachability of a state satisfying the goal from the initial
state $s_0$ via the relations interpreting the actions.

5.2. *Classical planning*

When an action description a has a precondition and two (not neces-
sarily different) conditional effects whose preconditions are jointly satis-
fiable with pre(a) then there is a conflict. The other way round, we say
that a is classically consistent if and only if for every ce₁, ce₂ ∈ eff(a), if
pre(a) ∧ cnd(ce₁) ∧ cnd(ce₂) is CPC satisfiable then ceff⁺(ce₁) and ceff⁻(ce₂) are
disjoint.

**Example 5.** For an example of inconsistency consider the following de-
scription of the action swap<sub>p,q</sub> swapping the truth values of *p* and *q*. Suppose
this action can always be executed, so its precondition is pre(swap<sub>p,q</sub>) = ⊤,
and suppose its conditional effects are naively described by eff(swap<sub>p,q</sub>) =
{⟨*p*, {*q*}, {*p*}⟩, ⟨*q*}, {*p*}, {*q*}⟩}. These two conditional effects conflict because ⊤ ∧ *p* ∧ *q*
is CPC-satisfiable. Observe that we can make the description classically
consistent by replacing the precondition by $\neg(p \leftrightarrow q)$: the action is executable only if the truth values of $p$ and $q$ differ.

A classically consistent action description determines the following relation on the set of states $2^V$:

$$sR_a^{CPC}s' \quad \text{iff} \quad s \models^{CPC} \text{pre}(a) \text{ and } s' = \left( s \setminus \bigcup_{\substack{ce \in \text{eff}(a), \\ s \models^{CPC} \text{cnd}(ce)}} \text{ceff}^{-}(ce) \right) \cup \left( \bigcup_{\substack{ce \in \text{eff}(a), \\ s \models^{CPC} \text{cnd}(ce)}} \text{ceff}^{+}(ce) \right).$$

A planning task is *classically solvable* if a state satisfying the goal formula is reachable from the initial state via $\{R_a^{CPC} : a \in \text{Act}\}$, i.e., via the CPC-interpretation of the actions in *Act*. It is known that classical solvability of a planning task is a PSPACE-complete reasoning problem [14].

### 5.3. EL-O consistent action descriptions

In order to describe epistemic preconditions and effects we instantiate the vocabulary $V$ by the set of observability atoms OA. An action description $a = \langle \text{pre}(a), \text{eff}(a) \rangle$ over OA is EL-O consistent if and only if

1. for every $ce \in \text{eff}(a)$, $\text{ceff}^{-}(ce)$ contains no introspective atoms;

2. for every $ce_1, ce_2 \in \text{eff}(a)$, if $\text{pre}(a) \wedge \text{cnd}(ce_1) \wedge \text{cnd}(ce_2)$ is satisfiable in EL-O then $\text{ceff}^{+}(ce_1)$ and $(\text{ceff}^{-}(ce_2))^{=}$ are disjoint.

Proposition 3 provides formal support to these two conditions. Let us explain the intuitions behind them. The first is clear: it makes no sense to delete introspective atoms. The second condition requires that two conditional effects of an action cannot conflict when $\text{pre}(a)$ and their triggering conditions are jointly satisfiable. Hence when an action $a$ has conditional effects $ce_1, ce_2 \in \text{eff}(a)$ and there are $\alpha_1 \in \text{ceff}^{+}(ce_1)$ and $\alpha_2 \in \text{ceff}^{-}(ce_2)$ such that $\alpha_1 \Rightarrow \alpha_2$ then $\text{pre}(a) \wedge \text{cnd}(ce_1) \wedge \text{cnd}(ce_2)$ must be inconsistent. Note that it follows from the transitivity of introspective consequence $\Rightarrow$ that $\text{ceff}^{+}(ce_1)$ and $(\text{ceff}^{-}(ce_2))^{=}$ are disjoint iff $\text{ceff}^{+}(ce_1) \Rightarrow$ and $(\text{ceff}^{-}(ce_2))^{=}$ are.

**Example 6.** The action flip of flipping a light switch is described by $\text{pre}(\text{flip}) = \top$ and $\text{eff}(\text{flip}) = \{\langle \text{On}, \emptyset, \{\text{On}\} \rangle, \langle \neg \text{On}, \{\text{On}\}, \emptyset \rangle\}$. It is EL-O consistent: first, none
consistent by replacing the precondition by $\neg(p \leftrightarrow q)$: the action is executable only if the truth values of $p$ and $q$ differ.

A classically consistent action description determines the following relation on the set of states $2^V$:

$$sR_a^{\text{CPC}} s' \text{ iff } s \models^{\text{CPC}} \text{pre}(a) \text{ and } s' = \left( s \setminus \bigcup_{\substack{ce \in \text{eff}(a), \\ s \models^{\text{CPC}} \text{cnd}(ce)}} \text{ceff}^{-}(ce) \right) \cup \left( \bigcup_{\substack{ce \in \text{eff}(a), \\ s \models^{\text{CPC}} \text{cnd}(ce)}} \text{ceff}^{+}(ce) \right).$$

A planning task is *classically solvable* if a state satisfying the goal formula is reachable from the initial state via $\{R_a^{\text{CPC}} : a \in \text{Act}\}$, i.e., via the CPC-interpretation of the actions in *Act*. It is known that classical solvability of a planning task is a PSPACE-complete reasoning problem [14].

### 5.3. EL-O consistent action descriptions

In order to describe epistemic preconditions and effects we instantiate the vocabulary $V$ by the set of observability atoms OA. An action description $a = \langle \text{pre}(a), \text{eff}(a) \rangle$ over OA is EL-O consistent if and only if

1. for every $ce \in \text{eff}(a)$, $\text{ceff}^{-}(ce)$ contains no introspective atoms;

2. for every $ce_1, ce_2 \in \text{eff}(a)$, if $\text{pre}(a) \wedge \text{cnd}(ce_1) \wedge \text{cnd}(ce_2)$ is satisfiable in EL-O then $\text{ceff}^{+}(ce_1)$ and $(\text{ceff}^{-}(ce_2))^{=} \text{ are disjoint.}$

Proposition 3 provides formal support to these two conditions. Let us explain the intuitions behind them. The first is clear: it makes no sense to delete introspective atoms. The second condition requires that two conditional effects of an action cannot conflict when $\text{pre}(a)$ and their triggering conditions are jointly satisfiable. Hence when an action $a$ has conditional effects $ce_1, ce_2 \in \text{eff}(a)$ and there are $\alpha_1 \in \text{ceff}^{+}(ce_1)$ and $\alpha_2 \in \text{ceff}^{-}(ce_2)$ such that $\alpha_1 \Rightarrow \alpha_2$ then $\text{pre}(a) \wedge \text{cnd}(ce_1) \wedge \text{cnd}(ce_2)$ must be inconsistent. Note that it follows from the transitivity of introspective consequence $\Rightarrow$ that $\text{ceff}^{+}(ce_1)$ and $(\text{ceff}^{-}(ce_2))^{=} \text{ are disjoint iff } \text{ceff}^{+}(ce_1) \Rightarrow \text{ and } (\text{ceff}^{-}(ce_2))^{=} \text{ are.}$

**Example 6.** The action flip of flipping a light switch is described by $\text{pre}(\text{flip}) = \top$ and $\text{eff}(\text{flip}) = \{\langle \text{On}, \emptyset, \{\text{On}\} \rangle, \langle \neg\text{On}, \{\text{On}\}, \emptyset \rangle\}$. It is EL-O consistent: first, none
of the negative effects is an introspective atom, and second, although there are two conditional effects with contradictory add- and delete-lists, there can be no conflict because the conjunction $\top \wedge \text{On} \wedge \neg \text{On}$ of the precondition and the conditions of the two conditional effects is unsatisfiable.

**Example 7.** Let us describe calls in the original gossip problem where the goal is to obtain shared knowledge of depth $k = 1$. Suppose OA is built from $\mathbf{A} = \{1, \dots, n\}$ and $\mathbf{P} = \{s_i : i \in \mathbf{A}\}$. During the action $\text{call}_j^i$, in which a call is made between agents $i$ and $j$ (this action being symmetrical), the two agents tell each other every secret they know among all $n$ secrets. We have $\text{call}_j^i = \langle \text{pre}(\text{call}_j^i), \text{eff}(\text{call}_j^i) \rangle$ with $\text{pre}(\text{call}_j^i) = \top$ and:

$$ \begin{align*} \text{eff}(\text{call}_j^i) &= \{ \langle S_i s_1 \lor S_j s_1, \{S_i s_1, S_j s_1\}, \emptyset \rangle, \\ &\dots, \\ &\langle S_i s_n \lor S_j s_n, \{S_i s_n, S_j s_n\}, \emptyset \rangle \}. \end{align*} $$

Intuitively, a secret becomes observable for both agents if at least one of them observes it. Each $\text{call}_j^i$ is EL-O consistent because it has no negative effects. The length of a call is $\ell(\text{call}_j^i) = 5+(|\mathbf{A}|\times(8+4+0)) = 12n+5$. (Remember that disjunctions $S_i s_k \lor S_j s_k$ abbreviate $\neg(\neg S_i s_1 \wedge \neg S_j s_1)$.)

Here is a more complex example of a consistent action.

**Example 8.** Consider the action pour of pouring a bottle of liquid on a healthy lawn [45]. Factually, its effect is that if the liquid is poisonous the lawn becomes dead. Epistemically, pour has several conditional effects: (1) if $i$ knows that Poisonous then $i$ will know that the lawn is dead; (2) if $i$ does not know whether Poisonous and if the lawn is known to be healthy<fnref n="3" /> then $i$ will no longer know whether the lawn is healthy or dead. (There is a third possible epistemic situation where $i$ knows that $\neg$Poisonous, but we

<footnote n="3">³In [45], the condition of the last effect is only that it is not known *that* $\neg$Poisonous, and the effect is that it is no longer known *that* $\neg$Dead. This however produces an unintuitive result in states where the liquid is known to be poisonous.</footnote>
of the negative effects is an introspective atom, and second, although there are two conditional effects with contradictory add- and delete-lists, there can be no conflict because the conjunction $\top \wedge \text{On} \wedge \neg \text{On}$ of the precondition and the conditions of the two conditional effects is unsatisfiable.

**Example 7.** Let us describe calls in the original gossip problem where the goal is to obtain shared knowledge of depth $k = 1$. Suppose OA is built from $A = \{1, \dots, n\}$ and $P = \{s_i : i \in A\}$. During the action $call_j^i$, in which a call is made between agents $i$ and $j$ (this action being symmetrical), the two agents tell each other every secret they know among all $n$ secrets. We have $call_j^i = \langle \text{pre}(call_j^i), \text{eff}(call_j^i) \rangle$ with $\text{pre}(call_j^i) = \top$ and:

$$ \begin{align*} \text{eff}(\text{call}_j^i) &= \{ \langle S_i s_1 \lor S_j s_1, \{S_i s_1, S_j s_1\}, \emptyset \rangle, \\ &\dots, \\ &\langle S_i s_n \lor S_j s_n, \{S_i s_n, S_j s_n\}, \emptyset \rangle \}. \end{align*} $$

Intuitively, a secret becomes observable for both agents if at least one of them observes it. Each $call_j^i$ is EL-O consistent because it has no negative effects. The length of a call is $\ell(\text{call}_j^i) = 5+(|A|(8+4+0)) = 12n+5$. (Remember that disjunctions $S_i s_k \lor S_j s_k$ abbreviate $\neg(\neg S_i s_1 \wedge \neg S_j s_1)$.)

Here is a more complex example of a consistent action.

**Example 8.** Consider the action pour of pouring a bottle of liquid on a healthy lawn [45]. Factually, its effect is that if the liquid is poisonous the lawn becomes dead. Epistemically, pour has several conditional effects: (1) if $i$ knows that Poisonous then $i$ will know that the lawn is dead; (2) if $i$ does not know whether Poisonous and if the lawn is known to be healthy<fnref n="3" /> then $i$ will no longer know whether the lawn is healthy or dead. (There is a third possible epistemic situation where $i$ knows that $\neg$Poisonous, but we

<footnote n="3">³In [45], the condition of the last effect is only that it is not known *that* $\neg$Poisonous, and the effect is that it is no longer known *that* $\neg$Dead. This however produces an unintuitive result in states where the liquid is known to be poisonous.</footnote>
need not say anything here because there is no effect as far as the status
of Dead is concerned.) Consider the description of pour with precondition
pre(pour) = ⊤ and effect

$$
\begin{align*}
eff(\text{pour}) ={}& \langle \text{Poisonous}, \{\text{Dead}\}, \emptyset \rangle, \\
& \langle \text{Poisonous} \wedge S_i \text{ Poisonous}, \{S_i \text{ Dead}\}, \emptyset \rangle, \\
& \langle \neg S_i \text{ Poisonous} \wedge \neg \text{Dead} \wedge S_i \text{ Dead}, \emptyset, \{S_i \text{ Dead}\} \rangle.
\end{align*}
$$

The first conditional effect is factual and the last two are epistemic. The
second represents (1): Poisonous ∧ S<sub>i</sub> Poisonous expresses that *i* knows that
the liquid is poisonous; and the third represents (2): ¬Dead ∧ S<sub>i</sub> Dead ex-
presses that *i* knows that the lawn is healthy. This action description is EL-
O consistent in particular because the conjunction of the two last conditions
Poisonous ∧ S<sub>i</sub> Poisonous and ¬S<sub>i</sub> Poisonous ∧ ¬Dead ∧ S<sub>i</sub> Dead is inconsistent.

5.4. Simple epistemic planning tasks

Every EL-O consistent action determines a relation $R_a^{\text{EL-O}}$ between states that is a partial function: for every $s, s' \in 2^{\text{OA}}$,

$$
s R_a^{\text{EL-O}} s' \quad \text{iff} \quad s \models \text{pre}(a) \text{ and } s' = \left( s \setminus \bigcup_{\substack{ce \in \text{eff}(a), \\ s \models \text{cnd}(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in \text{eff}(a), \\ s \models \text{cnd}(ce)}} (ceff^{+}(ce)) \right) \Rightarrow .
$$

That is, if its precondition is satisfied then an action

• removes negative effects of firing conditional effects, plus their causes;

• adds positive effects of firing conditional effects, plus their consequences.

Thanks to EL-O consistency the order of removals and additions does not
matter. Moreover, if we start from an introspectively closed state in *I-STATES*
then the resulting state is also introspectively closed.

A *simple epistemic planning task* is a planning task over some subset of the set of observability atoms OA. It is EL-O *solvable* iff there is a state *s* such that *s* ⊨ *Goal* that is reachable from *s* ⇝ 0 ∪ I-OA via the EL-O-interpretation of the actions in *Act*, i.e., via {*R*<sub>a</sub><sup>EL-O</sup> : a ∈ *Act*}.
need not say anything here because there is no effect as far as the status of Dead is concerned.) Consider the description of pour with precondition $pre(pour) = \top$ and effect

$$ \begin{aligned} \mathit{eff}(pour) = & \{\langle\mathit{Poisonous}, \{\mathit{Dead}\}, \emptyset\rangle, \\ & \langle\mathit{Poisonous} \wedge \mathit{S}_i \mathit{Poisonous}, \{\mathit{S}_i \mathit{Dead}\}, \emptyset\rangle, \\ & \langle\neg \mathit{S}_i \mathit{Poisonous} \wedge \neg \mathit{Dead} \wedge \mathit{S}_i \mathit{Dead}, \emptyset, \{\mathit{S}_i \mathit{Dead}\}\rangle\}. \end{aligned} $$

The first conditional effect is factual and the last two are epistemic. The second represents (1): Poisonous $\wedge \mathit{S}_i$ Poisonous expresses that $i$ knows that the liquid is poisonous; and the third represents (2): $\neg \mathit{Dead} \wedge \mathit{S}_i$ Dead expresses that $i$ knows that the lawn is healthy. This action description is EL-O consistent in particular because the conjunction of the two last conditions Poisonous $\wedge \mathit{S}_i$ Poisonous and $\neg \mathit{S}_i$ Poisonous $\wedge \neg \mathit{Dead} \wedge \mathit{S}_i$ Dead is inconsistent.

### 5.4. Simple epistemic planning tasks

Every EL-O consistent action determines a relation $R_a^{EL-O}$ between states that is a partial function: for every $s, s' \in 2^{OA}$,

$$ s R_a^{EL-O} s' \quad \text{iff} \quad s \models pre(a) \text{ and } s' = \left( s \setminus \bigcup_{\substack{ce \in eff(a), \\ s \models cnd(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in eff(a), \\ s \models cnd(ce)}} (ceff^{+}(ce)) \right). $$

That is, if its precondition is satisfied then an action

* removes negative effects of firing conditional effects, plus their causes;

* adds positive effects of firing conditional effects, plus their consequences.

Thanks to EL-O consistency the order of removals and additions does not matter. Moreover, if we start from an introspectively closed state in I-STATES then the resulting state is also introspectively closed.

A simple epistemic planning task is a planning task over some subset of the set of observability atoms OA. It is EL-O *solvable* iff there is a state *s* such that *s* $\models$ *Goal* that is reachable from $s \stackrel{\rightarrow}{\rightarrow} 0 \cup I$-OA via the EL-O-interpretation of the actions in *Act*, i.e., via $\{R_a^{EL-O} : a \in Act\}$.
**Example 9.** The planning task corresponding to the original gossip problem is $G_1 = \langle OA, Act^{G_1}, s_0^{G_1}, Goal^{G_1} \rangle$ with

$$Act^{G_1} = \{\text{call}_j^i : i, j \in A \text{ and } i \neq j\},$$

$$s_0^{G_1} = \{S_i s_i : i \in A\} \cup S \text{ for some } S \subseteq \{s_i : i \in A\},$$

$$Goal^{G_1} = \bigwedge_{i, j \in A} S_i s_j.$$

It can be solved via $2n - 4$ calls; when $n \ge 4$ then there is no EL-O solution that takes less calls [46, 47, 48]. For instance, for $n = 4$ the sequence $call_2^1; call_4^3; call_3^1; call_4^2$ is an EL-O solution with 4 calls.

If the vocabulary is $\mathbb{P}$ then classical planning tasks as defined in Section 5.2 are particular simple epistemic planning tasks: when action descriptions contain no observability operators then classical consistency and EL-O consistency of actions coincide; moreover, $ceff^{-}(ce) = (ceff^{-}(ce))^{=} \text{ and } ceff^{+}(ce) = (ceff^{+}(ce))^{\Rightarrow}$ for all conditional effects, and therefore $R_a^{\text{EL-O}} = R_a^{\text{CPC}}$ for every action $a$. It follows from PSPACE hardness of classical solvability that EL-O solvability of simple epistemic planning tasks is PSPACE-hard, too.

### 5.5. Translation into classical planning

The expansion of a simple epistemic planning task $\mathcal{P} = \langle OA, Act, s_0, Goal \rangle$ adds 'enough' consequences of atoms, viz. the relevant ones occurring in $\mathcal{P}$:

$$\mathrm{Exp}(\mathcal{P}) = \langle \mathrm{Voc}(\mathcal{P}), \{\langle \mathrm{pre}(a), \mathrm{Exp}_{\varphi}(\mathrm{eff}(a)) \rangle : a \in \mathrm{Act} \}, (s_0 \stackrel{\rightarrow}{\cup} \mathrm{I-OA}) \cap \mathrm{Voc}(\mathcal{P}), \mathrm{Goal} \rangle$$

where the expansion of the effects of an action relative to $\mathcal{P}$ is defined as:

$$\mathrm{Exp}_{\varphi}(\mathrm{eff}(a)) = \{\langle \mathrm{cnd}(ce), \mathrm{ceff}^{+}(ce) \Rightarrow \cap \mathrm{Voc}(\mathcal{P}), \mathrm{ceff}^{-}(ce) \rightleftharpoons \cap \mathrm{Voc}(\mathcal{P}) \rangle : ce \in \mathrm{eff}(a)\}.$$

After expansion classical solvability and EL-O solvability coincide:

**Proposition 12.** Let $\mathcal{P} = \langle OA, Act, s_0, Goal \rangle$ be a simple epistemic planning task. Then $\mathcal{P}$ is EL-O solvable iff $\mathrm{Exp}(\mathcal{P})$ is classically solvable.
**Example 9.** The planning task corresponding to the original gossip problem is $G_1 = \langle \text{OA}, Act^{G_1}, s_0^{G_1}, Goal^{G_1} \rangle$ with

$$Act^{G_1} = \{\text{call}_j^i : i, j \in \mathbb{A} \text{ and } i \neq j\},$$

$$s_0^{G_1} = \{S_i s_i : i \in \mathbb{A}\} \cup S \text{ for some } S \subseteq \{s_i : i \in \mathbb{A}\},$$

$$Goal^{G_1} = \bigwedge_{i, j \in \mathbb{A}} S_i s_j.$$

It can be solved via $2n - 4$ calls; when $n \ge 4$ then there is no EL-O solution that takes less calls [46, 47, 48]. For instance, for $n = 4$ the sequence $call_2^1; call_4^3; call_3^1; call_4^2$ is an EL-O solution with 4 calls.

If the vocabulary is $\mathbb{P}$ then classical planning tasks as defined in Section 5.2 are particular simple epistemic planning tasks: when action descriptions contain no observability operators then classical consistency and EL-O consistency of actions coincide; moreover, $ceff^{-}(ce) = (ceff^{-}(ce))^{=} \text{ and } ceff^{+}(ce) = (ceff^{+}(ce))^{=} \text{ for all conditional effects, and therefore } R_{\mathbb{A}}^{\text{EL-O}} = R_{\mathbb{A}}^{\text{CPC}} \text{ for every action } \mathbb{A}$. It follows from PSPACE hardness of classical solvability that EL-O solvability of simple epistemic planning tasks is PSPACE-hard, too.

### 5.5. Translation into classical planning

The expansion of a simple epistemic planning task $\mathcal{P} = \langle \text{OA}, Act, s_0, Goal \rangle$ adds 'enough' consequences of atoms, viz. the relevant ones occurring in $\mathcal{P}$:

$$\text{Exp}(\mathcal{P}) = \langle \text{Voc}(\mathcal{P}), \{\langle \text{pre}(a), \text{Exp}_{\varphi}(\text{eff}(a)) \rangle : a \in \text{Act} \}, (s_0 \stackrel{\rightarrow}{\cup} \text{I-OA}) \cap \text{Voc}(\mathcal{P}), \text{Goal} \rangle$$

where the expansion of the effects of an action relative to $\mathcal{P}$ is defined as:

$$\text{Exp}_{\varphi}(\text{eff}(a)) = \{\langle \text{cnd}(ce), \text{ceff}^{+}(ce) \stackrel{\rightarrow}{\cap} \text{Voc}(\mathcal{P}), \text{ceff}^{-}(ce) \stackrel{=} \cap \text{Voc}(\mathcal{P}) \rangle : ce \in \text{eff}(a)\}.$$

After expansion classical solvability and EL-O solvability coincide:

**Proposition 12.** Let $\mathcal{P} = \langle \text{OA}, Act, s_0, Goal \rangle$ be a simple epistemic planning task. Then $\mathcal{P}$ is EL-O solvable iff $\text{Exp}(\mathcal{P})$ is classically solvable.
*Proof.* We restrict the domain of the interpretation of actions to

$$ I-STATES|_{\mathrm{Voc}(\mathcal{P})} = \{s \cap \mathrm{Voc}(\mathcal{P}) : s \in I-STATES\} = \{(s \Rightarrow \cup I-OA) \cap \mathrm{Voc}(\mathcal{P}) : s \in 2^{\mathrm{OA}}\}. $$

For each $a \in \mathcal{A}$ we write $sR_a^P s'$ for the restriction of $sR_a^{EL-O}s'$ to the set $I-STATES|_{\mathrm{Voc}(\mathcal{P})}$. We therefore have $sR_a^P s'$ iff $s, s' \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$, $s \models \mathrm{pre}(a)$ and

$$ s' = \left( s \setminus \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{+}(ce)) \right) \rightarrow \mathrm{Voc}(\mathcal{P}). $$

It is easily shown that if $s \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$ then $s' \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$.

We now show the following result: for any state $s \in I-STATES$ and action $a \in \mathcal{A}$, there exists a state $s' \in I-STATES$ such that $sR_a^{EL-O}s'$ iff there exists a state $s'' \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$ such that $(s \cap \mathrm{Voc}(\mathcal{P}))R_a^P s''$, and in that case we have that $s'' = s' \cap \mathrm{Voc}(\mathcal{P})$. The first half is straightforward: as $\mathrm{Voc}(\mathrm{pre}(a)) \subseteq \mathrm{Voc}(\mathcal{P})$, for any introspectively closed state $s$, $s$ and $s \cap \mathrm{Voc}(\mathcal{P})$ agree on $\mathrm{pre}(a)$ and hence $s \models \mathrm{pre}(a)$ iff $s \cap \mathrm{Voc}(\mathcal{P}) \models \mathrm{pre}(a)$ (following Proposition 4). By the same argument, if $sR_a^{EL-O}s'$ and if $(s \cap \mathrm{Voc}(\mathcal{P}))R_a^P s''$, then

$$ s' = \left( s \setminus \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{+}(ce)) \right), $$

and therefore

$$ s' = \left( s \setminus \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \cap \mathrm{Voc}(\mathcal{P}) \models \mathrm{cnd}(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \cap \mathrm{Voc}(\mathcal{P}) \models \mathrm{cnd}(ce)}} (ceff^{+}(ce)) \right). $$

By intersecting this with $\mathrm{Voc}(\mathcal{P})$ we conclude that $s' \cap \mathrm{Voc}(\mathcal{P}) = s''$.

We can extend this result to any sequence of actions: for every $s \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$, there exists a state $s'$ that is reachable from $s$ via $\{R_a^{EL-O} : a \in \mathcal{A}\}$ iff there exists a state $s''$ that is reachable from $s \cap \mathrm{Voc}(\mathcal{P})$ via $\{R_a^P : a \in \mathcal{A}\}$, and in that case $s'' = s' \cap \mathrm{Voc}(\mathcal{P})$. Moreover, $s'$ and $s''$ agree on $\mathrm{Voc}(\mathrm{Goal})$, and therefore $\mathcal{P}$ is EL-O solvable via $\{R_a^{EL-O} : a \in \mathcal{A}\}$

610
Proof. We restrict the domain of the interpretation of actions to

$$
I-STATES|_{\mathrm{Voc}(\mathcal{P})} = \{s \cap \mathrm{Voc}(\mathcal{P}) : s \in I-STATES\} = \{(s \Rightarrow \cup I-OA) \cap \mathrm{Voc}(\mathcal{P}) : s \in 2^{\mathrm{OA}}\}.
$$

For each $a \in \mathit{Act}$ we write $sR_a^P s'$ for the restriction of $sR_a^{\mathrm{EL-O}} s'$ to the set $I-\mathrm{STATES}|_{\mathrm{Voc}(\mathcal{P})}$. We therefore have $sR_a^P s'$ iff $s, s' \in I-\mathrm{STATES}|_{\mathrm{Voc}(\mathcal{P})}$, $s \models \mathrm{pre}(a)$ and

and

$$
s' = \left( s \setminus \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{+}(ce)) \right) \rightrightarrows \mathrm{Voc}(\mathcal{P}).
$$

It is easily shown that if $s \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$ then $s' \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$.

We now show the following result: for any state $s \in I-STATES$ and action $a \in \mathit{Act}$, there exists a state $s' \in I-STATES$ such that $sR_a^{\mathrm{EL-O}} s'$ iff there exists a state $s'' \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$ such that $(s \cap \mathrm{Voc}(\mathcal{P}))R_a^{\mathrm{P}} s''$, and in that case we have that $s'' = s' \cap \mathrm{Voc}(\mathcal{P})$. The first half is straightforward: as $\mathrm{Voc}(\mathrm{pre}(a)) \subseteq \mathrm{Voc}(\mathcal{P})$, for any introspectively closed state $s$, $s$ and $s \cap \mathrm{Voc}(\mathcal{P})$ agree on $\mathrm{pre}(a)$ and hence $s \models \mathrm{pre}(a)$ iff $s \cap \mathrm{Voc}(\mathcal{P}) \models \mathrm{pre}(a)$ (following Proposition 4). By the same argument, if $sR_a^{\mathrm{EL-O}} s'$ and if $(s \cap \mathrm{Voc}(\mathcal{P}))R_a^{\mathrm{P}} s''$, then

$$
s' = \left( s \setminus \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \models \mathrm{cnd}(ce)}} (ceff^{+}(ce)) \right),
$$

and therefore

$$
s' = \left( s \setminus \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \cap \mathrm{Voc}(\mathcal{P}) \models \mathrm{cnd}(ce)}} (ceff^{-}(ce)) \right) \cup \left( \bigcup_{\substack{ce \in \mathrm{eff}(a), \\ s \cap \mathrm{Voc}(\mathcal{P}) \models \mathrm{cnd}(ce)}} (ceff^{+}(ce)) \right).
$$

By intersecting this with $\mathrm{Voc}(\mathcal{P})$ we conclude that $s' \cap \mathrm{Voc}(\mathcal{P}) = s''$.

We can extend this result to any sequence of actions: for every $s \in I-STATES|_{\mathrm{Voc}(\mathcal{P})}$, there exists a state $s'$ that is reachable from $s$ via $\{R_a^{\mathrm{EL-O}} : a \in \mathit{Act}\}$ iff there exists a state $s''$ that is reachable from $s \cap \mathrm{Voc}(\mathcal{P})$ via $\{R_a^{\mathrm{P}} : a \in \mathit{Act}\}$, and in that case $s'' = s' \cap \mathrm{Voc}(\mathcal{P})$. Moreover, $s'$ and $s''$ agree on $\mathrm{Voc}(\mathrm{Goal})$, and therefore $\mathcal{P}$ is EL-O solvable via $\{R_a^{\mathrm{EL-O}} : a \in \mathit{Act}\}$

610
iff the planning task $\langle \text{Voc}(\mathcal{P}), \text{Act}, (s_0 \stackrel{\rightarrow}{\cup} \text{l-OA}) \cap \text{Voc}(\mathcal{P}), \text{Goal} \rangle$ is EL-O solvable
via $\{R_a^\mathcal{P} : a \in \text{Act}\}$. Finally, thanks to Proposition 6 the latter is the case iff
the expansion of $\mathcal{P}$ is classically solvable via $\{R_a^{\text{CPC}} : a \in \text{Act}\}$. $\square$

615

5.6. Complexity

Our translation from epistemic planning to classical planning increases
task length only polynomially:

**Proposition 13.** For every simple epistemic planning task $\mathcal{P}$, $l(\text{Exp}(\mathcal{P})) \le (l(\mathcal{P}))^2$.

620

*Proof.* This follows from Proposition 1.

□

**Proposition 14.** *Solvability of a simple epistemic planning task is PSPACE-complete.*

*Proof.* We have seen in Section 5.2 that classical planning tasks can be viewed as simple epistemic planning tasks. The solvability problem is therefore PSPACE-hard just as classical planning [14]. Membership follows from Propositions 13 and 12 and from Bylander's proof that classical planning is in PSPACE [14]. □

625

□

6. Applications

In this section, we give some examples of epistemic planning tasks. We start with the Byzantine Generals Problem and some toy examples most of which were introduced in [49]. We then focus on the generalised gossip problem.

630

6.1. *Two Generals’ Problem*

The Two Generals' Problem [50, 51] is about coordination by communi-
cating over an unreliable channel, highlighting the importance of common
knowledge. The Byzantine Generals' Problem [52] is a generalisation of
that problem. In short, two generals need to coordinate an attack; they can

635
iff the planning task $\langle \text{Voc}(\mathcal{P}), \text{Act}, (s_0 \stackrel{\rightarrow}{\cup} \text{l-OA}) \cap \text{Voc}(\mathcal{P}), \text{Goal} \rangle$ is EL-O solvable
via $\{R_a^\mathcal{P} : a \in \text{Act}\}$. Finally, thanks to Proposition 6 the latter is the case iff
the expansion of $\mathcal{P}$ is classically solvable via $\{R_a^{\text{CPC}} : a \in \text{Act}\}$. $\square$

615

5.6. Complexity

Our translation from epistemic planning to classical planning increases
task length only polynomially:

**Proposition 13.** For every simple epistemic planning task $\mathcal{P}$, $l(\text{Exp}(\mathcal{P})) \le (l(\mathcal{P}))^2$.

620

*Proof.* This follows from Proposition 1.

□

**Proposition 14.** *Solvability of a simple epistemic planning task is PSPACE-complete.*

*Proof.* We have seen in Section 5.2 that classical planning tasks can be viewed as simple epistemic planning tasks. The solvability problem is therefore PSPACE-hard just as classical planning [14]. Membership follows from Propositions 13 and 12 and from Bylander's proof that classical planning is in PSPACE [14]. □

625

□

6. Applications

In this section, we give some examples of epistemic planning tasks. We start with the Byzantine Generals Problem and some toy examples most of which were introduced in [49]. We then focus on the generalised gossip problem.

630

6.1. *Two Generals’ Problem*

The Two Generals' Problem [50, 51] is about coordination by communi-
cating over an unreliable channel, highlighting the importance of common
knowledge. The Byzantine Generals' Problem [52] is a generalisation of
that problem. In short, two generals need to coordinate an attack; they can

635
640

win only if they attack at the same time: either both attack in the morning (ta) or both attack in the afternoon (¬ta). To communicate they must send a messenger who can be captured. They must decide on a time to attack, agree on this time, and each general must know that the other has agreed, and so on. To do this, one general sends a time for the attack, but since he cannot be sure the message was received, the other general must send an acknowledgment. Of course, just like the original message, the acknowledgment can be lost, so the first general must send an acknowledgment, and so on. It is impossible to be fully coordinated, i.e., to obtain common knowledge of the fact that the second general knows the time of the attack.

645

Formally, with $\mathbf{A} = \{1,2\}$ and $\mathbf{P} = \{ta\}$, we define the atom $\alpha_n$ as:

650

* $\alpha_n = \underbrace{S_1 S_2 S_1 \dots S_2 ta}_{n \text{ alternations}}$ if $n$ is even;

* $\alpha_n = \underbrace{S_2 S_1 S_2 \dots S_2 ta}_{n \text{ alternations}}$ if $n$ is odd.

For $n \ge 0$ we define the family of actions $\text{sndMsg}_n$ by stipulating:

$$ \text{pre}(\text{sndMsg}_n) = ta \wedge S_1 ta \wedge S_2 ta \wedge \alpha_2 \wedge \alpha_3 \wedge \dots \wedge \alpha_{n-1} $$

$$ \text{eff}(\text{sndMsg}_n) = \{ \langle \tau, \{ta, S_1 ta, S_2 ta, \alpha_2, \alpha_3, \dots, \alpha_n\}, \emptyset \rangle \} $$

whose effect is that the time of the attack is set, that both agents know it, that 1 knows that 2 knows it, and so on until $n$.

655

The planning task to be solved is $\mathcal{P} = \langle \text{OA}, \text{Act}, s_0, \text{Goal} \rangle$ with $s_0 = \emptyset, \text{Goal} = \text{JS} S_2 ta$, and $\text{Act} = \{\text{sndMsg}_n : n \ge 0\}$. There is no solution for this task: while all sequences $\langle \text{sndMsg}_0, \dots, \text{sndMsg}_n \rangle$ are executable, none of them reaches a state where $\text{JS} S_2 ta$ is true.

660

**Remark 6.** The initial state $s_0 = \emptyset$ of the Two Generals' Problem illustrates a case of maximal ignorance as discussed in Remark 5. The infiniteness of the maximal ignorance Kripke model may explain why the DEL literature pays only little attention to this and other Byzantine coordination problems: most presentations are in semantical terms and use model checking
640

win only if they attack at the same time: either both attack in the morning (ta) or both attack in the afternoon (¬ta). To communicate they must send a messenger who can be captured. They must decide on a time to attack, agree on this time, and each general must know that the other has agreed, and so on. To do this, one general sends a time for the attack, but since he cannot be sure the message was received, the other general must send an acknowledgment. Of course, just like the original message, the acknowledgment can be lost, so the first general must send an acknowledgment, and so on. It is impossible to be fully coordinated, i.e., to obtain common knowledge of the fact that the second general knows the time of the attack.

645

Formally, with $\mathbf{A} = \{1,2\}$ and $\mathbf{P} = \{ta\}$, we define the atom $\alpha_n$ as:

650

* $\alpha_n = \underbrace{S_1 S_2 S_1 \dots S_2 ta}_{n \text{ alternations}}$ if $n$ is even;

* $\alpha_n = \underbrace{S_2 S_1 S_2 \dots S_2 ta}_{n \text{ alternations}}$ if $n$ is odd.

For $n \ge 0$ we define the family of actions $\text{sndMsg}_n$ by stipulating:

$$ \text{pre}(\text{sndMsg}_n) = ta \wedge S_1 ta \wedge S_2 ta \wedge \alpha_2 \wedge \alpha_3 \wedge \dots \wedge \alpha_{n-1} $$

$$ \text{eff}(\text{sndMsg}_n) = \{ \langle \tau, \{ta, S_1 ta, S_2 ta, \alpha_2, \alpha_3, \dots, \alpha_n\}, \emptyset \rangle \} $$

whose effect is that the time of the attack is set, that both agents know it, that 1 knows that 2 knows it, and so on until $n$.

655

The planning task to be solved is $\mathcal{P} = \langle \text{OA}, \text{Act}, s_0, \text{Goal} \rangle$ with $s_0 = \emptyset, \text{Goal} = \text{JS} S_2 ta$, and $\text{Act} = \{\text{sndMsg}_n : n \ge 0\}$. There is no solution for this task: while all sequences $\langle \text{sndMsg}_0, \dots, \text{sndMsg}_n \rangle$ are executable, none of them reaches a state where $\text{JS} S_2 ta$ is true.

660

**Remark 6.** The initial state $s_0 = \emptyset$ of the Two Generals' Problem illustrates a case of maximal ignorance as discussed in Remark 5. The infiniteness of the maximal ignorance Kripke model may explain why the DEL literature pays only little attention to this and other Byzantine coordination problems: most presentations are in semantical terms and use model checking
<table><caption>Table 2: Action descriptions for the message task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>enter<sub>i</sub></td><td>¬In<sub>i</sub></td><td>{<span style="text-decoration: overline">T</span>, {In<sub>i</sub>}, 0}</td></tr><tr><td>enter'<sub>i</sub></td><td>¬In<sub>i</sub> ∧ ¬In<sub>j</sub>, i ≠ j</td><td>{<span style="text-decoration: overline">T</span>, {In<sub>i</sub>}, 0}</td></tr><tr><td>leave<sub>i</sub></td><td>In<sub>i</sub></td><td>{<span style="text-decoration: overline">T</span>, 0, {In<sub>i</sub>}}</td></tr><tr><td>reveal<sub>i</sub></td><td>In<sub>i</sub></td><td>{<span style="text-decoration: overline">T</span>, {S<sub>i</sub> m}, 0} &cup; {<span style="text-decoration: overline">In</span><sub>j</sub>, {JS m}, 0}, j ≠ i</td></tr><tr><td>informs<sub>1,2</sub>m</td><td>(In<sub>1</sub> &leftrightarrow; In<sub>2</sub>) &and; S<sub>1</sub> m &and; ¬(S<sub>2</sub> m &and; S<sub>1</sub> S<sub>2</sub> m)</td><td>{<span style="text-decoration: overline">T</span>, {JS m}, 0}</td></tr><tr><td>informs'<sub>1,2</sub>m</td><td>(In<sub>1</sub> &leftrightarrow; In<sub>2</sub>) &and; S<sub>1</sub> m &and; ¬S<sub>2</sub> m &and; S<sub>1</sub> S<sub>2</sub> m</td><td>{<span style="text-decoration: overline">T</span>, {JS m}, 0}</td></tr></tbody></table>

in finite Kripke models. (A finite modelling was however proposed recently in [19].)

## 6.2. Learning a message

Suppose two agents 1 and 2 are outside a room (¬In<sub>1</sub> ∧ ¬In<sub>2</sub>). The room contains a message that we suppose for simplicity to be the value of the propositional variable *m*. Each of the agents can enter and leave the room and can (temporarily) reveal the message when she is in the room. In case the other agent is also in the room the message is jointly seen. (So this is a conditional effect.) We define a series of planning tasks where the initial state is $s_0 = \{m\}$ and where we vary the action descriptions and the goal. For convenience we list all the action descriptions in Table 2.

For a start, consider $Act = \{\text{enter}_i, \text{leave}_i, \text{reveal}_i : i \in \{1, 2\}\}$ where $\text{enter}_i$ and $\text{leave}_i$ respectively have preconditions $¬In_i$ and $In_i$ and the obvious effects and where $\text{reveal}_i$ requires to be in the room and has one unconditional effect ($i$ knows the message) and one conditional effect: if the other agent is in the room then the message becomes common knowledge. We suppose, for simplicity, that there are no epistemic consequences when an agent enters or leaves the room because we are not interested in the epistemic status of
<table><caption>Table 2: Action descriptions for the message task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>enter<sub>i</sub></td><td>¬In<sub>i</sub></td><td>{<span style="text-decoration: overline;">&tau;</span>, {In<sub>i</sub>}, 0}</td></tr><tr><td>enter'<sub>i</sub></td><td>¬In<sub>i</sub> &and; ¬In<sub>j</sub>, i &ne; j</td><td>{<span style="text-decoration: overline;">&tau;</span>, {In<sub>i</sub>}, 0}</td></tr><tr><td>leave<sub>i</sub></td><td>In<sub>i</sub></td><td>{<span style="text-decoration: overline;">&tau;</span>, 0, {In<sub>i</sub>}</span>}</td></tr><tr><td>reveal<sub>i</sub></td><td>In<sub>i</sub></td><td>{<span style="text-decoration: overline;">&tau;</span>, {S<sub>i</sub> m}, 0}</td></tr><tr><td>informs<sub>1,2</sub>m</td><td>(In<sub>1</sub> &leftrightarrow; In<sub>2</sub>) &and; S<sub>1</sub> m &and; ¬(S<sub>2</sub> m &and; S<sub>1</sub> S<sub>2</sub> m)</td><td>{<span style="text-decoration: overline;">In<sub>j</sub>, {JS m}, 0</span>, j &ne; i}</td></tr><tr><td>informs'<sub>1,2</sub>m</td><td>(In<sub>1</sub> &leftrightarrow; In<sub>2</sub>) &and; S<sub>1</sub> m &and; ¬S<sub>2</sub> m &and; S<sub>1</sub> S<sub>2</sub> m</td><td>{<span style="text-decoration: overline;">&tau;</span>, {JS m}, 0}</td></tr></tbody></table>

in finite Kripke models. (A finite modelling was however proposed recently in [19].)

## 6.2. Learning a message

Suppose two agents 1 and 2 are outside a room (¬In<sub>1</sub> &and; ¬In<sub>2</sub>). The room contains a message that we suppose for simplicity to be the value of the propositional variable *m*. Each of the agents can enter and leave the room and can (temporarily) reveal the message when she is in the room. In case the other agent is also in the room the message is jointly seen. (So this is a conditional effect.) We define a series of planning tasks where the initial state is $s_0 = \{m\}$ and where we vary the action descriptions and the goal. For convenience we list all the action descriptions in Table 2.

For a start, consider $Act = \{\text{enter}_i, \text{leave}_i, \text{reveal}_i : i \in \{1, 2\}\}$ where $\text{enter}_i$ and $\text{leave}_i$ respectively have preconditions $¬In_i$ and $In_i$ and the obvious effects and where $\text{reveal}_i$ requires to be in the room and has one unconditional effect (*i* knows the message) and one conditional effect: if the other agent is in the room then the message becomes common knowledge. We suppose, for simplicity, that there are no epistemic consequences when an agent enters or leaves the room because we are not interested in the epistemic status of
$\ln_1$ and $\ln_2$. Consider Goal = $\neg \ln_1 \wedge \neg \ln_2 \wedge S_1 m \wedge S_2 m$. The sequences

$$sol_1 = \langle \text{enter}_1, \text{reveal}_1, \text{leave}_1, \text{enter}_2, \text{reveal}_2, \text{leave}_2 \rangle,$$

$$sol_2 = \langle \text{enter}_1, \text{enter}_2, \text{reveal}_1, \text{leave}_1, \text{leave}_2 \rangle$$

are both solutions of $\langle \text{OA}, \text{Act}, s_0, \text{Goal} \rangle$.

If we replace Goal by Goal' = $\neg \ln_1 \wedge \neg \ln_2 \wedge JSm$ then $sol_2$ still solves $\langle \text{OA}, \text{Act}, s_0, \text{Goal}' \rangle$, but $sol_1$ no longer does so.

Next, consider a variant of Act where the room is so small that it does not fit two persons: we have to replace enterᵢ by enter'ᵢ with precondition pre(enterᵢ) = $\neg \ln_i \wedge \neg \ln_j$, for i ≠ j. Let the resulting action description be Act'. While there is still a solution of $\langle \text{OA}, \text{Act}', s_0, \text{Goal} \rangle$, there is no solution of $\langle \text{OA}, \text{Act}', s_0, \text{Goal}' \rangle$.

Let us augment the set of actions by adding a further action informs₁,₂m whose precondition is that both agents are in the same place, that the speaker 1 knows whether m and that it is possible for her that m is informative for the hearer 2. Let the resulting set of actions be Act''. Then the sequence

$$sol_3 = \langle \text{enter}_1, \text{reveal}_1, \text{leave}_1, \text{informs}_{1,2m} \rangle$$

becomes a further solution of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal} \rangle$ as well as of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal}' \rangle$. Observe that $sol_3$ is shorter than the other solutions.

Let us finally modify Act'' into Act''' by a more demanding precondition of informing, namely by requiring that the speaker knows that her utterance is relevant for the hearer. Then $sol_3$ is no longer a solution of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal} \rangle$ nor of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal}' \rangle$: the speaker lacks knowledge about the hearer. It becomes a solution again if we make the hypothesis that there is initial common knowledge of ignorance about m, i.e., if we set $s'_0 = \{m, JS S_1 m, JS S_2 m\}$.

### 6.3. Selective communication

The following example is from Kominis and Geffner:
$\ln_1$ and $\ln_2$. Consider Goal = $\neg\ln_1 \wedge \neg\ln_2 \wedge S_1 m \wedge S_2 m$. The sequences

$$sol_1 = \langle \text{enter}_1, \text{reveal}_1, \text{leave}_1, \text{enter}_2, \text{reveal}_2, \text{leave}_2 \rangle,$$

$$sol_2 = \langle \text{enter}_1, \text{enter}_2, \text{reveal}_1, \text{leave}_1, \text{leave}_2 \rangle$$

are both solutions of $\langle \text{OA}, \text{Act}, s_0, \text{Goal} \rangle$.

If we replace Goal by Goal' = $\neg\ln_1 \wedge \neg\ln_2 \wedge JSm$ then $sol_2$ still solves $\langle \text{OA}, \text{Act}, s_0, \text{Goal}' \rangle$, but $sol_1$ no longer does so.

Next, consider a variant of Act where the room is so small that it does not fit two persons: we have to replace enterᵢ by enter'ᵢ with precondition $pre(enter'ᵢ) = \neg\ln_i \wedge \neg\ln_j$, for $i \neq j$. Let the resulting action description be Act'. While there is still a solution of $\langle \text{OA}, \text{Act}', s_0, \text{Goal} \rangle$, there is no solution of $\langle \text{OA}, \text{Act}', s_0, \text{Goal}' \rangle$.

Let us augment the set of actions by adding a further action informs₁,₂m whose precondition is that both agents are in the same place, that the speaker 1 knows whether m and that it is possible for her that m is informative for the hearer 2. Let the resulting set of actions be Act''. Then the sequence

$$sol_3 = \langle \text{enter}_1, \text{reveal}_1, \text{leave}_1, \text{informs}_{1,2m} \rangle$$

becomes a further solution of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal} \rangle$ as well as of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal}' \rangle$. Observe that $sol_3$ is shorter than the other solutions.

Let us finally modify Act'' into Act''' by a more demanding precondition of informing, namely by requiring that the speaker knows that her utterance is relevant for the hearer. Then $sol_3$ is no longer a solution of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal} \rangle$ nor of $\langle \text{OA}, \text{Act}'', s_0, \text{Goal}' \rangle$: the speaker lacks knowledge about the hearer. It becomes a solution again if we make the hypothesis that there is initial common knowledge of ignorance about m, i.e., if we set $s'_0 = \{m, JS S_1 m, JS S_2 m\}$.

### 6.3. Selective communication

The following example is from Kominis and Geffner:
<table><caption>Table 3: Action descriptions for the selective communication task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>goright<sub>a</sub></td><td>⊤</td><td>{⟨p<sub>a,k</sub>, {p<sub>a,k+1</sub>}, {p<sub>a,k</sub>}⟩ : 1 ≤ k ≤ 3}</td></tr><tr><td>goleft<sub>a</sub></td><td>⊤</td><td>{⟨p<sub>a,k</sub>, {p<sub>a,k−1</sub>}, {p<sub>a,k</sub>}⟩ : 2 ≤ k ≤ 4}</td></tr><tr><td>sense<sub>a,q</sub></td><td>p<sub>a,2</sub></td><td>{⟨⊤, {S<sub>a</sub> q}, Ø⟩}</td></tr><tr><td>tell<sub>a,q</sub></td><td>S<sub>a</sub> q</td><td>{⟨ϕ<sub>b</sub>, S<sub>b</sub> q, Ø⟩, ⟨ϕ<sub>c</sub>, S<sub>c</sub> q, Ø⟩}</td></tr></tbody></table>

Let $a, b$, and $c$ be three agents in a corridor of four rooms ($p_1, p_2, p_3$ and $p_4$ from left to right). The agents can move from a room to a contiguous room, and when agent $i$ communicates (tells) some information, all the agents that are in the same room or in a contiguous room, will hear what was communicated. For example, if agent $i$ expresses in $p_3$ his knowledge about $q$, all agents in rooms $p_2, p_3$ and $p_4$ will come to know it. We consider the problem where agent $a$ is initially in room $p_1$, $b$ in $p_2$, $c$ in $p_3$, and $a$ has to find out the truth value of a proposition $q$ and let $c$ know without agent $b$ learning it [53].

Let $p_{i,k}$ mean that agent $i$ is in room $p_k$, for $i \in \{a, b, c\}$ and $1 \le k \le 4$. Then the formula $\varphi_b = \bigvee_{1 \le k, \ell \le 4, |k-\ell| \le 1} (p_{b,k} \wedge p_{b,\ell})$ expresses that $b$ is close to $a$, and likewise for $\varphi_c$. We model this as a simple epistemic planning task $\mathcal{P} = \langle \text{OA}, \text{Act}, s_0, \text{Goal} \rangle$ with $\text{Act} = \{\text{goleft}_a, \text{goright}_a, \text{sense}_{a,q}, \text{tell}_{a,q}\}$, $s_0 = \{p_{a,1}, p_{b,2}, p_{c,3}\}$, $\text{Goal} = S_c q \wedge \neg S_b q$.<fnref n="4" /> The descriptions of the actions in $\text{Act}$ are listed in Table 3. Then the sequence

$$ \langle \text{goleft}_a, \text{sense}_{a,q}, \text{goright}_a, \text{goright}_a, \text{goright}_a, \text{tell}_{a,q} \rangle $$

is a solution of $\mathcal{P}$.

<footnote n="4">⁴Kominis and Geffner suppose that the possible initial states are common knowledge. We could express this by adding to $s_0$ the sets $\{\mathcal{JS}_i p_{a,1} : i \in \{a, b, c\}\}$, $\{\mathcal{JS}_i p_{b,2} : i \in \{a, b, c\}\}$, and $\{\mathcal{JS}_i p_{c,3} : i \in \{a, b, c\}\}$. We however disregard these hypotheses because our approach does not require it.</footnote>
<table><caption>Table 3: Action descriptions for the selective communication task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>goright<sub>a</sub></td><td>⊤</td><td>{⟨p<sub>a,k</sub>, {p<sub>a,k+1</sub>}, {p<sub>a,k</sub>}⟩ : 1 ≤ k ≤ 3}</td></tr><tr><td>goleft<sub>a</sub></td><td>⊤</td><td>{⟨p<sub>a,k</sub>, {p<sub>a,k−1</sub>}, {p<sub>a,k</sub>}⟩ : 2 ≤ k ≤ 4}</td></tr><tr><td>sense<sub>a,q</sub></td><td>p<sub>a,2</sub></td><td>{⟨⊤, {S<sub>a</sub> q}, Ø⟩}</td></tr><tr><td>tell<sub>a,q</sub></td><td>S<sub>a</sub> q</td><td>{⟨ϕ<sub>b</sub>, S<sub>b</sub> q, Ø⟩, ⟨ϕ<sub>c</sub>, S<sub>c</sub> q, Ø⟩}</td></tr></tbody></table>

Let $a, b$, and $c$ be three agents in a corridor of four rooms ($p_1, p_2, p_3$ and $p_4$ from left to right). The agents can move from a room to a contiguous room, and when agent $i$ communicates (tells) some information, all the agents that are in the same room or in a contiguous room, will hear what was communicated. For example, if agent $i$ expresses in $p_3$ his knowledge about $q$, all agents in rooms $p_2, p_3$ and $p_4$ will come to know it. We consider the problem where agent $a$ is initially in room $p_1$, $b$ in $p_2$, $c$ in $p_3$, and $a$ has to find out the truth value of a proposition $q$ and let $c$ know without agent $b$ learning it [53].

Let $p_{i,k}$ mean that agent $i$ is in room $p_k$, for $i \in \{a, b, c\}$ and $1 \le k \le 4$. Then the formula $\varphi_b = \bigvee_{1 \le k, \ell \le 4, |k-\ell| \le 1} (p_{b,k} \wedge p_{b,\ell})$ expresses that $b$ is close to $a$, and likewise for $\varphi_c$. We model this as a simple epistemic planning task $\mathcal{P} = \langle \text{OA}, \text{Act}, s_0, \text{Goal} \rangle$ with $\text{Act} = \{\text{goleft}_a, \text{goright}_a, \text{sense}_{a,q}, \text{tell}_{a,q}\}$, $s_0 = \{p_{a,1}, p_{b,2}, p_{c,3}\}$, $\text{Goal} = S_c q \wedge \neg S_b q$.<fnref n="4" /> The descriptions of the actions in $\text{Act}$ are listed in Table 3. Then the sequence

$$ \langle \text{goleft}_a, \text{sense}_{a,q}, \text{goright}_a, \text{goright}_a, \text{goright}_a, \text{tell}_{a,q} \rangle $$

is a solution of $\mathcal{P}$.

<footnote n="4">⁴Kominis and Geffner suppose that the possible initial states are common knowledge. We could express this by adding to $s_0$ the sets $\{\mathcal{JS}_i p_{a,1} : i \in \{a, b, c\}\}$, $\{\mathcal{JS}_i p_{b,2} : i \in \{a, b, c\}\}$, and $\{\mathcal{JS}_i p_{c,3} : i \in \{a, b, c\}\}$. We however disregard these hypotheses because our approach does not require it.</footnote>
6.4. *Pedestrian crossing*

In this 2-agent coordination problem that is derived from Lewis’s [54], a
pedestrian wants to cross a road at the same time as a car wants to reach
its destination. The driver can either continue or stop to let the pedestrian
cross. In the latter case the driver signals to the pedestrian, for example by
flashing the car’s headlights, that it is safe for the pedestrian to cross. We
assume that the intentions of the pedestrian are obvious to the driver while
the car is approaching (but not after it has driven away since the driver will
not be looking in the rear-view mirror), but the pedestrian does not know
this. Thus, before the pedestrian crosses the road, common knowledge must
be established between the two agents (pedestrian and driver) of the pedes-
trian’s intention to cross.

We can model this problem using the following propositional variables:
$d_c$ is true if the car is driving forward, $r_c$ is true if the car has reached its
destination; $r_p$ is true if the pedestrian has reached the other side of the
road, $wr_p$ is true if the pedestrian wants to reach the other side of the road.

Then the planning task can be described as follows. The initial state
is $s_0 = \{d_c, wr_p, S_c wr_p\}$, the goal is $Goal = r_p \wedge r_c$, and the set of actions $Act$
has four elements, three concerning the car and one the pedestrian, whose
preconditions and effects are listed in Table 4. The action drivesOn$_c$ has a
precondition $d_c \wedge \neg r_c$ and (unique) conditional effect that the car reaches its
destination, stops driving and no longer sees the value of $wr_p$ (whether the
pedestrian wants to cross or not). Note that the fact that $S_c wr_p$ becomes
false implies that $JS wr_p$ becomes false because the latter is an atomic (in-
trospective) cause of the former, i.e., because $JS wr_p \in (S_c wr_p)^{=}$.
The action
stopsAndSignals$_c$ has a precondition $d_c \wedge wr_p \wedge S_c wr_p$ and (unique) conditional
effect that the car stops and signals (by flashing its lights) that the driver
knows that the pedestrian wants to cross which leads immediately to com-
mon knowledge of $wr_p$. The third possible action of the car is to restart
(after a stop). Finally, the only action of the pedestrian is crosses$_p$.
6.4. *Pedestrian crossing*

In this 2-agent coordination problem that is derived from Lewis’s [54], a
pedestrian wants to cross a road at the same time as a car wants to reach
its destination. The driver can either continue or stop to let the pedestrian
cross. In the latter case the driver signals to the pedestrian, for example by
flashing the car’s headlights, that it is safe for the pedestrian to cross. We
assume that the intentions of the pedestrian are obvious to the driver while
the car is approaching (but not after it has driven away since the driver will
not be looking in the rear-view mirror), but the pedestrian does not know
this. Thus, before the pedestrian crosses the road, common knowledge must
be established between the two agents (pedestrian and driver) of the pedes-
trian’s intention to cross.

We can model this problem using the following propositional variables:
$d_c$ is true if the car is driving forward, $r_c$ is true if the car has reached its
destination; $r_p$ is true if the pedestrian has reached the other side of the
road, $wr_p$ is true if the pedestrian wants to reach the other side of the road.

Then the planning task can be described as follows. The initial state
is $s_0 = \{d_c, wr_p, S_c wr_p\}$, the goal is $Goal = r_p \wedge r_c$, and the set of actions $Act$
has four elements, three concerning the car and one the pedestrian, whose
preconditions and effects are listed in Table 4. The action drivesOn$_c$ has a
precondition $d_c \wedge \neg r_c$ and (unique) conditional effect that the car reaches its
destination, stops driving and no longer sees the value of $wr_p$ (whether the
pedestrian wants to cross or not). Note that the fact that $S_c wr_p$ becomes
false implies that $JS wr_p$ becomes false because the latter is an atomic (in-
trospective) cause of the former, i.e., because $JS wr_p \in (S_c wr_p)^{=}$.
The action
stopsAndSignals$_c$ has a precondition $d_c \wedge wr_p \wedge S_c wr_p$ and (unique) conditional
effect that the car stops and signals (by flashing its lights) that the driver
knows that the pedestrian wants to cross which leads immediately to com-
mon knowledge of $wr_p$. The third possible action of the car is to restart
(after a stop). Finally, the only action of the pedestrian is crosses$_p$.
<table><caption>Table 4: Action descriptions for the pedestrian crossing task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>drivesOn<sub>c</sub></td><td>d<sub>c</sub> ∧ ¬r<sub>c</sub></td><td>{⟨⊤, {r<sub>c</sub>}, {d<sub>c</sub>, S<sub>c</sub> wr<sub>p</sub>}⟩}</td></tr><tr><td>stopsAndSignals<sub>c</sub></td><td>d<sub>c</sub> ∧ wr<sub>p</sub> ∧ S<sub>c</sub> wr<sub>p</sub></td><td>{⟨⊤, {JS wr<sub>p</sub>}, {d<sub>c</sub>}⟩}</td></tr><tr><td>restarts<sub>c</sub></td><td>¬d<sub>c</sub> ∧ r<sub>p</sub></td><td>{⟨⊤, d<sub>c</sub>, Ø⟩}</td></tr><tr><td>crosses<sub>p</sub></td><td>wr<sub>p</sub> ∧ ((¬d<sub>c</sub> ∧ JS wr<sub>p</sub>) ∨ r<sub>c</sub>)</td><td>{⟨⊤, {r<sub>p</sub>}, {wr<sub>p</sub>}⟩}</td></tr></tbody></table>

Then the two sequences of actions

⟨drivesOn<sub>c</sub>, crosses<sub>p</sub>⟩,

⟨stopsAndSignals<sub>c</sub>, crosses<sub>p</sub>, restarts<sub>c</sub>, drivesOn<sub>c</sub>⟩

both solve our simple epistemic planning task ⟨OA, Act, s<sub>0</sub>, Goal⟩.

## 6.5. Authorisation via plenary meetings

Here is a further example of actions with common knowledge preconditions. Consider a planning task involving cooperation between different agents that can be divided into *m* different stages with tasks to be performed at each stage by each agent. Agents are only authorised to start stage *k* + 1 if *all* tasks of stage *k* have been completed and all agents have common knowledge of this. The only way this can be achieved is by having a plenary meeting at the end of each stage during which each agent announces that her stage-*k* task has been completed.<fnref n="5" />

Each agent *i* requires an authorisation $a_{ik}$ to start her stage-*k* task. Initially, $a_{i1}$ is true for all agents *i*, i.e., $s_0 = \{a_{i1} : i \in A\}$. Let $t_{ik}$ represent

<footnote n="5">⁵The need for common knowledge can be motivated in the following manner: in order to go back to work, agents must know that other agents have completed their stage-*k* task. Therefore agents need an acknowledgement of their announcing that they have completed this task in order to know that they are not preventing anybody else from going on with their work. But just like they need an acknowledgement, others need an acknowledgement of their acknowledgement, and so on, just like in the Byzantine Generals' Problem.</footnote>
<table><caption>Table 4: Action descriptions for the pedestrian crossing task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>drivesOn<sub>c</sub></td><td>d<sub>c</sub> ∧ ¬r<sub>c</sub></td><td>{⟨⊤, {r<sub>c</sub>}, {d<sub>c</sub>, S<sub>c</sub> wr<sub>p</sub>}⟩}</td></tr><tr><td>stopsAndSignals<sub>c</sub></td><td>d<sub>c</sub> ∧ wr<sub>p</sub> ∧ S<sub>c</sub> wr<sub>p</sub></td><td>{⟨⊤, {JS wr<sub>p</sub>}, {d<sub>c</sub>}⟩}</td></tr><tr><td>restarts<sub>c</sub></td><td>¬d<sub>c</sub> ∧ r<sub>p</sub></td><td>{⟨⊤, d<sub>c</sub>, Ø⟩}</td></tr><tr><td>crosses<sub>p</sub></td><td>wr<sub>p</sub> ∧ ((¬d<sub>c</sub> ∧ JS wr<sub>p</sub>) ∨ r<sub>c</sub>)</td><td>{⟨⊤, {r<sub>p</sub>}, {wr<sub>p</sub>}⟩}</td></tr></tbody></table>

Then the two sequences of actions

⟨drivesOn<sub>c</sub>, crosses<sub>p</sub>⟩,

⟨stopsAndSignals<sub>c</sub>, crosses<sub>p</sub>, restarts<sub>c</sub>, drivesOn<sub>c</sub>⟩

both solve our simple epistemic planning task ⟨OA, Act, s<sub>0</sub>, Goal⟩.

## 6.5. Authorisation via plenary meetings

Here is a further example of actions with common knowledge preconditions. Consider a planning task involving cooperation between different agents that can be divided into *m* different stages with tasks to be performed at each stage by each agent. Agents are only authorised to start stage *k* + 1 if *all* tasks of stage *k* have been completed and all agents have common knowledge of this. The only way this can be achieved is by having a plenary meeting at the end of each stage during which each agent announces that her stage-*k* task has been completed.<fnref n="5" />

Each agent *i* requires an authorisation $a_{ik}$ to start her stage-*k* task. Initially, $a_{i1}$ is true for all agents *i*, i.e., $s_0 = \{a_{i1} : i \in A\}$. Let $t_{ik}$ represent

<footnote n="5">⁵The need for common knowledge can be motivated in the following manner: in order to go back to work, agents must know that other agents have completed their stage-*k* task. Therefore agents need an acknowledgement of their announcing that they have completed this task in order to know that they are not preventing anybody else from going on with their work. But just like they need an acknowledgement, others need an acknowledgement of their acknowledgement, and so on, just like in the Byzantine Generals' Problem.</footnote>
<table><caption>Table 5: Action descriptions for the authorisation via plenary meetings task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>doTask<sub>ik</sub></td><td>a<sub>ik</sub></td><td>{⟨T, t<sub>ik</sub> ∧ S<sub>i</sub>t<sub>ik</sub>, Θ⟩}</td></tr><tr><td>authorise<sub>k</sub></td><td>∧<sub>i∈A<sub>k</sub></sub> JS t<sub>i,k-1</sub></td><td>{⟨T, {a<sub>ik</sub> : i ∈ A<sub>k</sub>}, {p<sub>i</sub> : i ∈ A<sub>k</sub>}⟩}</td></tr><tr><td>goMeeting<sub>i</sub></td><td>T</td><td>{⟨T, p<sub>i</sub>, Θ⟩}</td></tr><tr><td>announce<sub>i</sub></td><td>∧<sub>k∈A<sub>i</sub></sub> p<sub>k</sub></td><td>{⟨t<sub>ik</sub> ∧ S<sub>i</sub>t<sub>ik</sub>, JS t<sub>ik</sub>, Θ⟩}</td></tr></tbody></table>

the fact that agent $i \in A$ has completed her stage-$k$ task. The propositional variable $p_i$ is true if agent $i$ is present at the meeting.

The preconditions and effects of the four action types doTask<sub>ik</sub>, authorise<sub>k</sub>, goMeeting<sub>i</sub>, and announce<sub>i</sub> are described in Table 5. For the action doTask<sub>ik</sub>, when an agent completes a task she sees this, but the other agents don't. The action authorise<sub>k</sub> ($k = 2, \dots, m$) authorises the start of stage $k$. Authorisations for stage $k > 1$ are only issued if there is common knowledge that all tasks of stage $k-1$ have been completed. They are thus issued at the end of the plenary meeting. A side effect of this is that all agents leave the meeting. The action goMeeting<sub>i</sub> allows each agent to go to the meeting room whenever she wants. Once everybody is present, each agent $i$ can announce that her task has been completed via the action announce<sub>i</sub>.

The goal is common knowledge that all tasks have been completed:

$$ \text{Goal} = \bigwedge_{i \in A} \bigwedge_{k=1,\dots,m} (t_{ik} \land JS t_{ik}). $$

With 2 agents and 2 stages, the following sequence is a solution:

⟨doTask<sub>11</sub>, doTask<sub>21</sub>, goMeeting<sub>1</sub>, goMeeting<sub>2</sub>, announce<sub>1</sub>, announce<sub>2</sub>, authorise<sub>2</sub>, doTask<sub>12</sub>, doTask<sub>22</sub>, goMeeting<sub>1</sub>, goMeeting<sub>2</sub>, announce<sub>1</sub>, announce<sub>2</sub>⟩.

## 6.6. The generalised gossip problem

Let the set of agents be $A = \{1, \dots, n\}$ and let the set of propositional variables be $\mathbb{P} = \{s_i : i \in A\}$. Let us describe the planning task for the
<table><caption>Table 5: Action descriptions for the authorisation via plenary meetings task</caption><thead><tr><th>action</th><th>precondition</th><th>conditional effects</th></tr></thead><tbody><tr><td>doTask<sub>ik</sub></td><td>a<sub>ik</sub></td><td>{⟨T, t<sub>ik</sub> ∧ S<sub>i</sub>t<sub>ik</sub>, Θ⟩}</td></tr><tr><td>authorise<sub>k</sub></td><td>∧<sub>i∈A</sub> JS t<sub>i,k-1</sub></td><td>{⟨T, {a<sub>ik</sub> : i ∈ A}, {p<sub>i</sub> : i ∈ A}⟩}</td></tr><tr><td>goMeeting<sub>i</sub></td><td>T</td><td>{⟨T, p<sub>i</sub>, Θ⟩}</td></tr><tr><td>announce<sub>i</sub></td><td>∧<sub>k∈A</sub> p<sub>k</sub></td><td>{⟨t<sub>ik</sub> ∧ S<sub>i</sub>t<sub>ik</sub>, JS t<sub>ik</sub>, Θ⟩}</td></tr></tbody></table>

the fact that agent $i \in A$ has completed her stage-$k$ task. The propositional variable $p_i$ is true if agent $i$ is present at the meeting.

The preconditions and effects of the four action types doTask<sub>ik</sub>, authorise<sub>k</sub>, goMeeting<sub>i</sub>, and announce<sub>i</sub> are described in Table 5. For the action doTask<sub>ik</sub>, when an agent completes a task she sees this, but the other agents don't. The action authorise<sub>k</sub> ($k = 2, \dots, m$) authorises the start of stage $k$. Authorisations for stage $k > 1$ are only issued if there is common knowledge that all tasks of stage $k-1$ have been completed. They are thus issued at the end of the plenary meeting. A side effect of this is that all agents leave the meeting. The action goMeeting<sub>i</sub> allows each agent to go to the meeting room whenever she wants. Once everybody is present, each agent $i$ can announce that her task has been completed via the action announce<sub>i</sub>.

The goal is common knowledge that all tasks have been completed:

$$ \text{Goal} = \bigwedge_{i \in A} \bigwedge_{k=1,\dots,m} (t_{ik} \land JS t_{ik}). $$

With 2 agents and 2 stages, the following sequence is a solution:

⟨doTask<sub>11</sub>, doTask<sub>21</sub>, goMeeting<sub>1</sub>, goMeeting<sub>2</sub>, announce<sub>1</sub>, announce<sub>2</sub>, authorise<sub>2</sub>, doTask<sub>12</sub>, doTask<sub>22</sub>, goMeeting<sub>1</sub>, goMeeting<sub>2</sub>, announce<sub>1</sub>, announce<sub>2</sub>⟩.

## 6.6. The generalised gossip problem

Let the set of agents be $A = \{1, \dots, n\}$ and let the set of propositional variables be $\mathbb{P} = \{s_i : i \in A\}$. Let us describe the planning task for the
generalised gossip problem of depth $k$ as a simple epistemic planning task
$G_k = \langle OA, Act^{G_k}, s_0^{G_k}, Goal^{G_k} \rangle$. The initial state is $s_0^{G_k} = \{S_i s_i : i \in A\} \cup S$ for
some $S \subseteq \{s_i : i \in A\}$ (cf. Example 3). As we have seen in Example 4, the
goal of obtaining shared knowledge of depth $k$ can be described in EL-O by

$$ Goal^{G_k} = \bigwedge_{i \in A} \bigwedge_{\sigma \in OBS^{+}, l(\sigma) \le k} \sigma s_i. $$

The set of actions is $Act^{G_k} = \{\text{call}_j^i : i, j \in A, i \neq j\}$, where $\text{pre}(\text{call}_j^i) = \top$ and where for every $0 \le m < k$, every $\sigma_m \in OBS^{\le m}$ of length at most $m$ and every $r \in A$ there are conditional effects $ce \in \text{eff}(\text{call}_j^i)$ of the form:

$$ \text{cnd}(ce) = S_i \sigma_m s_r \lor S_j \sigma_m s_r; $$

$$ \text{ceff}^{+}(ce) = \{\sigma S_i \sigma_m s_r : \sigma \in \{S_i, S_j\}^{\le k-m-1}\} \cup \{\sigma S_j \sigma_m s_r : \sigma \in \{S_i, S_j\}^{\le k-m-1}\} $$

$$ = \{\sigma \sigma_m s_r : \sigma \in \{S_i, S_j\}^{\le k-m}\}; $$

$$ \text{ceff}^{-}(ce) = \emptyset. $$

Remember that {$S_i, S_j$}^{$\le k-m$} denotes the set all sequences of observability op-
erators $S_i$ and $S_j$ of length at most $k-m$. For $k=1$ we obtain $\text{cnd}(ce) =$
$S_i s_r \lor S_j s_r$, $\text{ceff}^{+}(ce) = \{S_i s_r, S_j s_r\}$, and $\text{ceff}^{-}(ce) = \emptyset$, matching Example 7.

We recall that the original gossip problem with $n \ge 4$ agents can be
solved in $2(n-2)$ calls [46, 47, 48] and that there is no shorter solution. It
is known that the generalised gossip problem $G_k$ can be solved in at most
$(k+1)(n-2)$ calls [36] and that there is no shorter solution [4]. For instance,
for $k=2$ and $n=5$ the sequence

$$ \text{call}_3^1, \text{call}_4^1, \text{call}_5^2, \text{call}_5^1, \text{call}_3^1, \text{call}_4^2, \text{call}_4^1, \text{call}_5^1, \text{call}_3^2 $$

770 is a solution with $3 \times 3 = 9$ calls, which is therefore optimal.

6.7. Generalised gossiping with ignorance goals

We can also easily model ignorance goals. Given a set of atoms A, let
$G\text{-}neg_{k,A} = \langle OA, Act^{G\text{-}neg_{k,A}}, s_0^{G\text{-}neg_{k,A}}, Goal^{G\text{-}neg_{k,A}} \rangle$ be the planning task for the gen-
eralised gossip problem of depth $k$ with the atoms of A as the only negative
generalised gossip problem of depth $k$ as a simple epistemic planning task
$G_k = \langle OA, Act^{G_k}, s_0^{G_k}, Goal^{G_k} \rangle$. The initial state is $s_0^{G_k} = \{S_i s_i : i \in A\} \cup S$ for
some $S \subseteq \{s_i : i \in A\}$ (cf. Example 3). As we have seen in Example 4, the
goal of obtaining shared knowledge of depth $k$ can be described in EL-O by

$$Goal^{G_k} = \bigwedge_{i \in A} \bigwedge_{\sigma \in OBS^{+}, l(\sigma) \le k} \sigma s_i.$$

The set of actions is $Act^{G_k} = \{\text{call}_j^i : i, j \in A, i \neq j\}$, where $\text{pre}(\text{call}_j^i) = \top$ and where for every $0 \le m < k$, every $\sigma_m \in OBS^{\le m}$ of length at most $m$ and every $r \in A$ there are conditional effects $ce \in \text{eff}(\text{call}_j^i)$ of the form:

$$cnd(ce) = S_i \sigma_m s_r \lor S_j \sigma_m s_r;$$

$$ceff^{+}(ce) = \{\sigma S_i \sigma_m s_r : \sigma \in \{S_i, S_j\}^{\le k-m-1}\} \cup \{\sigma S_j \sigma_m s_r : \sigma \in \{S_i, S_j\}^{\le k-m-1}\}$$

$$= \{\sigma \sigma_m s_r : \sigma \in \{S_i, S_j\}^{\le k-m}\};$$

$$ceff^{-}(ce) = \emptyset.$$

Remember that {$S_i, S_j$}^{$\le k-m$} denotes the set all sequences of observability op-
erators $S_i$ and $S_j$ of length at most $k-m$. For $k=1$ we obtain $cnd(ce) =$
$S_i s_r \lor S_j s_r$, $ceff^{+}(ce) = \{S_i s_r, S_j s_r\}$, and $ceff^{-}(ce) = \emptyset$, matching Example 7.

We recall that the original gossip problem with $n \ge 4$ agents can be
solved in $2(n-2)$ calls [46, 47, 48] and that there is no shorter solution. It
is known that the generalised gossip problem $G_k$ can be solved in at most
$(k+1)(n-2)$ calls [36] and that there is no shorter solution [4]. For instance,
for $k=2$ and $n=5$ the sequence

$$\text{call}_3^1, \text{call}_4^1, \text{call}_5^2, \text{call}_5^1, \text{call}_3^1, \text{call}_4^2, \text{call}_4^1, \text{call}_5^1, \text{call}_3^2$$

770 is a solution with $3 \times 3 = 9$ calls, which is therefore optimal.

6.7. Generalised gossiping with ignorance goals

We can also easily model ignorance goals. Given a set of atoms $A$, let
$G\text{-}neg_{k,A} = \langle OA, Act^{G\text{-}neg_{k,A}}, s_0^{G\text{-}neg_{k,A}}, Goal^{G\text{-}neg_{k,A}} \rangle$ be the planning task for the gen-
eralised gossip problem of depth $k$ with the atoms of $A$ as the only negative
goals. The initial state and the actions remain the same: $s_0^{G-neg_{k,A}} = \{S_i s_i : i \in A\} \cup S$ for some $S \subseteq \{s_i : i \in A\}$ and $Act^{G-neg_{k,A}} = \{\text{call}_j^i : i, j \in A, i \neq j\}$; but the goal changes:

$$ \text{Goal}^{G-neg_{k,A}} = \left( \bigwedge_{\sigma \in \{S_i : i \in A\} \subseteq k} \bigwedge_{j \in A, \sigma s_j \notin A} \sigma s_j \right) \wedge \left( \bigwedge_{\alpha \in A} \neg \alpha \right). $$

Here are some examples:

* $G-neg_{1,\{S_1 S_2\}}$ corresponds to the case where we want everyone to know all secrets, except that 1 should not know the secret of 2;

775

* $G-neg_{1,\{S_1 s_3,S_2 s_4\}}$, to the case where only 1 should not get to know the secret of 3 and 2, the secret of 4;

* $G-neg_{2,\{S_1 S_2 s_3\}}$, to the case of epistemic depth 2 where only 1 should not know whether 2 knows the secret of 3, while 1 and 2 should know the secret of 3;

780

* $G-neg_{3,\{S_1 S_2 s_3\}}$ is the same as $G-neg_{2,\{S_1 S_2 s_3\}}$ but with depth 3.

It was shown in [55] that the existence of a solution for gossiping with ignorance goals is an NP-complete problem.

## 7. Encoding into PDDL and experiments

785

In this section we report about some experiments with those simple epis- temic planning tasks of Section 6 that are parametrised: general gossiping, general gossiping with ignorance goals, and authorisation via plenary meet- ings.

790

The experiments were done using three planners of the optimal track of IPC 2018: Planning-PDBs, Complementary1 and Complementary2. They all gave similar results for the two problems described below, so we chose to only show those for Planning-PDBs. The results were obtained on a GNU/Linux machine running on a 3,6 to 4,4 GHz processor (Ryzen 7 3700x) with 32 GB of RAM and a 30 minutes time limit.
goals. The initial state and the actions remain the same: $s_0^{G-neg_{k,A}} = \{S_i s_i : i \in A\} \cup S$ for some $S \subseteq \{s_i : i \in A\}$ and $Act^{G-neg_{k,A}} = \{\text{call}_j^i : i, j \in A, i \neq j\}$; but the goal changes:

$$ \text{Goal}^{G-neg_{k,A}} = \left( \bigwedge_{\sigma \in \{S_i : i \in A\} \subseteq k} \bigwedge_{j \in A, \sigma s_j \notin A} \sigma s_j \right) \wedge \left( \bigwedge_{\alpha \in A} \neg \alpha \right). $$

Here are some examples:

* $G-neg_{1,\{S_1 S_2\}}$ corresponds to the case where we want everyone to know all secrets, except that 1 should not know the secret of 2;

775

* $G-neg_{1,\{S_1 S_3,S_2 S_4\}}$, to the case where only 1 should not get to know the secret of 3 and 2, the secret of 4;

* $G-neg_{2,\{S_1 S_2 S_3\}}$, to the case of epistemic depth 2 where only 1 should not know whether 2 knows the secret of 3, while 1 and 2 should know the secret of 3;

780

* $G-neg_{3,\{S_1 S_2 S_3\}}$ is the same as $G-neg_{2,\{S_1 S_2 S_3\}}$ but with depth 3.

It was shown in [55] that the existence of a solution for gossiping with ignorance goals is an NP-complete problem.

## 7. Encoding into PDDL and experiments

In this section we report about some experiments with those simple epis-temic planning tasks of Section 6 that are parametrised: general gossiping, general gossiping with ignorance goals, and authorisation via plenary meetings.

785

The experiments were done using three planners of the optimal track of IPC 2018: Planning-PDBs, Complementary1 and Complementary2. They all gave similar results for the two problems described below, so we chose to only show those for Planning-PDBs. The results were obtained on a GNU/Linux machine running on a 3,6 to 4,4 GHz processor (Ryzen 7 3700x) with 32 GB of RAM and a 30 minutes time limit.

790
We first show how to encode simple planning tasks into the Planning Domain Description Language PDDL [56].

## 7.1. Encoding into PDDL

Consider a simple epistemic planning task $\mathcal{P} = (\text{OA}, \text{Act}, s_0, \text{Goal})$. We show how to encode EL-O formulas and actions from $\text{Exp}(\mathcal{P})$ into PDDL. Some PDDL requirement flags should be set depending on the form of conditions $cnd(ce)$ of conditional effects $ce$ of actions as well as on the form of the formula *Goal*:

* the default flag :strips for conjunctions;

* the flag :negative-preconditions for negations;

* the flag :disjunctive-preconditions for negations of conjunctions, and disjunctions, if used to simplify writing.

Fortunately almost all planners from the 2018 International Planning Competition (IPC 2018)<fnref n="6" /> handle conditional effects and negative preconditions, and most of them handle disjunctive preconditions.

Given a formula $\varphi$ without introspective atoms, we define a recursive function $\text{tr}_{\text{PDDL}}(\varphi)$ which returns the encoding of $\varphi$ into PDDL:

$$ 
\begin{align*}
\text{tr}_{\text{PDDL}}(S_{i_1} \dots S_{i_m} p) &= \begin{cases} (p) & \text{if } m = 0, \\ (\mathbf{S}-\mathbf{m} \ \mathbf{i1} \ \dots \ \mathbf{im} \ p) & \text{otherwise;} \end{cases} \\
\text{tr}_{\text{PDDL}}(JS S_{i_1} \dots S_{i_m} p) &= \begin{cases} (\mathbf{JS} \ p) & \text{if } m = 0, \\ (\mathbf{JS}-\mathbf{m} \ \mathbf{i1} \ \dots \ \mathbf{im} \ p) & \text{otherwise;} \end{cases} \\
\text{tr}_{\text{PDDL}}(\neg \varphi) &= (\text{not } \text{tr}_{\text{PDDL}}(\varphi)); \\
\text{tr}_{\text{PDDL}}(\varphi_1 \land \varphi_2) &= (\text{and } \text{tr}_{\text{PDDL}}(\varphi_1) \ \text{tr}_{\text{PDDL}}(\varphi_2)).
\end{align*}
$$

with $p \in \mathbb{P}$, $m \ge 0$, and $i_1, \dots, i_m \in \mathbb{A}$. In words, observability atoms $S_{i_1} \dots S_{i_m} p$ and $JS S_{i_1} \dots S_{i_m} p$ are respectively encoded by the special fluents $\mathbf{S}-\mathbf{m}$ and

<footnote n="6">⁶https://ipc2018-classical.bitbucket.io/</footnote>
We first show how to encode simple planning tasks into the Planning Domain Description Language PDDL [56].

## 7.1. Encoding into PDDL

Consider a simple epistemic planning task $\mathcal{P} = (\text{OA}, \text{Act}, s_0, \text{Goal})$. We show how to encode EL-O formulas and actions from $\text{Exp}(\mathcal{P})$ into PDDL. Some PDDL requirement flags should be set depending on the form of conditions $cnd(ce)$ of conditional effects $ce$ of actions as well as on the form of the formula *Goal*:

* the default flag :strips for conjunctions;

* the flag :negative-preconditions for negations;

* the flag :disjunctive-preconditions for negations of conjunctions, and disjunctions, if used to simplify writing.

Fortunately almost all planners from the 2018 International Planning Competition (IPC 2018)<fnref n="6" /> handle conditional effects and negative preconditions, and most of them handle disjunctive preconditions.

Given a formula $\varphi$ without introspective atoms, we define a recursive function $\text{tr}_{\text{PDDL}}(\varphi)$ which returns the encoding of $\varphi$ into PDDL:

$$ 
\begin{aligned}
\text{tr}_{\text{PDDL}}(S_{i_1} \dots S_{i_m} p) &= \begin{cases} (p) & \text{if } m=0, \\ (\mathbf{S}-\mathbf{m} \text{ il } \dots \text{ im } p) & \text{otherwise;} \end{cases} \\
\text{tr}_{\text{PDDL}}(JS S_{i_1} \dots S_{i_m} p) &= \begin{cases} (\mathbf{JS} p) & \text{if } m=0, \\ (\mathbf{JS}-\mathbf{m} \text{ il } \dots \text{ im } p) & \text{otherwise;} \end{cases} \\
\text{tr}_{\text{PDDL}}(\neg\varphi) &= (\text{not } \text{tr}_{\text{PDDL}}(\varphi)); \\
\text{tr}_{\text{PDDL}}(\varphi_1 \land \varphi_2) &= (\text{and } \text{tr}_{\text{PDDL}}(\varphi_1) \text{ tr}_{\text{PDDL}}(\varphi_2)).
\end{aligned}
$$

with $p \in \mathbb{P}$, $m \ge 0$, and $i_1, \dots, i_m \in \mathbb{A}$. In words, observability atoms $S_{i_1} \dots S_{i_m} p$ and $JS S_{i_1} \dots S_{i_m} p$ are respectively encoded by the special fluents $\mathbf{S}-\mathbf{m}$ and

<footnote n="6">⁶https://ipc2018-classical.bitbucket.io/</footnote>
JS, both with $m+1$ parameters. For $m=0$, the propositional variable $p$ is encoded as a fluent without parameters and $JSp$ is encoded as a special fluent (JS p). The initial state $s_0 \supseteq \text{Voc}(\mathcal{P}) \cap \text{Exp}(\mathcal{P})$ of $\text{Exp}(\mathcal{P})$ is trivially encoded as a set of fluents thanks to $\text{tr}_{\text{PDDL}}(\alpha)$. The formula *Goal* and the preconditions of every action can be encoded using $\text{tr}_{\text{PDDL}}(\varphi)$ since they are all EL-O formulas. We note that we give no encoding into PDDL for atoms of the form $\sigma JS\alpha$ where $\sigma \in \text{OBS}^+$: these atoms are introspective, and as the translation of planning tasks is normalised so as to remove any introspective atoms, we do not need to worry about encoding such atoms.

815

As we consider actions with conditional effects, the requirement flag
:conditional-effects must be set.

820

Consider an action $a \in \text{Act}$. For every $ce \in \text{eff}(a)$ with $ceff^{+}(ce) \supseteq \text{Voc}(\mathcal{P}) = \{\alpha_1, \dots, \alpha_m\}$ and $ceff^{-}(ce) \subsetneq \text{Voc}(\mathcal{P}) = \{\beta_1, \dots, \beta_l\}$, we add the conditional effect:

(when $\text{tr}_{\text{PDDL}}(\text{cnd}(ce))$
(and $\text{tr}_{\text{PDDL}}(\alpha_1) \dots \text{tr}_{\text{PDDL}}(\alpha_m)$
(not $\text{tr}_{\text{PDDL}}(\beta_1)) \dots (\text{not } \text{tr}_{\text{PDDL}}(\beta_l))$)

**Example 10 (Example 7, ctd.).** For the original gossip problem, the action description call<sub>2</sub><sup>1</sup> of Example 7 is coded in PDDL as follows:

(:action call-1-2

825

:effect (and

(when (or (S-1 1 s1) (S-1 2 s1))
(and (S-1 1 s1) (S-1 2 s1)))

...

(when (or (S-1 1 sn) (S-1 2 sn)))

830

(and (S-1 1 sn) (S-1 2 sn))))

This is a direct encoding of a call into PDDL. Observe that we can generalise
it to any $i$ and $j$ by writing:

(:action call

:parameters (?i ?j)

835

:effect (and (forall (?s)
JS, both with $m+1$ parameters. For $m=0$, the propositional variable $p$ is encoded as a fluent without parameters and $JSp$ is encoded as a special fluent (JS p). The initial state $s_0 \supseteq \text{Voc}(\mathcal{P}) \cap \text{Exp}(\mathcal{P})$ of $\text{Exp}(\mathcal{P})$ is trivially encoded as a set of fluents thanks to $\text{tr}_{\text{PDDL}}(\alpha)$. The formula *Goal* and the preconditions of every action can be encoded using $\text{tr}_{\text{PDDL}}(\varphi)$ since they are all EL-O formulas. We note that we give no encoding into PDDL for atoms of the form $\sigma JS\alpha$ where $\sigma \in \text{OBS}^+$: these atoms are introspective, and as the translation of planning tasks is normalised so as to remove any introspective atoms, we do not need to worry about encoding such atoms.

As we consider actions with conditional effects, the requirement flag
:conditional-effects must be set.

Consider an action $a \in \text{Act}$. For every $ce \in \text{eff}(a)$ with $ceff^{+}(ce) \supseteq \text{Voc}(\mathcal{P}) = \{\alpha_1, \dots, \alpha_m\}$ and $ceff^{-}(ce) \subsetneq \text{Voc}(\mathcal{P}) = \{\beta_1, \dots, \beta_l\}$, we add the conditional effect:

(when $\text{tr}_{\text{PDDL}}(\text{cnd}(ce))$
(and $\text{tr}_{\text{PDDL}}(\alpha_1) \dots \text{tr}_{\text{PDDL}}(\alpha_m)$
(not $\text{tr}_{\text{PDDL}}(\beta_1)) \dots (\text{not } \text{tr}_{\text{PDDL}}(\beta_l))$)

**Example 10 (Example 7, ctd.)** For the original gossip problem, the action description call<sub>2</sub><sup>1</sup> of Example 7 is coded in PDDL as follows:

(:action call-1-2
:effect (and
(when (or (S-1 1 s1) (S-1 2 s1))
(and (S-1 1 s1) (S-1 2 s1)))
...
(when (or (S-1 1 sn) (S-1 2 sn))
(and (S-1 1 sn) (S-1 2 sn)))))

This is a direct encoding of a call into PDDL. Observe that we can generalise
it to any $i$ and $j$ by writing:

(:action call
:parameters (?i ?j)
:effect (and (forall (?s)
(and

(when (or (S-1 ?i ?s) (S-1 ?j ?s)))

(and (S-1 ?i ?s) (S-1 ?j ?s)))))))))

Finally, let us consider the generalised gossip problem of depth *k* for the case of two agents 1 and 2. According to Section 6.6, call<sub>2</sub><sup>1</sup> can be modelled as follows:

(:action call-1-2

:effect (and

(when (or (S-1 1 s1) (S-1 2 s1)))

(and (S-1 1 s1) (S-1 2 s1))

845

(S-2 1 2 s1) (S-2 2 1 s1)

...

(S-k 1 2 1 ... s1) (S-k 2 1 2 ... s1)))

(when (or (S-1 1 s2) (S-1 2 s2)))

(and (S-1 1 s2) (S-1 2 s2))

850

(S-2 1 2 s2) (S-2 2 1 s2)

...

(S-k 1 2 1 ... s2) (S-k 2 1 2 ... s2))))) )

## 7.2. Experiments

In previous experiments we had used the planner FDSS-2014 [57] that handles conditional effects and negative and disjunctive preconditions for the gossip problem [10]. In more recent experiments we have used Planning-PDBs [58], as reported in the sequel. In comparison, the behaviour on the gossip problem was very similar, which is explained by the fact that in both cases the bottleneck was the grounding phase.

855

860

The resources available online<sup>7</sup> also contain an open-source PDDL generator for the gossip problem that was developed in Python<sup>8</sup>. It allowed

<footnote n="7"><sup>7</sup>http://www.irit.fr/%7EAndreas.Herzig/P/Ecai16.html</footnote>

<footnote n="8"><sup>8</sup>https://github.com/FaustineMaffre/GossipProblem-PDDL-generator</footnote>
(and

(when (or (S-1 ?i ?s) (S-1 ?j ?s)))

(and (S-1 ?i ?s) (S-1 ?j ?s)))))))))

Finally, let us consider the generalised gossip problem of depth *k* for the case of two agents 1 and 2. According to Section 6.6, call<sub>2</sub><sup>1</sup> can be modelled as follows:

(:action call-1-2

:effect (and

(when (or (S-1 1 s1) (S-1 2 s1)))

(and (S-1 1 s1) (S-1 2 s1))

(S-2 1 2 s1) (S-2 2 1 s1)

...

(S-k 1 2 1 ... s1) (S-k 2 1 2 ... s1)))

(when (or (S-1 1 s2) (S-1 2 s2)))

(and (S-1 1 s2) (S-1 2 s2))

(S-2 1 2 s2) (S-2 2 1 s2)

...

(S-k 1 2 1 ... s2) (S-k 2 1 2 ... s2))))) )

## 7.2. Experiments

In previous experiments we had used the planner FDSS-2014 [57] that handles conditional effects and negative and disjunctive preconditions for the gossip problem [10]. In more recent experiments we have used Planning-PDBs [58], as reported in the sequel. In comparison, the behaviour on the gossip problem was very similar, which is explained by the fact that in both cases the bottleneck was the grounding phase.

The resources available online<sup>7</sup> also contain an open-source PDDL generator for the gossip problem that was developed in Python<sup>8</sup>. It allowed

<footnote n="7"><sup>7</sup>http://www.irit.fr/%7EAndreas.Herzig/P/Ecai16.html</footnote>

<footnote n="8"><sup>8</sup>https://github.com/FaustineMaffre/GossipProblem-PDDL-generator</footnote>
us to create the domain and problem files for the generalised gossip problem and its variant with ignorance goals. In its basic settings, the program needs the depth $k$ and the number of agents $n$. It is also possible to specify sets of negative goals, either directly by giving the index of agents such as $\{S_1 s_3, S_2 s_4\}$, or with constraints such as $\{S_i s_j : i \neq j \text{ and } j < 3\}$ if we want no agent except 1 and 2 to know all secrets. Feeding the resulting files into a PDDL planner returns a solution to the corresponding gossip problem, namely a sequence of calls.

**Generalised gossip problem.** We ran FDSS-2014 and Planning-PDBs fixing a number of agents $n$ and increasing the depth $k$ until the first $k$ that leads to a timeout. We recall that the original gossip problem with $n \ge 4$ agents can be solved in $2n-4$ calls and the generalised gossip problem (without negative goals) in at most $(k+1)(n-2)$ calls. For $k=2$ and $n=5$ the optimal plan found by both FDSS-2014 and Planning-PDBs was the following with 9 calls:

$$ \langle \text{call}_2^1, \text{call}_3^1, \text{call}_5^4, \text{call}_4^1, \text{call}_5^3, \text{call}_5^2, \text{call}_5^1, \text{call}_4^2, \text{call}_4^3 \rangle. $$

More generally, for $k=2$ and $n \le 5$, FDSS-2014 was able to find all optimal solutions that are computed by the protocol given in [36] and produced a timeout for $n=6$. For $n \ge 8$, FDSS-2014 produced a timeout already for $k=1$. The performance of Planning-PDBs was only slightly better: for $k=1$ the timeout occurred for $n=9$ and a solution was found for $n=8$ in 848s. Figure 1 gives the execution time of Planning-PDBs parametrised by the depth, while Figure 2 gives the execution time parametrised by the number of agents.

**Generalised gossiping with ignorance goals.** We ran FDSS-2014 and Planning-PDBs in the same manner as the generalised gossip problem, fixing a number of agents $n$ and increasing the depth $k$ until the first $k$ leading to a timeout. This time the timeout occurred for exactly the same $n$ and $k$. Table 6 contains the optimal plans that were produced for $n=4$ agents. The timeout occurred for $k=3$.
us to create the domain and problem files for the generalised gossip problem and its variant with ignorance goals. In its basic settings, the program needs the depth $k$ and the number of agents $n$. It is also possible to specify sets of negative goals, either directly by giving the index of agents such as $\{S_1 s_3, S_2 s_4\}$, or with constraints such as $\{S_i s_j : i \neq j \text{ and } j < 3\}$ if we want no agent except 1 and 2 to know all secrets. Feeding the resulting files into a PDDL planner returns a solution to the corresponding gossip problem, namely a sequence of calls.

**Generalised gossip problem.** We ran FDSS-2014 and Planning-PDBs fixing a number of agents $n$ and increasing the depth $k$ until the first $k$ that leads to a timeout. We recall that the original gossip problem with $n \ge 4$ agents can be solved in $2n-4$ calls and the generalised gossip problem (without negative goals) in at most $(k+1)(n-2)$ calls. For $k=2$ and $n=5$ the optimal plan found by both FDSS-2014 and Planning-PDBs was the following with 9 calls:

$$ \langle \text{call}_2^1, \text{call}_3^1, \text{call}_5^4, \text{call}_4^1, \text{call}_5^3, \text{call}_5^2, \text{call}_5^1, \text{call}_4^2, \text{call}_4^3 \rangle. $$

More generally, for $k=2$ and $n \le 5$, FDSS-2014 was able to find all optimal solutions that are computed by the protocol given in [36] and produced a timeout for $n=6$. For $n \ge 8$, FDSS-2014 produced a timeout already for $k=1$. The performance of Planning-PDBs was only slightly better: for $k=1$ the timeout occurred for $n=9$ and a solution was found for $n=8$ in 848s. Figure 1 gives the execution time of Planning-PDBs parametrised by the depth, while Figure 2 gives the execution time parametrised by the number of agents.

**Generalised gossiping with ignorance goals.** We ran FDSS-2014 and Planning-PDBs in the same manner as the generalised gossip problem, fixing a number of agents $n$ and increasing the depth $k$ until the first $k$ leading to a timeout. This time the timeout occurred for exactly the same $n$ and $k$. Table 6 contains the optimal plans that were produced for $n=4$ agents. The timeout occurred for $k=3$.
<figure><img src="image_1.png" /><figcaption>Figure 1: Generalised gossiping: time to find an optimal plan vs. epistemic depth (for different fixed numbers of agents)</figcaption></figure>

<table><caption>Table 6: Generalised gossiping with ignorance goals: optimal plans found by FDSS-2014 and Planning-PDBs, for n = 4 agents</caption><tr><td>G-neg<sub>1, {S<sub>1</sub> S<sub>2</sub>}</sub></td><td>&lt;call<sub>3</sub><sup>1</sup>, call<sub>4</sub><sup>1</sup>, call<sub>4</sub><sup>2</sup>, call<sub>4</sub><sup>3</sup>&gt;</td></tr><tr><td>G-neg<sub>1, {S<sub>1</sub> S<sub>3</sub>, S<sub>2</sub> S<sub>4</sub>}</sub></td><td>&lt;call<sub>2</sub><sup>1</sup>, call<sub>4</sub><sup>1</sup>, call<sub>3</sub><sup>2</sup>, call<sub>4</sub><sup>3</sup>&gt;</td></tr><tr><td>G-neg<sub>2, {S<sub>1</sub> S<sub>2</sub> S<sub>3</sub>}</sub></td><td>&lt;call<sub>2</sub><sup>1</sup>, call<sub>4</sub><sup>2</sup>, call<sub>4</sub><sup>3</sup>, call<sub>3</sub><sup>1</sup>, call<sub>3</sub><sup>2</sup>, call<sub>4</sub><sup>2</sup>&gt;</td></tr><tr><td>G-neg<sub>3, {S<sub>1</sub> S<sub>2</sub> S<sub>3</sub>}</sub></td><td>(timeout)</td></tr></table>