Practical rationality or decision-making is a key component of autonomous agents, like humans, and correspondingly has been studied at large. Research on this topic has been conducted from several fields: game theory, planning, decision theory, etc. each focusing on a different aspect: strategic decision-making, propositional means-ends analysis, and uncertainty, respectively. Moreover, some of these models of rationality also provide a foundation for the notion of agreement (game-theoretic approaches to negotiation, multi-agent planning, etc). Indeed, the process of reaching an agreement seems to be a particular case of (multi-agent) practical decision-making.
While these models of practical rationality are well-understood, they were (understandably) designed with a considerably low level of expressivity at the object language. For instance, game-theory abstracts from propositional representations of states, actions and goals. Planning algorithms take them into account, but not fully in the object language, which makes it difficult to extend these algorithms to reason about others' beliefs and actions. All this contrasts with the area of logic, where logics with increasing expressivity have been characterized; though abilities or motivational attitudes have only more recently been dealt with, in BDI, logics of strategic ability, etc. In the present contribution we mainly focus on combining dynamic epistemic logic and plan search [9], [5].
Specially relevant to the topic of cognitive agents are the notions of belief, action, goal, norm, etc. The first two elements are the target of dynamic epistemic logics DEL, a recent family of logics for reasoning about agents' communications and observations. We focus on the so-called Logics of Communication and Change LCC [10], AT2012, 15-16 October 2012, Dubrovnik, Croatia. Copyright held by the author(s).
which generalize many previously known DEL logics with physical actions and common knowledge. In particular LCC logics include a rich variety of epistemic actions from the literature on DEL, including several types of communicative actions (truthful or lying, public or private announcements). This is done with the help of action models, that assign each action an accessibility relation describing how the action appears to other agents, and hence what they learn after its execution.
These logics may offer a semantic understanding of the notion of agreement between agents, since reaching an agreement requires these agents to have common knowledge about it. The same can be said about the epistemic aspects involved in the (intentional) process of reaching such an agreement. To this end, we address planning problems expressible in LCC. This is done by introducing goals, which can be an arbitrary formula in the language of LCC. Planning domains consist as usual of an initial state formula, available actions and a goal formula, and the task consists in finding some structure of actions that make the goal formula true when executed in the initial state. Instead of a semantic [3], [11], [7] or a proof-theoretic approach [1], we suggest to reduce plan search into search in the space of proofs. With more detail, search methods operate in the space of LCC formulas that are about plans (their success, and executability). As in those works, an LCC plan is built while having in mind what agents can learn during its execution.
In the present contribution, we extend previous results on Backward Planning by describing simpler algorithms for deterministic and strong non-deterministic planning. These are shown to be sound and complete: if the algorithm terminates, it outputs a solution plan; and if a successful plan exists, then the algorithm will find such a solution.
Motivating example. Our aim, then, is to endow LCC reasoning agents with planning capacities for these logics, so they can achieve their goals in scenarios where other agents have similar cognitive and acting abilities. In particular, LCC planning seems necessary for an agent whose goals consist in (or depend on) a certain distribution of knowledge, ignorance and false beliefs among agents. To illustrate the kind of rational behavior an LCC planner can exhibit, consider the following example.
Example 1. Agent a just bet some prize agent b that the next coin toss will land heads (h); a knows she can sense and even flip the coin without b ever suspecting it. Given a sensing action that tells a whether h holds or not, a successful plan seems to be: toss the coin; if sense that h, then announce it to b; otherwise flip the coin and announce h.
Structure of the paper. The paper is structured as follows: after a review of the related work in Section 2, we briefly present the dynamic epistemic logics in LCC in Section 3. Then in Section 4, we present an algorithm for deterministic planning in LCC based on Breadth First Search (BFS) and show it is sound and complete. The rest of the paper is devoted to non-deterministic planning: Section 5 we present an extension of LCC with action composition and choice. Finally, in Section 6 we propose an algorithm for (strong) non-deterministic and show its soundness and completeness. The paper concludes with a summary and some topics for future work.
Several logics address the related problem of plan existence (rather than plan search) for similarly expressive languages. For example, arbitrary public announcement logics APAL [4], and logics for strategic ability. These logics contain modal operators C for agents or coalitions, with formulas C ϕ expressing: there is a plan or strategy allowing agents in C to enforce ϕ.
More in line with the present aims, among logics for action guidance we find the family of BDI and related logics for intention (or some other motivational attitudes). While these logics usually allow for considerable expressivity w.r.t. intention (and their interaction with beliefs), they are not completely understood, and in fact planning methods have been suggested for BDI agent architectures. In particular, Bolander et al. [3] suggest the use of LCC planning to this end for (a limited fragment of) BDI. In this work [3], the authors study incremental forward planning based on the semantics of update models. By incremental we mean that the plan is built in a step-wise fashion: plans are being refined (with further actions) until a solution is found. The framework of [3] is shown to be sound and complete under Breadth First Search, and hence the proposed planning system for LCC becomes semi-decidable. Here we study the opposite direction of search, i.e. backward planning (from the goals to the initial state). The reason is that in forward planning, relevant actions to be considered are those that are currently executable actions to be the notion of relevant action, rather than current goal enforcing actions, as in backward planning. This makes a difference in LCC since many actions may exist (in the action model) which are everywhere executable, so forward planning would typically face the state explosion problem. Along this line, Aucher [1] (and related papers) introduce regression methods for the fragment of LCC without common knowledge. The present work differs from the latter two by making plan search incremental (as in [3], [11]), but allowing for backward search. The proposed algorithms easily adapt to search for optimal plans in backward planning.
We briefly recall the basics of LCC logics [10]. Since these are built by adding an action model U on top of (an epistemic reading of) propositional dynamic logic PDL, we recall the latter first. The syntax of PDL, denoted L PDL , is as follows:
As usual, the symbols ⊥, ∨, ↔ and π are defined from the above as abbreviations.
In the epistemic reading of PDL, denoted as E•PDL, the set of atomic programs a is just the set of agents Ag, and we read the program [a] as agent a believes (or knows) that. 3 With the PDL program constructors (composition ";", choice "∪" and the Kleene star "(•) * ", we can model: nested beliefs
) does, as usual, contain a set of worlds W , a relation R a for each agent a, and an evaluation V : Var → P(W )).
An LCC logic will add to an E•PDL language a set of modalities [U, e] for each pointed action model U, e with distinguished (actual) action e. These new operators [U, e] read after each execution of action e it is the case that. An action model is a tuple Here, though, we will follow [14] and restrict postconditions to post(e)(p) ∈ {p, , ⊥}. This makes the truth-value of p after e to be either: that before e, or simply true or false irregardless of its truth-value before e. (This framework is shown in [14] to be as expressive as the general case above, in case choice of actions is considered. See Section 6.) The PDL semantics [ • ] for E•PDL-formulas can be extended to a semantics for LCC as follows:
In [10], the authors define program transformers T U ij (π) provide a mapping between E•PDL programs. Given any combination of ontic or epistemic actions (e.g. public and private announcements) the transformers provide a complete set of reduction axioms, reducing LCC to E•PDL. These axioms push the U, e-modalities inside the formula, and then the basic case [U, e]p is turned into an E•PDL formula. See [10] for the details on the T U (π) mapping. Definition 1. A calculus for LCC is given by the axioms and rules for PDL plus [U, e] ↔ and the following The completeness for this calculus is shown by reducing LCC to E•PDL. The translation simultaneously defined for formulas and programs, resp. t and r, is
r is trivial for all programs, and t is also trivial for the remaining types of formula. The translation assigns to each L LCC formula an equivalent formula in L E•PDL .
4 Backward deterministic LCC planning.
In [8], we studied LCC planning with the help of generalized frame axioms for LCC (actually, theorems in this logic) used to study the regression of an open goal under an action. Here we propose a simpler approach, based on the above reduction of LCC into E•PDL; and moreover they allow for better plan search methods. We will simply use the expressions of the form
These give rise to a goal-regression function: a current goal ϕ is mapped into t([U, e]ϕ∧ U, e ); the latter is the new goal we need to address for an execution of e to end up in a ϕ-world.
Definition 2. Given some LCC logic for an action model U, a planning domain is a triple M = (ϕ T , A, ϕ G ), where ϕ T , ϕ G are consistent E•PDL formulas describing, resp., the initial and goal states; and A ⊆ E is the subset of a actions available to the agent.
A solution to M is a sequence π = (f 1 , . . . , f m ) of actions in A, such that
Given some planning domain M = (ϕ T , A, ϕ G ), the (initial) empty plan is the pair π ∅ = (∅, ϕ G ) and if π = (π, ϕ goals(π) ) is a plan, then π(e) = (π ∩ e , ϕ goals (π(e))), defined by the goal ϕ goals(π(e)) = t([U, e]ϕ goals(π) ∧ U, e ), is also a plan.A plan π is a leaf iff ϕ goals(π(e)) is inconsistent, or |= ϕ goals(π(e)) → ϕ goals(π) .
Leafs are plans not worth considering, either because unexecutable or noncontributing to the ultimate goals ϕ G . Also note that actions e -as defined above-are deterministic, in the sense that |= [U, e]ϕ ∨ ψ ↔ [U, e]ϕ ∨ [U, e]ψ. Thus, deterministic planning simply consists in "restricting" actions e ∈ E to our current action models, or simply LCC planning. Later we extend LCC with composition ⊗ and choice ∪ to study the non-deterministic case. A BFS plan search algorithm for deterministic planning is the following.
We may consider as well a cost function cost : E → R + assigning to e the cost of an execution of e. 4 This gives a measure of the total cost of a plan cost(π) = Σ e∈π cost(e).
Recall search for optimal plans (e.g. A*) can be defined from BFS in Fig. 1 by adding an extra step in step 3: after updating Plans, this set is re-ordered into a sequence of plans with increasing cost. That is, π is re-ordered before π in Plans if and only if cost(π) ≤ cost(π ). Since by definition cost(e) > 0, and the set E is finite, there can be no infinite sequence of actions with decreasing cost. This implies (using [9] Thm 1) that A* is complete and admissible for deterministic backward planning in LCC using the (trivial) heuristic estimation h(π(e)) = cost(π) + cost(e).
Corollary 1. A* is sound, and complete for LCC backward deterministic planning. It is also admissible: the output of A* is an optimal solution π for (ϕ T , A, ϕ G ), if some solution exists. Example 2. Suppose you are a high-ranked employee a in Phil. Inc and want to sell some sensible information, ¬p = Phil. Inc is not doing well, to a close acquaintance a 1 , an important investor in Phil. Inc. It is commonly ignored that ¬p, except for you and a 0 , also an important investor in Phil. Inc. Knowing ¬p, a 0 wants to sell stocks before a 1 does, but she prefers to wait for the price to increase a bit more. As long as [a 0 ] a 1 p holds, you can sell the info, so your actions e should preserve this formula while causing [a 1 ]¬p. To make things more difficult, say agents a 0 , a 1 are sitting next to each other.
Figure 2 (Left) models your truthful announcement of ¬p, presenting yourself as insider a ; that is, ¬p! a a1 . Intuitively, this would not preserve [a 0 ] a 1 p; and indeed, available actions would either destroy the old goal or would not be successful about the new goal.
Figure 2 (Right) models ¬p! a /f a1 : your truthful announcement that ¬p when disguised as a fortune-teller. You expect a 1 will identify you as a , while a 0 will think it common belief that you are a fortune-teller (and that no one can tell a fortune-teller is right or not). The new goal raised by this refinement is already true in any ϕ T state. So this action already constitutes a solution to the problem.
In this section we introduce non-deterministic actions into planning models, and study the corresponding logic LCC ⊗∪ . This will be used in Section 6 to find an algorithm for non-deterministic planning in this logic. First, we expand any LCC logic with action composition ⊗, and later we add choice ∪. These operations model the following executions:
composition e ⊗ f models an execution of e followed by an execution of f, and choice e ∪ f, models non-deterministic actions: each execution of e ∪ f either instantiates as an execution of e or as an execution of f.
We introduce first composition ⊗ in the action models U and define the logic LCC ⊗ , which can be reduced to LCC. Then, we will introduce choice ∪ and its semantics, the latter be based on the semantics of LCC ⊗ .
On the one hand, the introduction of composition ⊗ proceeds as usual. We will simply consider that the action model U is now closed under finite composition ⊗. To do so, we must define first the composition of an action model by itself U ⊗ U, also denoted
Definition 5. The axioms and rules corresponding to LCC ⊗ are those of LCC plus: axiom K and Necessitation for e ⊗ f and the reduction axiom:
The LCC calculus extends to LCC ⊗ using this reduction axiom. Moreover, the previous Lemma 1 extends to the general update U ⊗ with compositions e ⊗ • • • ⊗ f of at most n actions in E, for any fixed finite number n. (This is done by taking disjoint unions of update models with n compositions, for each n ≤ n.) The extensions of LCC for these compositional action models (defined by the corresponding axioms) will also be denoted LCC ⊗ . Having such a bound n on composition means in practice that we will not know a priori which LCC ⊗ is actually needed to solve the planning problem. Only after the plan search algorithm terminates, we can identify this logic. A similar remark applies to the logical extensions LCC ⊗∪ studied next.
5.2 LCC ⊗∪ : extending LCC with composition and choice. Now we will introduce the choice for actions e ∪ f, denoting an indeterminate choice between e and f. Note if the action e ∪ f is available (in A), then in general e, f will be in E but not in A. As suggested in [10], we adopt the (multi-pointed In fact, for simplicity here we only consider the case pre(e) = pre(f), for any (available) non-deterministic action e ∪ f. Also note that e ∪ f is not an action in the set E of the action model U or U ⊗ . The syntax of LCC ⊗∪ extends that of LCC ⊗ with the further type of formulas [U, E d ]ϕ, for each E d ⊆ E (whose elements have identical preconditions). In [10], the next reduction axiom was suggested for ∪:
Now we turn into strong planning for domains with non-deterministic actions, i.e. planning involving actions with (truly) disjunctive effects
(For this, let post(f 0 )(p) = post(f 1 )(q) = , and post(f 0 )(q) = q and post(f 1 )(p) = p). A strong solution for a given planning domain is a plan such that all of its executions in the initial state lead to a goal state. Thus, ignoring preconditions, the above action
and it is a weak solution if ϕ G = p.) Consider the action of tossing a coin, whose effect is heads or tails, denoted h ∨ ¬h. We represent it as a choice between two actions: toss h , toss ¬h , with postconditions post(toss h )(h) = , and post(toss ¬h )(h) = ⊥ Note both toss h and toss ¬h are deterministic actions in E, though neither of them will be in A. The reason is that they are not individually available to the agent: only toss(h)∪ toss(¬h) models this agent's abilities and hence only the latter can be used during plan search. On the other hand, e ∪ f is an element of A but not of E. For simplicity, we only define the choice between two actions f 0 ∪ f 1 . The following definitions easily generalize to the choice of finitely many actions e ∪ • • • ∪ f. First we must redefine solution for the non-deterministic case; the reasons for this are the generalization of available actions A to the non-deterministic case, and the the limited reduction axioms that characterize U, e ∪ f modalities. Definition 8. Given an action model U in LCC, let A be a set of actions e in E and actions of the form f 0 ∪ f 1 , where f 0 , f 1 ∈ E. We define a set A ⊗∪ of A-modalities in the extended language of LCC ⊗∪ as follows:
If e does not make use of (⊗R) we say it is in search form. If e does not make use of (⊗L) or (⊗R) we say it is in branching form.
See Figure 3 for an illustration of these and other modalities. Note a modality U, e in branching form essentially consists in a conjunction of LCC ⊗ modalities. The output of a plan search algorithm for LCC ⊗∪ will be an A-modality U, e in tree form. But let us define first when an A-modality is a solution for a planning domain M. Definition 9. Let the LCC ⊗∪ logic of some action model U(= U ⊗ ) be given, plus a set of available actions A. Let M = (ϕ T , A, ϕ G ) be some planning domain definable in this logic. We say an action e ∈ A ⊗∪ is a solution for M iff
The only difference with Definition 2 lies in executability: we check that every possible instantiation − → e of e does indeed lead to some state (and so, by (1), the actual instantiation will lead to a goal state). For (strong) non-deterministic planning, the idea is to reduce the search for a nondeterministic output Π to a tree of deterministic solutions Π = ({π, . . .}, ≺). With more detail, the planning domain M = (ϕ T , A, ϕ G ) will split into a tree of planning domains M ξ , each to with its own deterministic solution π ξ . For this, we need to enrich the notation π ξ = (π ξ , ϕ goals(π ξ ) ) into a 4-tuple as follows plan = ( action seq., open goals, initial state, original goals ),
The tree structure of these deterministic plans is given by the successor relation ≺. A plan π ξ and any of its successors π ξ are related by some formula they share: π ξ ≺ π ξ means that the initial state ϕ T ξ in M ξ is part of the goals ϕ G ξ for M ξ . Besides the tree structure for these components π ξ , these and their planning domains M ξ will be totally ordered by some lexicographic ordering < lex on the labels ξ. This ordering will capture the order in which planning domains π ξ are to be solved. See Figure 3 for an illustration of the lexicographic ordering of labels ξ, namely 0 < lex 1 < lex 2 < lex 21 < lex 22 < lex 221 < lex 222.
Another modification w.r.t. LCC deterministic planning concerns the Terminating Condition for plans introduced after refining with some non-deterministic action e ∪ f. For a plan of the form π ξ1 addressing the case where e ∪ f instantiates as f, we replace the condition
The reason is that we need to capture the effects of f, for which a single formula might not suffice. (Consider, for example, all the consequences of common knowledge after a public announcement). We will denote this kind of initial states as "[U, f 1 ](•)". If this kind of Terminating Condition is satisfied by π ξ1 , the resulting plan solution for M ξ1 will be defined as π ξ1 (f 1 ). under the convention that the refinement π ξ (e) will be again denoted as π ξ . While π ξ (e) is as in Def. 3 (but now a 4-tuple), the triple of new plans π ξ , π ξ1 , π ξ2 and the new partial order ≺ + are defined as follows.
plan actions open goals initial state original goals
Example 3. Let the output Π for some (ϕ T , A, ϕ G ) and A be as in Figure 3. The leftmost figure represents the output of the BFS nd algorithm, built incrementally according to the lexicographic ordering: Π = π ∅ , π 1 , π 2 , π 21 , π 22 , π 221 , π 222 . Arrows also indicate the direction of backward search, with horizontal arrows representing the introduction of a non-deterministic action.
See Figure 4 for a description of the BFS nd algorithm for non-deterministic planning. If a plan Π is the output of BFS nd , then we also call its ≺-minimal element, say π ξ2 , as π root . First we show how to translate a BFS nd output (plan set) for M into a modality U, e with e ∈ A ⊗∪ , and such that U, e is in search form. Then we show soundness of BFS nd , i.e. that U, e to be a solution for M. Definition 11. Given an output Π for a planning domain (ϕ T , A, ϕ G ), we define the modality e induced from Π as follows. First, for each
Finally, we define e = e root . Theorem 2. For any output for Π for a given M = (ϕ T , A, ϕ G ), the induced U, e modality defines a solution for M:
Now we proceed to show that BFS nd is also complete for non-deterministic planning in LCC ⊗∪ .
Lemma 2. For a given action model U and a set of available actions A, each modality U, e in A ⊗∪ is logically equivalent to a modality U, e in A ⊗∪ search form.
Using this Lemma, we may simply assume next that the solution, to be found by BFS nd , is in search form. Let us note that from Theorems 2 and 3 we can conclude that backward planning for LCC ⊗∪ logics is at least semi-decidable. For the case of (incremental) forward planning, this result is shown in [3]. To illustrate non-determinsitic planning, let us finally solve Example 1. Example 4. Recall Example 1, where the planner agent a must show heads, denoted h, to win the prize. Among the actions A of agent a, we find: getting the coin; tossing the coin; flipping the coin to heads (with precondition that a knows that ¬h); a set of announcements, including justified truthful announcements ϕ!! a b (the latter require that the announcing agent knows the truth of ϕ); and secret observations, for heads h? a and tails ¬h? a . (Their secrecy consists in b mistaking either action by skip a .) In 5(Left), the BFS nd algorithm searches first for a single plan π 0 . This particular π 0 demands ϕ goals(π 0 ) = h, and the only action possibly enforcing h is to toss the coin, which also can lead to ¬h. Refining with this action is shown in (Center). Finally, (Right) shows the output of BFS nd that solves this problem.
Before concluding, let us remark that the previous A * search for optimal planning easily extends to the non-deterministic case. Among the several possible options to define the total cost of a non-deterministic plan, consider e.g. the pessimistic and optimistic estimations based on cost(e ∪ e ) = max{cost(e), cost(e )} and cost(e ∪ e ) = min{cost(e), cost(e )} Thus, the cost of a plan is the max or min cost of its paths. For each of these cost aggregation functions max, min, one can redefine the BFS nd algorithm so that instead of stopping when the first output Π is found (with cost k), it continues search until all plans Π ∈ Plans have at least some path whose cost is ≥ k. Hence, optimal planning can be extended to strong non-deterministic planning in LCC ⊗∪ .
We presented backward planning algorithms for a planner-reasoner agent enabling this agent to find deterministic or (non-deterministic) strong plans in multi-agent scenarios. The logics considered here are dynamic epistemic logics with ontic actions, thus allowing the plans to contain communicative actions, sensing or the usual fact-changing actions. We hope the proposed work might serve for practical reasoning in communicative agents, and in particular provide a logical foundation for the modeling (and computing) of agreements among motivated agents. As for future work, several directions seem interesting: like the introduction of dynamic operators for belief revision, and at a more applied level, the study of heuristic criteria for optimal plans.
Theorem 1. BFS is sound and complete for LCC backward planning: the output π of the algorithm in Fig. 1 is a solution for (ϕ T , A, ϕ G ), and is such a solution exists, then the algorithm terminates with such an output. Acknowledgements: This work has been funded by projects AT (CSD 2007-022); Lo-MoReVI (FFI2008-03126-E/FILO FP006); ARINF (TIN2009-14704-C03-03); and the GenCat 2009-SGR-1434 and EPSRC grant EP/J002607/1.