Action representation and partially observable planning using epistemic logic

1 Introduction

Planning under incomplete knowledge and partial observabil­ ity is a tricky issue in AI, because of its computational (tem­ poral and spatial) hardness. Partially observable Markov decision processes (POMDP) are the mainstream approach to partially observable planning. Nevertheless, the applicabil­ ity of the POMDP approach is limited from the practical side as soon as the set of states has a strong combinatorial struc­ ture, rendering the number of states much too high for an ex­ plicit representation of actions, preferences, and policies. On the other hand, logical approaches to planning under incom­ plete knowledge allow for much more compact encodings of planning problems than POMDPs; most of them deal with an incomplete initial state and/or nondeterministic actions, but either they do not handle partial observability, or at least they do it in a very simple way, by assuming for instance that the set of variables is partitioned between (directly) observable and unobservable variables.

To fill the gap between POMDPs and logical approaches, an abstraction of the POMDP model (leaving aside probabili­ ties and expected utility) can be considered. It should account at least for the following elements: a set S of states; a set B of belief states built from S ; a set A of actions, where each action is associated with a transition model between states and/or belief states; some preference structure (e.g., a sim­ ple goal or a utility function); and a set 0 of observations, together with some correlation function between states and observations.

While policies for a fully observable MDP map states to actions, the output of such an abstract POMDP is a policy mapping belief states to actions; indeed, a POMDP can be viewed as a fully observable MDP over the set of belief states

Pierre Marquis

CRIL/Universite d' Artois F-62307 Lens Cedex France marquis@cril.univ-artois.fr

(this is a classical way of understanding POMDPs- and even to solve them).

In this paper, we present a rich logical framework that in­ stantiates the abstraction above, views a partially observable process as a fully observable process over belief states, and allows for expressing actions and policies in a compact way. The framework has a fairly good level of generality (since it avoids for instance to commit to a particular action language, see Section 3.1) and is therefore modular enough to be easily adapted or extended.

The simplest and best-known way of distinguishing be­ tween truths and beliefs in logic consists in expressing the problem in an epistemic or doxastic logic. To make the ex­ position simpler, we assume that the agent has accurate be­ liefs, i.e., all she believes is true in the actual world. This means that we identify belief and knowledge (since knowl­ edge is usually viewed as true belief); therefore our frame­ work is based on the logic SS and instead of belief we use the term knowledge throughout the paper. 1 SS is computation­ ally no more complex than classical logic: SS satisfiability is NP-complete [Ladner, 1977].

In Section 2 we define two notions of knowledge states: simple knowledge states (for on-line plan execution) and complex knowledge states (for off-line reasoning about the effects of a plan). In Section 3 we show how a knowledge state evolves when an action is performed. Then we show in Section 4 how to perform goal regression, and we show in Section 5 how it can be used so as to implement a sound and complete plan generator. Section 6 discusses related work.

2 Knowledge states

The language LK of propositional logic SS is built up from a finite set of propositional variables V AR, the usual con­ nectives, the logical constants T and ..1. and the epistemic modality K. SS formulas are denoted by capital Greek let­ ters <I>, 'II etc. An SS formula is objective (or modality-free) iff it does not contain any occurrence of K (i.e., it is a clas­ sical propositional formula). Objective formulas are denoted by small Greek letters <p , 'ljJ etc. and the set of all objective formulas from LK is denoted by LVAR·

1 Alternatively, we could have chosen to work with beliefs, using the doxastic logic KD45, which is very similar to S5 except that beliefs may be wrong, that is, Kcp -t cp is not an axiom. The techni­ cal issues developed in this paper would have been almost identical. Now, choosing another logic than S5 or KD45 would induce a lot of complications, including an important complexity gap.

A fundamental property of SS is that nested modalities col­ lapse, i.e., KK<I> is equivalent to Kil> and K-.Kil> to -.Kil>; for this reason, we assume without loss of generality that the scope of each occurrence of modality K in formula <I> is an objective formula.

An epistemic atom is an SS formula of the form K<p, where <p is objective. An epistemic formula is a formula built up from epistemic atoms and usual connectives: K(a V b) V -.K( c 1\ -.d) is an epistemic formula, while a 1\ Kb is not. An epistemic formula is positive iff it does not contain any occur­ rence of K in the scope of a negation: K( a V b) V -.K( c 1\ ·d) is not positive, while K(a V b) V K(c 1\ ·d) is.

S = 2VAR is the set of all interpretations of LvAR. also called states. States are denoted by s, s' etc. If <p is an ob­ jective formula, we let Mod( <p) = { s E Sis is a model of <p }.

A structure 2 for SS is defined as a nonempty set of states M ~ S. Rather than "structure", we call M a knowledge state (SKS). Intuitively, it represents all the states the agent considers possible. The satisfaction of an SS formula by an SKS M for a state s E M is defined inductively by:

• for <p objective, (M, s) I= <p iff s I= <p;
• for <p objective, (M, s) I= K<p iff Vs' E M we have (M, s') I= <p;
• (M, s) I= <I> 1\ w iff (M, s) I= <I> and (M, s) I= w;
• (M,s) I=<I>V'lliff(M,s) I=<I>or(M,s) !=W;
• (M, s) I= -.<I> iff (M, s) ~ <I>.

Finally, an SKS M satisfies <I>, denoted by M I= <I>-, iff for all s E M we have (M, s) I= <I>. An SS formula is valid (resp. satisfiable) iff it is satisfied by all SKSs (resp. by at least one SKS). An SS formula w is a consequence of an SS formula <I>, noted <I> I= W iff every SKS that satisfies <I> also satisfies W. <I> and W are equivalent, noted <I> = w iff <I> I= W and W I= <I> holds. Note that K( <p 1\ 'ljJ) is equivalent to K<p 1\ K'ljJ but K( <p V 'ljJ) is implied by but generally not equivalent to K<p V K'ljJ.

Importantly, an SKS M can be identified with the strongest epistemic atom K<p that is satisfied by M. Such a K<p is unique up to equivalence. Therefore, SKSs will be denoted syntactically, and without ambiguity, by epistemic atoms K<p.

A complex knowledge state (CKS) is a positive epistemic formula, 3 generated by epistemic atoms and the connectives

2 This semantics is equivalent (and simpler for our purpose) to the usual semantics by means of Kripke models (W, val, R) where W is a set of worlds, val a valuation function and R an equivalence relation. See for instance [Fagin et at., 1995].

3 We restrict the syntax of CKS to positive epistemic formulas because for almost all problems, ignorance can already be expressed by the fact that positive knowledge is not provable from the cur­ rent CKS. This way of generating explicit ignorance from implicit is a kind of Epistemic Closed World Assumption, already at work in [Reiter, 2001] and reminiscent of autoepistemic logic; its principle can be roughly be stated as "if I cannot prove that I know cp then I don't know cp". However, for the purpose of this paper, we do not need this completion because the set of valid plans from a CKS and the set of valid plans from its completion coincide.

1\ and V . For instance, [K(a V b) 1\ K-.c] V K(b ++ c) is a CKS but K(a V b) -+ Kc is not, -.Ka neither.

Example 1 In a model-based diagnosis context, let 1: = /\cECOM p K( ·ab(c) ++ <fJc) the formula representing the behaviour of a set of components COM P. Suppose that the agent is performing a test plan so as to identify the faulty com­ ponents. The formula characterizing the condition for stop­ ping performing tests and starting reparing the faulty com­ ponents is <I> = 1\cECOMP(Kab(c) V K-.ab(c)). The latter formula is a CKS. It is equivalent to an exponentially large disjunction of SKS: <I> = V{K61 I I ~ COMP} where 61 =(/\eEl ab(c)) 1\(1\cECOMP\f -.ab(c)).

A CKS <I> is said to be in epistemic disjunctive normal form (EDNF) iff it has the form K<p1 V ... V K<pn, where each <p; is an objective formula. Clearly, every CKS has an equivalent EDNF.

3 Actions and progression

In general, actions have both physical (or antic) and epistemic effects, i.e., they are meant to change both the state of the world and the agent's knowledge state, but without loss of generality we assume (as usually in AI) that any "mixed" ac­ tion can be decomposed into two actions, the first one having only ontic effects and the second one only epistemic effects. For instance, the action of tossing a coin is decomposed into a blind-toss action followed by a see action telling the agent whether the coin has landed on heads or on tails.

3.1 Ontic actions

Ontic actions are meant to have effects on the world outside the agent, especially physical effects such as moving a block, switching the light, moving etc. They are assumed to be de­ scribed in a propositional action language (allowing or not for nondeterminism, for ramifications/causality). Any action language LA can be chosen, provided that it is propositional and that it expresses the effects of an action a within a for­ mula :Ea involving atoms labelled by t and atoms labelled by t + 1 (the former for the state before the action is performed, the latter for the state after it is performed). Among candi­ date languages we find those of the A family [Gelfond and Lifschitz, 1993], "propositionalized" situation calculus [Lin, 2000] and causality languages [McCain and Turner, 1998]. 4

The description :Ea of an action a allows for comput­ ing the successor state of a state s (or the set of successor states if a is nondeterministic). This set is represented by any objective formula prog(s, a) (whose models form the set of successor states). This definition extends to sets of initial states, or equivalently to propositional formulas, by prog(<p, a) = V sEMod(cp) prog(s, a).

Now, given the description :Ea of action a and a CKS <I>, the subsequent CKS, denoted by Prog(il>,a), is defined as follows:

4 The common core of these languages is the use of explicit or implicit successor state axioms. These languages coincide for deter­ ministic, ramification-free actions and differ in the way they treat nondeterminism (using for instance exogeneous variables or Re­

lease statements), ramifications, etc.

Definition 1 (progression for ontic actions) Let a be an antic action and let ~ = Kcp1 V .. . V K cpn be a CKS in EDNF.

The problem with the latter definition is that the CKS has to be put in EDNF first. This does not induce any loss of ex­ pressivity but the transformation may be exponentially large so that we may want to compute the successor CKS directly from a CKS expressed in any form, such as in Example I.

We now give a more elegant way of computing progression via an extension of variable forgetting to 85 formulas. We recall first from [Lin and Reiter, 1994] the inductive definition of forget(X, cp ) where cp is objective and X ~ V AR:

Definition 2 (forgetting) Let ~ be an 85 formula and X ~ V AR. Forget(X, ~)is the strongest 85formula (a) entailed by ~ and (b) not mentioning any variable of X.

Forget( ., . ) is well-defined, because the set of formu­ las satisfying (a) and (b) is closed by conjunction. Thus Forget( X, ~) is unique up to equivalence in 85.

Proposition 1

• If~ is a CKS, then Forget(X, ~)is a CKS.
• Forget(X, ~1 V ~2 ) = Forget(X, ~1 ) V Forget(X, ~2).
• Forget(X, Kcp) = Kforget(X, cp).
• If ~ 1 and ~2 do not share any variable then Forget(X, ~ 1 1\ ~2 ) = Forget(X, ~I) 1\ Forget(X, ~2 ) .

The interest of defining this forgetting operator is made clear by the following result. From every symbol x E V AR we make two copies Xt, Xt+I, where t (resp. t + 1) represents the time point before (resp. after) the action is performed; then, for any formula cp E .C v AR, 'Pt (resp. 'Pt+I) is the formula from cp obtained by replacing each variable x by Xt (resp. Xt+I ).

Proposition 2 Let a be an antic action and let ~ be a CKS. We have:

where V ARt= {xt I x E V AR}.

3.2 Epistemic actions

An epistemic action f3 is described wlog by the finite set of its possible outcomes { o1 , ·.· , op} ~ 0, where each Oi is an objective formula describing a possible observation, and o1 V .. . Vop is a tautology. 6 Accordingly, we have 0 = .C v AR in our framework. The effects of f3 are motivated by the fol­ lowing principles: non-intrusiveness (for any objective for­ mula cp, if cp holds before f3 is performed, then it still holds after), no-forgetting (if the agent knows an objective formula cp before performing /3 , then she still knows it after) andre­ liability (if the agent observes o1 after performing /3 , then o1 holds, so that she knows o1 after observing it). These three properties imply that the effects of an epistemic action asso­ ciated with the outcome set { o1 , . . . , op} can be represented by the following progression operator:

5 In (1), 'Px<- T (resp. 'Px<-.L) represents the formula obtained by replacing in rp each occurrence of variable x by T (resp . ..i).

6 0r, more generally, L: f= 01 V .. . V Op , where L: is the given set of static domain rules.

Definition 3 (progression for epistemic actions) Let f3 be an epistemic action associated with the set of outcomes { o1 , .. . , op}, and let~ be a CKS. We have:

It follows that for any epistemic actions /3 , /31 , /32 and a CKS ~,progression is indifferent to the order of epistemic ac­ tions: Prog(Prog(~ ,/31) ,/32 ) = Prog(Prog(~ ,/32 ) ,/31 ); it is idempotent: Prog(Prog( ~ , /3 ), /3 ) = Prog( ~, /3 ); and it preserves positive knowledge: Prog( ~ , /3 ) f= ~ .

Epistemic actions can be assumed fully executable without loss of generality (adding new symbols if necessary). 7

A simple and well-known cla'ss of epistemic actions is the class of binary tests, also called truth tests: if cp is an ob­ jective formula, the action test( cp) is defined by the out­ come set { cp , -,cp}. Therefore we have Prog( ~ , test( cp)) = ~ 1\ (Kcp V K -,cp). In the rest of the paper, we focus on truth tests, which will make things simpler to expose. 8

Note that a straightforward (but important) consequence of Definitions 1 and 3 is that the set of all CKS is closed under progression, i.e., if~ is a CKS and a is an (on tic or epistemic) action, then Prog(~ , a) is a CKS.

4 Regression

The problem is stated as follows: given a CKS ~ (represent­ ing a goal knowledge state) and an (ontic or epistemic) action a, characterize the weakest CKS denoted by Reg(~ . a), in which performing a leads to a CKS satisfying ~.

Definition 4 (regression) Let a be an (antic or epistemic) action and let ~ be a CKS. The regression of ~ by a, is the unique CKS (up to logical equivalence), denoted by Reg(~, a), such that (a) Prog(Reg(~, a) , a) f= ~ and (b) for any~~ such that Prog(~ 1 ,a) f= ~we have~~ f= Reg(~, a).

This definition is well-founded: indeed, if Prog( ~ 1 , a) f= ~ then for any ~2 f= ~I we have Prog(~2, a) f= ~ (this is easily verified both for ontic actions and for epis­ temic actions). Therefore the set {w I Prog('ll, a) f= ~} is closed w.r.t. disjunction, which entails that there exists a weakest w such that Prog('ll, a) f= ~. equivalent to V{21 Prog(2, a) f= ~} .

7 Note that actions that may fail to be informative can only be expressed here by the occurrence of a tautology in their outcomes. In this case, unfortunately, we get that Prog(if?,/3) =if?, because Ko1 V . .. V Kop = T as soon as o; = T for some i .

8 This does not induce any loss of generality, because any epis­ temic action can be rewritten equivalently into a logarithmic se­ quence of binary tests, together with the addition of some domain constraints.

4.1 Regression for ontic actions

For any objective formula cp and any ontic action a, let reg(cp, a) be the standard (non-epistemic) regression of cp by a, i.e., any objective formula whose set of models consists of all states s E S s.t. Mod(prog(s,a)) <;;; Mod(cp) [Reiter, 1993].

Definition 5 (sufficient success conditions) A consistent conjunction of literals 1 is a sufficient success condition for a and cp if and only if for any pair of states (s, s') E S x S such that sis a model of! and s' is a model ofprog(s, a), s' is a model of cp. 1 is a minimal sufficient success condition for a and cp if and only if it is a sufficient success condition for a and cp and no proper subconjunction of 1 is. We denote by f( a, cp) the disjunction of all minimal sufficient success conditions for a and cp.

When actions are described using an action language satis­ fying the properties stated in Section 3.1, such conditions can be computed abductively. Clearly, 1 is a sufficient success condition for a and cp if and only if It 1\ La is satisfiable, and every model of It 1\ La is a model of 'Pt+I·

Proposition 3 Let La be the description of a in a proposi­ tional action language LA. reg(cp, a) is equivalent to

In this proposition, Pli{"AR,((cp)t+I) denotes the set of prime implicants of the formula La -+ (cp)t+I that are con­ sistent with La and built up from variables of V ARt. only.

The latter abductive characterization of on tic actions is in­ dependent of the action language chosen -and it now allows for characterizing the regression of complex epistemic states by an ontic action.

Proposition 4 Let a be an antic action, II> a CKS and let Kepi V ... V Kcpn be an EDNF formula equivalent to 11>. Then

4.2 Regression for epistemic actions

Proposition 5 Let f3 be an epistemic action whose outcome set is { 01, ... , op} and let II> be a CKS. Let Kepi V ... V Kcpn be any EDNF formula equivalent to 11>. Then equivalent to Vk E l..q, :Ji, j E l..n s.t. ok 1\ 'lj; -+ cp; and Ok 1\ -,'lj; -+ 'Pi are classically valid, which is equivalent to: Vk E l..q, :Ji,j E l..n s.t. ok-+ (('lj;-+ cp;) 1\ (...,'lj;-+ 'Pi)) is valid. The rest of the proof is easy. ·

Example 2 Consider the epistemic actions a = test(u 1\ v) and (3 = test( u +-t v ), and the antic action 1 that switches the value of u, thus described by ( ut+ 1 +-t -,ut) 1\ ( Vt+ I +-t vt). Let II> = Kv V K-,v. Applying Proposition 5 we get Reg( I!> , a) = Kv V K...,v V K(v -+ u) V K(v 1\ -,u) = Kv V K(v -+ u); Reg( I!> , (3) = Kv V K-,v V Ku V K-,u; Reg(Reg(IJ>, a), (3 ) = K(u -+ v) V K(v -+ u). Applying Proposition3wegetReg(11>, !) =II>, Reg(Reg( IJ> ,a),!) = Kv V K(v -+ -,u); Reg(Reg(l!> ,/3),!) = Reg(l!> , /3); Reg(Reg(Reg(IJ>, a), (3), 1) = K(u V v) V K(-,u V -,v).

5 Plan generation

Definition 6 (planning problems) A planning problem P w.r.t. a propositional action language LA consists of an SKS II> = Kepi nit describing the initial knowledge state of the agent, afinitesetofactionsA = Ao (ontic)UAe (epistemic) and a CKS f describing the goal. Effects of antic actions are described in LA.

The reason why r is a CKS is that it is not sufficient to reach the goal, it must also be the case that the goal is known to be reached. r may be purely epistemic goal such as Kcp V K ...,cp, i.e., an agent may have the ultimate goal to know whether cp holds or not.

Plans are defined inductively as follows:

• the empty plan >. is a plan;
• any action (ontic or epistemic) is a plan;
• if 1r and 7r 1 are plans then 1r; 1r 1 is a plan;
• if 1r and 7r 1 are plans and II> a CKS, then if II> then 1r else 1r 1 is a plan.

Therefore, a plan can be seen as a program without loops, whose branching conditions are epistemic formulas : the agent can decide whether she knows that a given objective formula is true (whereas she is not always able to decide whether a given objective formula is true in the actual world) .

In particular, if f3 = test( 'lj;) is a binary test then

Sketch of proof We give it in the latter case only (the proof for the general case is similar). We abbreviate Reg( II>, (3) by ~. We first establish (the proof is omitted) that ~ is necessarily a CKS, i.e ., ~ = Koi v ... v Koq . Now, I= ~ 1\ (K'Ij; V K ...,'lj;) -+ II>

At that stage, we make use of the following lemma: for any objective formulas A, Band C, KA-+ (KB V KC) is valid (in S5) iff A -+ B is valid or A -+ C is valid. (*) is then While CKS are relevant for off-line planning, i.e., for rea­ soning about the possible effects of a plan, they are no longer relevant for representing knowledge during plan execution, state.

Definition 7 (progression of a CKS by a plan)

The progression of a CKS II> in EDNF by a plan is defined inductively by

1. Prog(IJ>, >.)=II>;

Definition 8 (valid plans) A plan 1r is a valid plan for the planning problem P if and only if Prog(<p, 1r) I= r.

Exemple 2 (cont'd) Initially, the agent does not know the values of u and v (her initial knowledge state is KT ), and her goal is to reach a belief state where she knows the value

ofv: r = Kv V K-.v. Let 1r = /3; if K(u +-+ v) then n else(!; n) be a plan. We have: Prog(KT, 1r) = Prog(Prog(KT, j3), if K(u +-+ v) then n else(!; n)) = Prog(K(u +-+ v), n) V Prog(K(u +-+ ·v) , (!; n)) = K(uA v) VK(·uA·v) Therefore, 1r is valid.

A valid plan can be computed by the following backward algorithm based on goal regression which is reminiscent of dynamic programming. The current goal <pc, expressed in EDNF, is initialized as r. Then we nondeterministically pick an action nand compute Reg(ipc, n). The current goal is then updated by <pc := <pc V Reg(ipc, n). The process is iterated until K<pinit I= <pc or it is not possible to im­ prove <pc anymore. Since there is a finite number of possible belief states, the algorithms stop and returns a valid plan, if such a plan exists. An ordered list L is constantly up­ dated, initialized by ((KG1, >.), ... , (KGm, >.)) where r ::::: KG1 V . . . V KGm; each time a new disjunct (i .e., not sub­ sumed by any previous disjunct of <p 0 ) K'ljJ is added to <p 0 after regressing by action n, the pair (K'l/J, n) is added to L.

There are two slightly different possible outputs: (1) either the output is just L, i.e., an ordered knowledge-based pro­ gram (or decision list): at execution time, when observations are made, the new knowledge state is computed, then we look for the leftmost (K'ljJ, n) in L such that K'l/J is true in the cur­ rent knowledge state and n is performed; (2) or the output is a ready-to-use conditional plan computed by "simulating" possible executions from K<pinit to r using L.

Exemple 2 (cont'd) Regressing by a, 1 and then j3, the algorithm finds a valid knowledge-based program for r: L = ((Kv, >.) , (K·v, .A) , (K(v-+ u) , n), (K(v-+ ·u),/), (KT, /3) ). An associated conditional plan is 1r = /3; if K(u +-+ v) then n else(!; n).

6 Related work

Knowledge-based programs In the planning community, the idea of using explicit knowledge preconditions for ac­ tions and plans comes back to [Moore, 1985; Morgenstern, 1987]. Developed in a different perspective (agent design), knowledge-based programs [Fagin eta!., 1995; Brafman et a!., 1998; Herzig eta!., 2000; Reiter, 2001] are high-level pro­ tocols that describe the actions an agent should perform as a function of her knowledge. Thus, in a knowledge-based pro­ gram, branching conditions are epistemically interpretable, and plans explicitly involve deduction tasks during on-line execution Uust like in our framework). Actually, the output of our plan generation process is a knowledge-based program. Therefore, our work can be seen as an upstream task that generates a valid knowledge-based program from a compact specification of action effects and goals.

Action languages A number of works have extended action languages so as to handle explicit knowledge and partial ob­ servability, especially [Lobo et a!., 1997; de Giacomo and Rosati, 1999; Bara1 and Son, 200 I]. Knowledge is repre­ sented in all cases by an explicit or implicit epistemic modal­ ity (plus a "minimal knowledge" semantics in [de Giacomo and Rosati, 1999]). The line of work most related to ours is of [Baral and Son, 2001]; indeed, not only they represent epistemic actions with an epistemic modality but they also allow for conditional plans with epistemic branching condi­ tions. Our work can be seen as an extension of theirs: 9 (i) our formalism is general enough to accept any propositional action language (including those handling causal rules) for representing the effects of ontic actions); (ii) our syntax is less restricted, since we allow for any and-or combination of SKS (i .e., CKSs) while they consider SKS only; as ar­ gued in Section 3, this makes the representation more com­ pact, when reasoning at planning time about the future con­ sequences of actions; (iii) our progression and regression op­ erators have significant computational characterizations (e.g., ontic regression has an abductive characterization); lastly, we have a sound and complete algorithm for plan generation.

Planning under partial observability There is a number of recent approaches for logic-based plan generation under par­ tial observability.

[Bonet and Geffner, 1998] give a high-level language for describing action effects on both the world and the agent's beliefs. Their language is a decidable fragment of first-order logic. By describing ontic actions with successor state ax­ ioms, they allow for handling the frame problem and ram­ ification problems. After a problem has been represented in their language, its description is automatically translated into a POMDP model and solved by using POMDP algo­ rithms, so that there is no need to define progression and re­ gression directly in the logic, nor to have an explicit knowl­ edge modality: this is the main difference with our approach, where the compact logical representation is kept and propa­ gated throughout the process.

The next three approaches solve the plan generation prob­ lem directly in a high-level language but, on the other hand, they all make important restrictions that lead to a loss of ex­ pressivity. These restrictions imply that none of these ap­ proaches makes use of action languages, while ours can ben­ efit from the huge amount of work in this area and accord­ ingly, can handle the frame problem as well as ramification and causality in the best possible way while maintaining com­ putational complexity at a reasonable level.

[Bacchus and Petrick, 1998; Petrick and Bacchus, 2002], like us, use an epistemic modality. Apart from the repre­ sentation of ontic actions (less expressive than ours due to the abovementioned point 10 ), they restrict the syntax of epistemic formulas (for instance, simple disjunctive beliefs such as K(avb) cannot be expressed) and consequently, as they no­ tice, their algorithm sometimes fails to discover a valid plan.

9 Actually, only of the first part of [Baral and Son, 2001], since the second half of their paper gives a detailed study of sound and efficient approximations of their formalism. We plan to integrate similar approximations in our framework.

10 0n the other hand, they use a fragment of first-order logic which allows for expressing some actions (such as value tests) elegantly, and they motivate their expressivity restrictions by efficiency con­ siderations, so that their approach is a good trade-off between effi-

The approaches [Bertoli et al., 2001; Rintanen, 2002] do not make use of an epistemic modality, and therefore can­ not explicitly express disjunctions of belief states (i.e., CKSs) or complex knowledge-based programs. The representation of belief states in both approaches uses BDDs, which al­ low for a compact representation but not as space efficient as DAG-based propositional formulas. While the algorithm in [Bertoli et at., 2001] uses progression (based on model check­ ing), [Rintanen, 2002] has a regression operator, and, inter­ estingly enough, his combination operator ® between belief states (which aims at computing, given two belief states Bl and B2, the maximal belief states in which, after observing the values of observable variables, leads to know that the true state is in Bl or to know that the true state is in B2) can be reformulated using our epistemic regression (Section 4.2) 11 and thus epistemic logic helps understanding how and why this operator works. 12

Situation calculus [Scher! and Levesque, 1993] represent sensing actions in the situation calculus by means of an ex­ plicit accessibility relation between situations (which means that knowledge is treated as an ordinary fluent) which cor­ responds exactly to the semantics of our epistemic modality (once situations have been identified with states). Our ap­ proach expresses the problem at the formula level and en­ ables thus a more concise representation and can benefit from existing complexity and automated deduction results for S5. Levesque [Levesque, 1996] builts on the above framework towards a general theory of planning with sensing, handling complex plans involving, like ours, nondeterrninism, obser­ vations and branching (and also loops).

Acknowledgements

The third author has been partly supported by the IUT de Lens, the Universite d' Artois, the Region Nord I Pas-de­ Calais under the TACT-TIC project, and by the European Community FEDER Program.