As the research in multi-agent domain continues to grow it is becoming more and more important to investigate the agents' relations in such systems: not only to reason about agents' perception of the world but also about agents' knowledge of her and others' knowledge. This type of study is referred as epistemic reasoning. In certain domains, e.g., economy, security, justice and politics, reasoning about others' beliefs could lead to winning strategies or help in changing a group of agents' view of the world. In this work we formalize the epistemic planning problem where the state description is based on non-well-founded set theory. The introduction of such semantics would permit to characterize the planning problem in terms of set operations and not in term of reachability, as the state-ofthe-art suggests. Doing so we hope to introduce a more clear semantics and to establish the basis to exploit properties of set based operations inside multi-agent epistemic planning.
Multi-agent planning and epistemic knowledge have recently gained attention
from several research communities. E cient autonomous systems that can
reason in these domains could lead to winning strategies in various elds such as
economy [
Epistemic planners are not only interested in the state of the world but also
in the knowledge (or beliefs) of the agents. Some problems can be expressed
through less expressive languages and need less powerful, and usually faster,
planners. For example [
C
ounsintghethfeulllanegxuteangte oLfALG ACpGr,esbeansteedthineirSeccotniocnep2t. oSfucshtastyestoenmKs,rtihpkaet csatrnucretuarseosn.
Using a Kripke structure as state has a negative impact on the performances
of the planner. First of all, to store all the necessary states, solvers require a
high amount of memory. Moreover to perform operations, such as entailment
or the application of the transition function, the states have been represented
explicitly. That is why, as the research on epistemic reasoning advances [
In this work we formalized the epistemic planning problem where the states are represented by possibilities (introduced in Section 4) which are based on non-well-founded set theory. This representation will allow us to describe the language through set-based operations and also to exploit some of the results from this eld, such as the concept of bisimulation, to add important features to the multi-agent epistemic (MEP) community.
The paper is organized as follows: Section 2 will present the concept of epistemic planning. In Section 3 we will introduce what, in our opinion, is the most complete action language for MEP that bases its states on the concept of Kripke structure. The background will be then concluded with Section 4 where we will describe possibilities, an interesting approach that combines non-well-founded set theory with epistemic logic. In Section 5 we will introduce our semantics, based on possibilities, of mA (an action language for MEP) and we will show a comparison with the state-of-the-art action language mA . We will nally conclude in Section 6 with future works. 2
In this section we will brie y introduce the background that is necessary to
understand multi-agent epistemic reasoning. As de ned in [
Let AG be a set of agents and let F be a set of propositional variables,
called uents. We have that each world is described by a subset of elements of
F (intuitively, those that are \true" in the world); we also refer to each world
as an interpretation. For each agent ag 2 AG we associate a modal operator
Bag (where B stands for belief) and we represent the beliefs of an agent as belief
formulae in a logic extended with these operators. Moreover, group operators are
also introduced in epistemic logic, such as E and C ; that intuitively represent
the belief of a group of agents and the common knowledge of respectively.
To be more precise, as in [
De nition 2 (belief formula). A belief formula is de ned as follow: { A uent formula is a belief formula; { let ' be belief formula and ag 2 AG, then Bag' is a belief formula; { let '1; '2 and '3 be belief formulae, then :'3 and '1 op '2 are belief formulae, where op 2 f^; _; )g; { all the formulae of the form E ' or C ' are belief formulae, where ' is itself a belief formula and ; 6= AG.
C the language of the belief formulae over the sets F and
Let us denote with LAG
AG. On the other hand we de ne LAG as the language over beliefs formulae that
does not allow the use of C. In [
Example 1. Let us consider the formula Bag1 Bag2 '. This formula expresses that the agent ag1 believes that the agent ag2 believes that ' is true, instead, Bag1 :' expresses that the agent ag1 believes that ' is false.
The classical way of providing a semantics for the language of epistemic logic is
in terms of Kripke models [
A pointed Kripke structure is a pair (M; s) where M is a Kripke structure as
de ned above, and s 2 S, where s represents the real world. As in [
Following the notation of [
De nition 4 (entailment w.r.t. a Kripke structure). Given the belief formulae '; '1; '2, an agent agi, a group of agents , a Kripke structure M = hS; ; B1; :::; Bni, and the worlds s,t 2 S: (i ) (M; s) j= ' if ' is a uent formula and (s) j= '; (ii ) (M; s) j= Bagi ' if for each t such that (s; t) 2 Bi it holds that (M; t) j= '; (iii ) (M; s) j= :' if (M; s) 6j= '; (iv ) (M; s) j= '1 _ '2 if (M; s) j= '1 or (M; s) j= '2; (v ) (M; s) j= '1 ^ '2 if (M; s) j= '1 and (M; s) j= '2; (vi ) (M; s) j= E ' if (M; s) j= Bagi ' for all agi 2 ; (vii ) (M; s) j= C ' if (M; s) j= Ek ' for every k
Ek+1' = E (Ek '). 0, where E0 ' = ' and
We will no further describe the properties of the Kripke structures since those
are not strictly needed to describe the contribution of this paper. The reader who
has interest in a more detailed description can refer to [
The mA [
The language has a declarative, English-like syntax and an event model based semantics which permits to reason about beliefs.
The semantics of mA is based on the assumption that agents are truthful. The language is built over a signature (AG; F ; A), where AG is a nite set of agent identi ers, F is a set of uents, and A is a set of actions.
We will introduce only the basics features of mA . The remaining details
about the language can be found in [
Agent A would like to know whether the coin lies heads or tails up. She would also like to let agent B knowing that she knows this fact. However, she would like to keep this information secret from C.
This can be achieved by: i) Distracting C from looking at the box; ii) Signaling B to look at the box if B is not looking at it; iii) Opening the box; and iv) Peeking into the box.
For this domain, we have that AG = fA; B; Cg, while the set of uent F consists of: { heads: the coin lies heads up; { key(ag): agent ag has the key of the box; { opened: the box is open; and { look(ag): agent ag is looking at the box.
Let ag 2 AG, the set of actions A comprises: { open: an agent opens the box; { peek: an agent peeks into the box; { signal(ag): an agent signals to agent ag to look at the box; { distract(ag): an agent distracts agent ag; { shout tails: an agent announces that the coin lies tails up.
In [
Given an action instance a 2 AI, where AI is the set of all the possible action instances A AG, a uent literal f 2 F , a uent formula and a belief formula ' we can quickly introduce the syntax adopted in mA .
Executability conditions are captured by statements of the form: For ontic actions we have: Sensing actions statements have the form expressed by Finally announcement actions are expressed as follows: executable a if ' a causes f if ' a determines f a announces :
In multi-agent domains the execution of an action might change or not the beliefs of an agent. This because, in such domains, each action instance associates an observability relation to each agent. For example the agent C that becomes oblivious as distracted by the agent A, is not able to see the execution of the action openhAi. On the other hand, watching an agent executing a sensing or an announcement action can change the beliefs of who is watching, e.g., the agent B, who is watching the agent A sensing the status of the coin, will know that A
knows the status of the coin without knowing the status herself. In Table 1 are summarized the possible observability relations for each type of action. Partial observability for World-altering action is not admitted as, whenever an agent is aware of the execution of an ontic action, she must knows its e ects on the world as well.
For brevity we address the reader to [
This section de nes the concept of possibility (originally introduced in [
For a more informative introduction the reader is addressed to [
Non-well-founded set theory fundamentals
We start by giving some fundamental de nitions of non-well-founded set theory.
First of all a well-founded set is described in [
Well-founded set theory states that all the sets in the sense of De nition 5 can be represented in the form of graphs, called pictures, (as shown in Figure 1). To formalize this concept of `picture of a set' however it is necessary to introduce the concept of decoration: De nition 6 (decoration and picture).
{ A decoration of a graph G=(V; E) is a function that assigns to each node n 2 V a set n in such a way that the elements of n are exactly the sets assigned to successors of n, i.e., n = f n0 j (n; n0) 2 Eg. { If is a decoration of a pointed graph (G; n), then (G; n) is a picture of the set n. (a) Pictures of von Neumann ordinals where 0 = ;; 1 = f;g; 2 = f;; f;gg; 3 = f;; f;g; f;; f;ggg. (b) Alternative Pictures of von
Moreover, in well-founded set theory, it holds the Mostovski's lemma: \each well-founded graph3 is a picture of exactly one set".
On the other hand in [
De nition 7 (non-well-founded set). A set is non-well-founded (or
extraordinary) when among its descents there are some which are in nite.
In fact, when the Foundation Axiom4 is substituted by the Anti-Foundation
Axiom (AFA), expressed by Aczel in [
A quick example of this representation can be derived by the set = f g
(Figure 2). We can, in fact, informally de ne this set by the (singleton) system
of equations x = fxg. Systems of equations and their solutions are described
more formally as follows in [
Since both graphs and systems of equations are representations for
non-wellfounded sets, it is natural to investigate their relationships. In particular it is
interesting to point out how from a graph G=(V; E) it is possible to construct a
system of equations and vice versa. The nodes in G, in fact, can be the set of
atoms (X ) and, for each node v 2 V , an equation is represented by v = fv0 j
(v; v0) 2 Eg. Since each graph has a unique decoration, each system of equations
has a unique solution. This is also true when we consider bisimilar systems of
equations. In fact we can collapse them into their minimal representation thanks
to the concept of maximum bisimulation as introduced in [
Possibilities
Let us introduce the notion of possibility as in [
In Section 5.1 we will use this concept to describe a `state' of the planning problem. The intuition behind this idea is that a possibility u is a possible interpretation of the world and of the agents' beliefs; in fact u(f) speci es the truth value of the uent f in u and u(A) is the set of all the interpretations the agent A considers possible in u.
Moreover a possibility can be pictured as a decoration of a labeled graph and therefore as a unique solution to a system of equations for possibilities. A 5 Objects that are not sets and have no further set-theoretic structure. 6 (X ) denotes the class of atoms X in which is described. possibility represents the solution to the minimal system of equations in which all bisimilar systems of equations are collapsed; that is the possibilities that represent decorations of bisimilar labeled graphs are bisimilar and can be represented by the minimal one. This shows that the class of bisimilar labeled graphs and, therefore, of bisimilar Kripke structures, used by mA as states, can be represented by a single possibility.
De nition 10 (equations for possibilities). Given a set of agents AG and a set of propositional variables F , a system of equations for possibilities in a class of possibilities X is a set of equations such that for each x 2 X there exists exactly one equation of the form x(f) = i, where i 2 f0; 1g, for each f 2 F , and of the form x(ag) = X, where X X , for each ag 2 AG.
A solution to a system of equations for possibilities is a function that assigns to each atom x a possibility x in such a way that if x(f) = i is an equation then x(f) = i, and if x(ag) = is an equation, then x(ag) = f y j y 2 g. 5
The research on multi-agent epistemic domain, both in logic and planning,
already comprehends several theoretical studies [
Anyway multi-agent epistemic solvers still have to reason on domains where the number of uents and/or agents is limited. This is to reduce the length of the planning problems solution that otherwise would require an excessive quantity of resources (i.e., time and memory). For these reasons the demand of computational resources needed (for example in respect to classical planning) is one of the central problem in MEP.
To reduce this gap several approaches can be used: i) as in [
Changing the structure is especially important because di erent state representation can lead to a better use of the resources, and to exploit properties of the new structure to introduce important functionalities; e.g., mA could rely on the concept of bisimulation to introduce the notion of visited states, being bisimulation an equality criteria for non-well-founded sets. 5.1
State As main contribution we introduce a modi ed version of mA , called mA . The di erence is in how a state is de ned: in mA a state is represented as a Kripke structure while in mA a state is a possibility (Section 4.2). For simplicity, we maintain the syntax used in mA .
The strict connection of these two structures is highlighted in [
Let us de ne the usage of possibilities as states in a MEP domain where the set of agents is AG and the set of uents is F . A possibility is a function that assigns to each propositional variable f 2 F a truth value u(f) 2 f0; 1g and to each agent ag 2 AG a set of possibilities u(ag).
A state in MEP has to encode the truth value of the uents, as in classical planning, and also the beliefs of the agents about uents and beliefs themselves. We de ned in Section 3 how Kripke structures represent these information. In Figure 3 we use a possibility as a system of equations to encode a state (of the domain in Example 2).
An equation is represented in the form u = f(ag1; ); (ag2; 0); : : : ; f; f0; : : : g where ag1, ag2 2 AG, ; 0 are sets of possibilities and f; f0 2 F . When we write (ag; ) we mean that, in u, the agent ag believes that the possibilities in are plausible. On the other hand only if a uent f is present in the equation this means that the uent itself is true in u. 8>w = f(ag; fw; w0g); (C; fv; v0g); look(ag); key(A); openedg ><>w0 = f(ag; fw; w0g); (C; fv; v0g); look(ag); key(A); opened; headsg >v = f(A; fv; v0g); (B; fv; v0g); (C; fv; v0g); look(ag); key(A)g >:>v0 = f(A; fv; v0g); (B; fv; v0g); (C; fv; v0g); look(ag); key(A); headsg where ag 2 fA; Bg: (a) System of equations for possibilities.
A,B C
C A,B,C w0 C v0
A,B
A,B,C (b) Decoration of the pointed labeled graph (G; w).
It is clear that a possibility correspond to a decoration of a pointed labeled graph and therefore to a unique Kripke model up to bisimulation. The representation through possibilities allows, in our opinion, a more clear and concise view of the state. That is because each state is represented by a single possibility; e.g., Figure 3 is represented by w= f(ag; fw; w0g); (C; fv; v0g); look(ag); key(A); openedg where ag 2 fA; Bg. One of the reasons we chose to use possibilities as states is to exploit this new structure to introduce new functionalities to MEP. In fact having the states described as possibilities, which are strongly related to non-well-founded sets, help us to introduce the concept of visited states, a core idea in planning.
As said before, a possibility in the sense of decoration, represents all the Kripke structures bisimilar to the decoration itself. This means that with possibilities we can exploit bisimulation to capture the idea of equality between states. In fact, given two bisimilar decorations (or labeled graphs), these, even with structural di erences, are represented by the same possibility. On the other hand this is not true when it comes to Kripke structures. This idea is best described through graphical representation; therefore we will use Figure 4 to explain this concept.
As an example, let us introduce two new actions: flip and tell(ag). The rst one is an ontic action, where an agent inverts the position of the coin; the observability of this action depends on the uents looking. On the other hand, tell(ag) means that an agent announces to ag the position in which she thinks the coin lies while all the other agents are oblivious.
Assuming that the coin lies tails up and given a sequence of action instances = peekhBi; distract(B)hCi; fliphCi; tell(B)hCi7 we show in Figure 4a the result of applying in a slightly modi ed initial state of Example 2 where CfA;B;Cg(opened ^:look(A)). In Figure 4b, it is represented a Kripke structure that has structural di erences in respect to the one in Figure 4a. This means that these two Kripke structures represent two di erent states in mA even if they are intuitively the same. On the contrary, if we think in term of possibilities, both the Kripke structures of Figure 4 are represented by possibility r1=f(A; fs0; s1g); (B; fr1g); (C; fr1g); look(C); key(A); opened; headsg. B, C A, B, C q0 A s0
r1
A A A
A, B, C s1
B, C
A, B, C (a) The resulting Kripke structure after the execution of .
A,B,C s0
A,B,C
A A r1 s1
B,C
A,B,C (b) A Kripke structure bisimilar to the one in Figure 4a.
Thanks to the use of possibilities we can capture bisimilar decoration while
the same were considered di erent in mA and, therefore, check if a state has
7 We recall that in [
E (Ek ').
0, where E0 ' = ' and Ek+1' = already been visited. Next we de ne the concept of entailment and transition function in mA . nally the We now introduce the concept of entailment w.r.t. possibilities.
De nition 11 (entailment w.r.t. possibilities). Given the belief formulae
'; '1; '2, a uent f, an agent ag, a group of agents , and a possibility u:
Finally we introduce the transition function for mA . In de ning this transition
function we made some assumptions: i) we consider that the given initial state
also speci es which world is the pointed one (as said in [
For the sake of readability, the abbreviations used in the following de nition are explained at the end of it.
De nition 12 (transition function for mA ). Let a 2 AI, and a possibility u be given. If a is not executable in u then D(a; u) = ; otherwise if a is executable in u :
v(f) = caused(a) and (v(ag) = u(ag)
v(ag) = Sw2u(ag) D(a; w) {
D(a; u) = v if a is an ontic action instance and (v(f) = u(f) if f 6= caused(a) if f = caused(a) if ag 2 OD if ag 2 FD 8 An agent ag has a false belief about ' in state s if s j= ' and s j= Bag:'. {
D(a; u) = v if a sensed the uent f 8 >; > ><v(ag) = u(ag) >>v(ag) = Sw2u(ag) D(a; w) >:v(ag) = Sw2u(ag)( D(a; w) [ {
D(a; u) = v if a announces the uent formula 8 >; > ><v(ag) = u(ag) >>v(ag) = Sw2u(ag) D(a; w) >:v(ag) = Sw2u(ag)( D(a; w) [ where:
D(:a; w)) D(:a; w)) if sensed(a)[f] 6= u(f) if ag 2 OD and sensed(a)[f] = u(f) if ag 2 FD and sensed(a)[f] = u(f) if ag 2 PD and sensed(a)[f] = u(f) if u 6j= if ag 2 OD and u j= if ag 2 FD and u j= if ag 2 PD and u j= { caused(a) is the uent modi ed by the action instance a; { FD, PD, OD identify the fully observant, partially observant and oblivious agents respectively; { sensed(a)[f] represents the truth value of the uent f determined by a = u(f); { :a describes the action that senses the opposite of a; namely sensed(a)[:f]. Note that sensing and announcement actions generate the empty set when the action e ects do not respect the uents truth values of the possibility where the action is executed. That is because epistemic action (i.e., announcement or sensing) cannot change the state of the world but only the beliefs of the agent.
As example we present the execution of the sequence distract(C)hAi; openhAi on the initial state of Example 2 encoded by the possibility u in Figure 5a. (u
= f(ag; fu; u0g); look(ag); key(A)g u0 = f(ag; fu; u0g); look(ag); key(A); headsg (a) The initial state u.
(v
= f(ag; fv; v0g); look(A); look(B); key(A)g v0 = f(ag; fv; v0g); look(A); look(B); key(A); headsg (b) The state v after executing distract(C)hAi. (w
= f(A; fw; w0g); (B; fw; w0g); (C; fv; v0g); look(A); look(B); key(A); openedg w0 = f(A; fw; w0g); (B; fw; w0g); (C; fv; v0g); look(A); look(B); key(A); opened; headsg (c) The state w after executing distract(C)hAi;openhAi. In this paper we investigated an alternative to Kripke structures as representation for multi-agent epistemic planning states. Doing so we presented mA , an action language for MEP based on possibilities, introducing MEP in non-wellfounded set theory. Moreover we exploited possibilities to de ne a stronger concept of equality on states collapsing all the bisimilar states into the same possibility. Finally, as with mA is more direct to have an implicit state-representation, using possibilities helps in reducing the search-space dimension.
In the near future we intend to implement a planner for mA and to study
alternative representations. In particular we plan to: i) exploit more set-based
operations: especially for the entailment of group operators; ii) formalize the
concept of non-consistent belief for mA ; iii) investigate more thoroughly the
connection between Kripke structures and non-well-founded sets; iv) examine
the concept of bisimulation as equality between epistemic states; v) and nally
consider other alternatives to Kripke structures,e.g., OBDD s [
comparison For a more clear comparison we show the execution, on both mA and mA , of the action instances sequence c = distract(C)hAi; openhAi; peekhAi, that leads to the desired goal, in the domain expressed in Example 2. With this we want to give a graphical explanation of both the transition functions and statespace de ned by the two languages. Each state in mA will be represented by a Kripke structure while in mA will be a possibility (expanded to its respective system of equations for clarity).
The observability relations of each action instance in following Table: c is expressed in the FD PD OD distract(C)hAi
A, B, C openhAi
A, B C peekhAi
A B C
The initial state, based on Example 2, is de ned by the conditions: intially C(key(A)) intially C(:key(B)) intially C(:key(C)) intially C(:opened) intially C(:Bagheads ^ :Bag:heads) for ag 2 fA; B; Cg intially C(look(ag)) for ag 2 fA; B; Cg intially :heads
Finally the goal that both the state in Figure 9 entail is expressed with the following formulae:
BA:heads ^ BA(BB(BAheads _ BA:heads)) BC[ BB(BAheads _ BA:heads) ^ (:BBheads ^ :BB:heads) ^
(:Bagheads ^ :Bag:heads)] A; B; C
A; B; C s0
A; B; C
s1 M0[ ](s0) = flook(ag); key(A)g M0[ ](s1) = flook(ag); key(A); headsg where ag 2 fA; B; Cg.
(u = f(ag; fu; u0g); look(ag); key(A)g
u0 = f(ag; fu; u0g); look(ag); key(A); headsg where ag 2 fA; B; Cg: (a) The intial Kripke structure (M0; s0).
(b) The initial possibility u. M1[ ](p0) =flook(A); look(B); key(A)g M1[ ](p1) =flook(A); look(B); key(A); headsg (v = f(ag; fv; v0g); look(A); look(B); key(A)g
v0 = f(ag; fv; v0g); look(A); look(B); key(A); headsg where ag 2 fA; B; Cg (a) The Kripke stucture (M1; p0), obtained after the execution of distract(C)hAi in (M0; s0) (Figure 6a). (b) Possibility v, obtained after the execution of distract(C)hAi in u (Figure 6b). A; B; C M2[ ](q0) = flook(ag); key(A); openedg M2[ ](p0) = M1[ ](p0) M2[ ](q1) = flook(ag); key(A); opened; headsg M2[ ](p1) = M1[ ](p1) where ag 2 fA; Bg: (a) The Kripke stucture (M2; q0), obtained after the execution of openhAi in (M1; p0) (Figure 7a).
M3[ ](r0) = flook(ag); key(A); openedg M3[ ](p0) = M1[ ](p0) M3[ ](r1) = flook(ag); key(A); opened; headsg M3[ ](p1) = M1[ ](p1) where ag 2 fA; Bg: (a) The Kripke structure (M3; q0), obtained after the execution of peekhAi in (M2; q0). where ag 2 fA; Bg and v; v0; are the possibilities represented in Figure 7b: (b) Possibility w, obtained after the execution of openhAi in v (Figure 7b).
= f(A; fzg); (B; fz; z0g)(C; fv; v0g); look(ag); key(A); openedg z0 = f(A; fz0g); (B; fz; z0g)(C; fv; v0g); look(ag); key(A); opened; headsg where ag 2 fA; Bg and the possibilities v, v0 are represented in Figure 7b. (b) Possibility z, obtained after the execution of peekhAi in w (Figure 8b).