Reasoning about actions and information is one of the most active areas of research in artificial intelligence. In this paper, we study the reasoning in multiagent conformant planning. We introduce a formalism to trace the update of information in multi-agent conformant planning over transition systems. We propose a dynamic epistemic logical framework EALn to capture reasoning in such scenarios and present an upper bound on the time complexity of multi-agent conformant planning in terms of EALn.
Introduction
approach introduced in [
Information change in multi-agent conformant planning Let Act be a set of actions, P be a set of proposition variables, and Ag be a set of agents.
A transition system T is a triple hST , {RaT | a ∈ Act}, V T i, where ST is a non-empty set of states, for each a ∈ Act, RaT is a function from S to P(S), and V T : P → P(ST ) is an assignment function.
We use possibility on transition systems, which is a variant of the notion used in [
A Kripke structure N on T models agents’ uncertainty over states in T . By [1], we know that a pointed Kripke structure can be represented by the following notion from non-well-founded set theory.
Let N be a Kripke structure on a transition system T . A decoration d of N is a function that assigns to each world w ∈ W a function d(w) such that • d(w)(T ) = LN (w) (i.e., d(w) assigns to T a state that is the one with which L labels w), and founded) set of functions associated with worlds reachable from w by 9i9K ).
• for each i ∈ Ag, d(w)(i) = {d(w0) | w 9i9K w0} (i.e., d(w) assigns to each agent i the (non-wellIf d is a decoration of N and w is a world in N , we say that d(w) is the solution of w in N , and (N , w) is a picture of d(w).
Now we are ready to introduce the concept of possibility.
Definition 1 (Possibility). Let T be a transition system. A possibility α on T is a function that assigns to T a state in ST , and to each agent i ∈ Ag a set of possibilities.
As shown in [
The choice of possibilities over Kripke structures as uncertainty representation provides several
advantages (see [
As an example, the update of the possibility α1 depicted in Figure 2a will result in a unit possibility set α11, which is depicted in Figure 3. Moreover, the update of α2 in Figure 2a, whose picture is (N , w2) in Figure 2b, is the set of possibilities α21 and α22, both of which are depicted in Figure 3. The pointed Kripke structures (N 0, w21) and (N 0, w22) are the pictures of α21 and α22 respectively. Moreover, we would like to point out that the difference between α11(i) and α21(i) corresponds to the fact that the information state of agent i at state t1 is different depending on how he/she gets there, and the identity between α11(j) and α21(j) reflects the fact that the information state of agent j at t1 is the same because he/she intuitively cannot distinguish s1 and s2.
α11 = α21 = α22 = {(i, (α11, α11)), (j, (α11, α11)), (j, (α11, α21)), (j, (α11, α22)), t1} {(i, (α21, α21)), (i, (α21, α22)), (j, (α21, α11)), (j, (α21, α21)), (j, (α21, α22)), t1} {(i, (α22, α21)), (i, (α22, α22)), (j, (α22, α11)), (j, (α22, α21)), (j, (α22, α22)), t2} (a) System of equations of α11 i,j w> 11:t`1 j
j i,j
i,j w621: t~1 o
/ w22:t 2h (b) Picture of α11: (N 0, w11) i,j
The logic EALn and its application In this section, we will firstly introduce the language and the semantics of EALn and then use it to capture reasoning in multi-agent conformant planning. At the end of the section, we provide an upper bound for multi-agent conformant planning in terms of EALn.
Definition 3 (Language). The language LEALn is defined by the following BNF:
φ ::= p | ¬φ | φ ∧ φ | [a]φ | Kiφ, where p ∈ P, a ∈ Act, and i ∈ Ag. We use ⊥, ∨, →, h·i as the usual abbreviations.
The formula [a]φ intuitively means that φ holds if the action a is successfully done. The formula Kiφ expresses that the agent i knows that φ. Since the language of EALn contains both action modalities and knowledge modalities, this allows one to talk about the interaction between action and knowledge in the object language.
Formulas of LEALn will be interpreted on dynamic epistemic models. A dynamic epistemic model is a pair (T , α), where T is a transition system and α is a possibility on T such that for each i ∈ Ag, α is in α(i) and α0 ∈ α(i) implies α0(i) = α(i). Definition 4 (Update semantics). Given a dynamic epistemic model (T , α) and a formula φ ∈ LEALn , the satisfaction relation is defined as follows:
T , α T , α
p ⇐⇒ α(T ) ∈ V (p) T , α ¬φ ⇐⇒ T , α 2 φ
φ and T , α φ ∧ ψ ⇐⇒ T , α ψ
Kiφ ⇐⇒ for all α0 ∈ α(i) : T , α0 φ T , α
T , α [a]φ ⇐⇒ for all α0 ∈ α|a : T , α0 φ We say that φ is valid, denoted as φ, if T , α
φ for each dynamic epistemic model T , α.
Within EALn, we can express the epistemic state of agents and its evolvement in multi-agent planning. Take the following example. Let T0 and α1 be depicted as Figure 1 and Figure 2 respectively. We then have the following statements.
• T0, α1 [a](Kip ∧ ¬Kjp). When the initial possibility is α1, after the action a is executed, agent i knows that p, and agent j does not know that p. • T0, α2 [a](¬Kip ∧ ¬Kjp). When the initial possibility is α2, after the action a is executed, neither i not j knows that p. • For all φ ∈ LEALn , T0, α1 [a]Kjφ iff T0, α2 [a]Kjφ. No matter the initial possibility is α1 or α2, after the action a is executed, the knowledge of j is the same.
Within EALn, we can capture reasoning about action and information change in multi-agent conformant planning.
Lemma 1 (Perfect Recall). For each dynamic epistemic model (T , α), we have that T , α for each i ∈ Ag and each a ∈ Act.
Ki[a]φ → [a]Kiφ Proof. Assume that T , α Ki[a]φ. We will show that T , α [a]Kiφ. Taka any α0 ∈ α|a and any β0 ∈ α0(i). To sShinowcetαh0at∈Tα,|aα, by Definition 2, this follows that α0(i) = Sβ∈α(i) β|a. Since β0 ∈ α0(i), we then have [a]Kiφ, by the update semantics, we only need to show that T , β0 φ. that there is some β ∈ α(i) such that β0 ∈ β|a. Since T , α Ki[a]φ and β ∈ α(i), this follows that T , β [a]φ. Moreover, since β0 ∈ β|a, this follows that T , β0 φ. Therefore, we have shown that T , β0 φ for each α0 ∈ α|a and each β0 ∈ α0(i), namely T , α [a]Kiφ. Thus, we have shown that if T , α Ki[a]φ then T , α [a]Kiφ.
Lemma 2 (No Miracles). For each dynamic epistemic model (T , α), we have that T , α for each i ∈ Ag and each a ∈ Act. haiKiφ → Ki[a]φ Proof. Assume that T , α haiKiφ. We will show that T , α Ki[a]φ. By the update semantics, we only need to show that T , β0 φ for each α0 ∈ α(i) and each β0 ∈ α0|a.
Since T , α haiKiφ, this follows that there is some γ ∈ α|a such that T , γ Kiφ. Since γ ∈ α|a, by Definition 2, this follows that γ(i) = Sβ∈α(i) β|a. Take any α0 ∈ α(i). We then have that α0|a ⊆ γ(i). Take any β0 ∈ α0|a. We then have that β0 ∈ γ(i). Since T , γ Kiφ, this follows that T , β0 φ. Thus, we have shown that T , β0 φ for each α0 ∈ α(i) and each β0 ∈ α0|a, namely T , α Ki[a]φ. Thus, we have shown that if T , α haiKiφ then T , α Ki[a]φ.
Intuitively, perfect recall means that if the agent cannot distinguish two states after doing action a, then he/she could not distinguish them before. No miracles mean that if the agent cannot distinguish two states and the same action is executed on both states, then he/she cannot distinguish the resulting states. These can be depicted in Figure 4.
We now introduce multi-agent conformant planning in terms of EALn. First, we introduce some auxiliary notations. Let Σ be a set of possibilities. We use Σ|a to denote the set S | . Let σ ∈ Act∗ be an action sequence a1 · · · an. We use α|σ to denote the information state (· · · ((αα∈|Σa1α)|aa2 ) · · · )|an . Definition 5 (Multi-agent conformant planning). A multi-agent conformant planning problem P is a tuple hT , α, G, {Acti | i ∈ G}, φgi, where T is a transition system, α is the initial possibility on T , G perfect −−re−ca−l→l s1 o a s2 o i i / s3
a / s4 no miracles ←−−−−−−− s1 o a s2 i / s3 a s4 is a group of agents, Acti ⊆ Act is a set of actions that the agent i can perform, φg ∈ LEALn is the goal formula. A solution to P is a finite sequence of actions σ = a1 · · · an ∈ (Si∈G Acti)∗ such that 1) the sequence σ is applicable 1 in the state α0(T ) for each α0 ∈ Ti∈G α(i), and 2) T , β φg for each α0 ∈ Ti∈G α(i) and each β ∈ α0|σ.
Let LaMφ be an abbreviation of the formula hai> ∧ [a]φ. It can be shown that an action sequence which means that the solution can be verified in EALLan1.M · · · LanM>. We then have the following theorem, a1 · · · an is applicable on the state α(T ) iff T , α Theorem 3. Let P = hT , α, G, {Acti | i ∈ G}, φgi be a planning problem. An action sequence a1 · · · an is a solution for P iff T , α0 La1M · · · LanMφg for each α0 ∈ Ti∈G α(i).
In this paper’s remainder, we show an upper bound on the time complexity of multi-agent conformant planning in terms of EALn. i
Let T = hS, {Ra | a ∈ Act}, V i be a transition system and N = hW, {99K | i ∈ Ag}, Li be a Kripke structure on T . The Kripke structure N † = hW N † , {9i9K N † | i ∈ Ag}, LN † i is defined as follows: W N † = {(w, L(w)) | w ∈ W }, 9i9K N † = {((w, L(w)), (w0, L(w0))) | w 9i9K w0}, and LN † (w, L(w)) = L(w). If N is a Kripke structure on T , so is N †. It is obvious that (N , w) is isomorphic to (N †, (w, L(w))). Therefore, if (N , w) is a picture of a possibility α, so is (N †, (w, L(w))).
Given a transition system T and a Kripke structure N on T , let the Kripke structure N † is defined as
above. We now define the update of N † with an action a ∈ Act, denoted as N †|a. The Kripke structure
N †|a = hW N †|a , {9i9K N †|a | i ∈ Ag}, LN †|a i is defined as follows: W N †|a = {(w, s0) ∈ W × S | there is
(w, s) ∈ W N † such that (s, s0) ∈ RaT }, 9i9K N †|a = {((w, s), (w0, s0)) | w 9i9K w0}, and LN †|a (w, s) = s. It is
evident that N †|a is also a Kripke structure on T . We have known that if (N , w) is a picture of a possibility
α, so is (N †, (w, L(w))). If α0 ∈ α|a, this follows that α(T )RaT α0(T ). Let α(T ) = s and α0(T ) = s0. Since
(N , w) is a picture of a possibility α, this follows that L(w) = s, and then we have that (w, s) ∈ W N † .
Since sRaT s0, by the definition of N †|a, we know that (w, s0) ∈ W N †|a . With the bisimulation principle
(see [
Given a possibility α, let the size of α be the size of the minimal pointed Kripke structure (N , w) such that (N , w) is a picture of α. Given a multi-agent conformant planning problem P = hT , α, G, {Acti | i ∈ G}, φgi, let the size of P be the product of the size of T , the size of α, and the size of φg. Theorem 4. Multi-agent conformant planning in terms of EALn is in double exponential time. Proof idea. Given a multi-agent conformant planning P , we can do a breadth-first search with duplicate checking on possibilities to find a plan. Since we have shown above that the number of possibilities that can be generated by the initial possibility α is bounded by the exponent of the size of P , this follows that the depth of the searching tree is bounded by the exponent of the size of P . Therefore, the time of the breadth-first search is in double exponent of the size of P . Moreover, by Theorem 3, we know that the verification of a plan can be reduced to model checking in EALn. Since model checking in EALn is in polynomial time, this follows that searching a plan for P is in double exponential time.
1a1 · · · an is applicable on a state s iff Ra1 (s) 6= ∅, and for each 1 ≤ k < n, t ∈ Ra1···ak (s) implies Rak+1 (t) 6= ∅.