Logical Filtering

1 Introduction

Any agent operating in a partially observable environment must perform computations that distinguish among the a pri­ ori possible current states of the world on the basis of past ob­ servations and actions. These computations may operate di­ rectly on a representation of the action-observation sequence (e.g., [Winslett, 1990; Kautz et al., 1996]); they may reduce queries about the current state to queries about the initial state (e.g., [Reiter, 2001 ]); or, they may update the belief state (the agent's knowledge about the state of the world) after each ac­ tion and observation. This latter approach, called filtering or recursive state estimation in the control theory literature, is particularly useful with unbounded sequences of actions and observations.

The main computational difficulties are 1) the time needed to update the belief state, and 2) the space required to repre­ sent it. These depend on the nature of the transition model, which describes how the environment evolves over time, the observation model, which describes the way in which the en­ vironment generates observations, and the family of repre­ sentations used to denote belief states. Early work, begin­ ning with Gauss, assumed stochastic models. For example, the Kalman filter [Kalman, 1960] is a ubiquitous device that maintains a multivariate Gaussian belief state over n vari­ ables, assuming linear-Gaussian transition and observation model. Crucially, the O(n 3 ) update cost and the O(n 2 ) space requirement do not depend on the length of the observation sequence; hence, a Kalman filter can run indefinitely. In this paper, we are interested in developing analogous results in the context of logical representations.

We adopt a simple logical language (Section 2) for describ­ ing the transition and observation models; the observations and the belief state itself are also logical formulae. The ini­ tial state may be only partially known; the transition model, which allows for actions by the agent itself, may be nondeter­ ministic; and the observation model may be nondeterministic and partial, in the sense that the agent may not be able to observe the actual state.

Even when we restrict ourselves to propositional logic, it is clear that the general filtering problem is nontrivial (we prove it is computationally hard), because there are exponen­ tially many possible states. We identify several classes of models that allow efficient filtering with respect to the belief­ state representation size. Our primary method is based on decomposition theorems showing that 1) filtering distributes over disjunction in the belief state formula, and 2) filtering distributes over conjunction and negation if the actions are permutations of the state space. Such actions serve as one-to­ one mappings between states, for those states in which they can be applied. We obtain efficient, exact algorithms for DNF belief states and for NNF (Negation Normal Form- all nega­ tions are in front of atoms) and CNF belief states with per­ muting actions. In other cases, we obtain efficient algorithms for approximate filtering.

In another class of dynamic systems, we can filter effi­ ciently if the belief state is represented in CNF that includes all its prime implicates. Finally, we show that STRIPS mod­ els (possibly with nondeterministic effects of actions) also ad­ mit efficient filtering. The STRIPS assumption, that every action has no conditional effects and that an effect's precon­ ditions are the preconditions for the action's execution, is key to this efficiency.

With respect to maintaining a compact representation, we show that properties similar to those mentioned above allow us to filter k-CNF formulae (CNF with clauses of at most k literals, when k is fixed) such that the result is represented in k-CNF (for the same fixed k). Thus, the belief state is main­ tained in O(nk) space indefinitely. In particular, we show mild conditions under which a compact belief state can be maintained in nondeterministic STRIPS domains and in per­ mutation domains. Finally, we show that DNF belief states remain compact if the effects of actions are deterministic and guaranteed to hold. These results are the first analogues, in the logical arena, of the desirable properties possessed by Kalman filters for continuous variables.

Ours is by no means the first work on filtering in a logical context. Early on, it was pointed out that filtering is easy for deterministic systems with a known initial state [Fikes et al., 1972; Lin and Reiter, 1997]. Filtering in nondeterministic domains is more difficult. In particular, the related problem of temporal projection is coNP-hard when the initial state is not fully known, or when actions have nondeterministic effects [Liberatore, 1997] (see also Section 3.3).

Traditionally, computational approaches for filtering take one of three approaches: 1) enumerate the world states possi­ ble in every belief state and update each of those states sep­ arately, together generating the updated belief state [Ferraris and Giunchiglia, 2000; Cimatti and Roveri, 2000], 2) list the sequence of actions and observations and prove queries on the updated belief state [Reiter, 2001; Sandewall, 1994], or 3) approximate the belief state representation [Son and Baral, 2001; Williams and Nayak, 1996].

The first two approaches cannot be used when there are too many possible worlds (e.g., when the domain includes more than a few dozens of fluents and there are more than 2 40 pos­ sible states) or when the sequence of actions is long (e.g., more than 100 actions). Examples include robot localization, tracking of objects and their relationships, and data mining. The third approach gives rise to many mistakes that are some­ times dangerous, and requires an approximation that fits the given problem (if one exists). Many domains of 100 fluents or less are still computationally infeasible for it.

2 Logical Filtering

In this section we define logical filtering using a transition model and action semantics that are compatible with the stan­ dard semantics belief update operator of [Winslett, 1990]. (To avoid confusion, this is different from another operator presented in the same publication, PMA, that applies a non­ monotonic approach to formalize minimal change.) This op­ erator is simple and allows us to examine computational prop­ erties easily. It can represent any logical transition system, and specifications in other action languages can be compiled into it [Winslett, 1990; Doherty et al., 1998].

In what follows, for a set of propositional formulae, w, L(w) is the signature of w, i.e., the set of propositional sym­ bols that appear in w . .C(w) is the language of w, i.e., the set of formulae built with L(w). Similarly, .C(L) is the language of L, for a set of symbols L.

A transition system is a tuple (P, S, A, R), where

• P is a finite set of propositional fluents;
• S ~ Pow(P) is the set of world states;
• A is a finite set of actions;
• n ~ s X A X s is the transition relation.

The intuition for this transition system description is that P is the set of features that are available for us in the world, every element inS is a world state (i .e., a subset of P, containing propositions that are true in this world state), A is the set of actions in the system and R(s, a, s') means that state s' is a possible result of action a in state s.

A belief state is a set of world states a ~ S. Performing an action a in a belief state a results in a belief state that includes all the world states that may result from a in a world state in a. We do not introduce observations in this transition model. Instead, we assume that observations are given to us (if at all) as logical sentences after performing an action.

A logical nondeterministic domain description D is a fi­ nite set of statements of the following kinds: value proposi­ tions of the form "initially F" describe the initial state and effect rules of the form "a causes F if G" describe the effects of actions, for F and G being state formulae (propositional combinations of fluent names). We say that F is the head and G is the tail of those rules.

For a domain description D we define P D, AD to be the set of propositional fluents and actions mentioned in D, respec­ tively. For a domain description D we define a transition relation Rv(s, a, s') as follows.

• A fluent f E PD is possibly affected by action a in state s, if there is a rule "a causes F if G" in D such that G is true ins and f E L(F).
• Let I (a, s) denote the set of fluents in P D that are not possibly affected by action a in state s.
• Let F( a, s) be a set of all the heads of activated effect rules in s (i .e., if "a causes F if G" is activated in s, then FE F(a, s)). We consider the case of F(a, s) = 0 (no activated effect rules) as F( a, s) = TRUE.
• Define (recalling that world states are sets of fluents)

When there is no confusion, we writeR for Rv.

If action a has an effect of FALSE ins, then it cannot execute.

In partially observable domains, we update our knowledge as a result of executing an action and collecting observations in the resulting state. The following definition of filtering as­ sumes that a is a set of world states. We use our transition operator n to define the resulting belief state from each ac­ tion. An observation o is a formula in our language.

Definition 2.1 (Logical Filtering Semantics). Let a ~ S be a belief state. The filtering of a sequence of actions and observations (a1, o1, . . . , at , Ot) is defined as follows:

1. Filter[E](a) =a;
2. Filter[a](a) = {s' I (s,a, s') En, sEa};
3. Filter[o](a) ={sEa I o is true ins};

We call Step 2 progression with a and Step 3 filtering with o.

For example, consider a robot that is in charge of cleaning a room. It can execute an action a = fetch( broom, closet) which has the single effect rule "a causes has( broom) A ·in( broom, closet) if in( broom, closet)". Assume that the robot's belief state is a = Pow(P) (i.e., it consid­ ers all states possible). Then, Filter[a](a) = {s E

Pow(P) I -.in(broom, closet) is true ins}, i.e., after per­ forming the action a we consider all worlds that satisfy ·in( broom, closet) possible. This is because if we are ini­ tially in a state in which in( broom, closet), then the resulting state is one in which -.in( broom, closet), and if we are ini­ tially in a state in which -.in( broom, closet), then we stay in the same state (thus, still satisfying -.in( broom, closet)). Call this resulting belief state u'. Now, if an observation o =has( broom) is received, then Filter[o](u') is exactly the set of worlds that satisfy ·in( broom, closet) and has(broom ).

3 Filtering Logical Formulae

Approaches to filtering actions and observations that at any stage enumerate the states in a belief state do not scale to large domains. An alternative approach is to perform logical progression in a form similar to the one described by [Lin and Reiter, 1997; Mcllraith, 1998]. The difference is that now we wish to do so (efficiently) in the context of nondeterministic actions and observations.

In this section we present a straightforward algorithm that filters belief state formulae directly, but does so in worst-case exponential time. This algorithm serves as a starting point for Section 4, where we propose efficient algorithms. We also present distribution properties of filtering over the log­ ical connectives 1\, V, -., and examine the theoretical limita­ tions of formula filtering. These will guide us in Section 4, and allow us to present classes of systems that are not subject to those limitations and can be tracked in polynomial time and a compact fashion indefinitely.

3.1 Zeroth-Order Filtering Algorithm

In the rest of the paper we assume that a fixed set of fluents persists for action a in all states in which it has an effect. Eff( a) is the set of fluents possibly affected by a, and Ejj{ a) is P \ E.ffi.. a). Some of the following notation assumes an implicit action, when this causes no confusion.

We represent a belief state u as a logical formula cp such that a state is in u iff it satisfies cp. The filtering of a belief state formula with an action and an observation is a formula representing the consequences of our effect rules and obser­ vation on states that satisfy our initial formula. We specify this filtering process formally using the following notation.

For a set of effect rules r 1 , ... , r1 for action a, each of the form "a causesFi ifG/', write Ff = Fi[P/P'l· for 'P' = {f{, ... , f~} a set of new symbols for fluents, [PIP'] a shorthand for [hI f {, ... , f n If~], and [f If'] means that we replace all instances of symbol f in the formula by instances of symbol f'. Here, we view P as the set of fluents in some time t, and P' as the same fluents in time t + 1. We add the following set of rules for action a:

the assertion that no precondition of a holds. This has a sim­ ilar effect to adding frame axioms to a set of effect axioms in an action language. We let r 1 , ... , r m be the complete set of rules for a and call the new rules, C = {r1+1 , ... , rm}, com­ pletion rules for a.

We filter a belief-state formula as follows. (We reuse Filter[·](·) for filtering a belief-state formula.) Let Cn(w) be the set of logical consequences of\[! (i.e., formulae 1/J such that\[! f= 1/J), and Cn.c(w) be Cn(w) n .C, the set of logical consequences of\[! in the language .C. We write CnL(w), when Lis asetofsymbols, to mean Cn.C(L)(Ilf).

For example, consider action a = fetch(broom, closet) which has the single effect rule "a causes has(broom) 1\ ·in( broom, closet) if in( broom, closet)", and consider a be­ lief state formula cp = TRUE (i.e., we consider all states possible). Then, Filter[a](cp) = -.in(broom,closet), i.e., after performing the action a we consider all worlds that satisfy -.in( broom, closet) possible (similar to our example in Section 2). Call this resulting belief state formula cp'. Now, if an observation o = has(broom) is received, then Filter[o] ( cp') = -.in( broom, closet) 1\ has( broom).

The following generalizes a theorem presented in [Doherty eta!., 1998] by allowing conditional and inconsistent effects.

Theorem 3.1. If cp is a belief state formula, and a an action, then

Our zeroth-order algorithm computes Filter[ (a1 , o1 , ... , ae, ot)] ( cp) by iterating the appli­ cation of filtering of a belief-state formula with an action and an observation. It sets cp0 cp and Cf)i = Filter[oi](Filter[ai](cpi- I)) recursively fori > 0 using the two equalities defined above. This algorithm is correct, as shown by Theorem 3.1. It can be implemented using a consequence finder in a restricted language (e.g., [Simon and del Val, 2001]).

From here on, when we say filtering we refer to filtering of a belief-state formula, unless otherwise mentioned.

3.2 Distribution Properties and Permutation

We can decompose the filtering of a formula cp along logical connectives once we establish several distribution properties.

Theorem 3.2 (Distribution over Connectives). Let a be an action, and let cp, 1/J be formulae. Then,

1. Filter[a](cp V 1/J) = Filter[a](cp) V Filter[a]('lj;)
2. f= Filter[a](cp 1\ 1/J) => Filter[a](cp) 1\ Filter[a]('lj;)
3. f= Filter[a](·cp)-¢::: -.Filter [a](cp)I\Filter[a](TRUE)

We can say something stronger for actions that act as permutations on the states in S in which they can be executed.

Definition 3.3 (Permuting Actions). Action a is permuting, if for every states' there is at most ones such that R(s, a, s').

Domains that include only permuting actions are called permutation domain.

For example, consider a = fetch( broom, closet) from above, and assume that we add a second effect rule "a causes FALSE if -,in( broom, closet)". Thus, a is not exe­ cutable unless its first rule's precondition holds. Then, the ac­ tion is a one-to-one mapping between states, when this map­ ping is defined (it is not defined when a state maps to no re­ sulting state). If this second rule is not added, then the action is not one-to-one because it maps two different states (in the first we already have the broom and in the second the broom is in the closet) to the same state.

In the same spirit, an action pickUp( A, B) that picks up block A from the top of block B is one-to-one when it is pos­ sible because we can find a single previous state for every resulting state. The same holds for putDown(A, C) . Other natural examples include turning a row in a Rubik's cube, flipping a light switch, and buying a gallon of gas. In con­ trast, turning on the light, setting a Rubik's cube to a partic­ ular configuration, and filling up the gas tank are not permu­ tation actions. Notice that we allow different actions to map different states to the same state (e.g., accelerating by 5MPH when driving 40MPH results in the same state as when decel­ erating by 5MPH when driving 50MPH).

Theorem 3.4 (Distribution for Permutation Domains). Let a be a permuting action, and let <p, '1/; be formulae. Then,

1. Filter[a](<p 1\ '1/;) = Filter[a](<p) 1\ Filter[a]('!f;)
2. Filter[a](<p V '1/;) = Filter[a](<p) V Filter[a]('!f;)
3. Filter[a](...,<p) = --,Filter[a](<p ) 1\ Filter[a](TRUE)

Proof Sketch. Space permits inclusion only of the most inter­ esting part, i.e., that of"¢=" of 2.

Let s' be a world state that satisfies Filter[a] ( <p) 1\ Filter[a]('!f;). Then, it satisfies both of Filter[a](<p), Filter[a]('!f;). For Filter[a](<p) there is a states such that RD(s, a, s') and s satisfies <p. Similarly, for Filter[a]('!f;) there is a state s 1 such that RD(s1 , a, s') and s 1 satisfies '1/J . However, since a acts as a one-to-one mapping from S to S, there is only one state inS that a maps to s'. Thus, s = s1, and s satisfies '1/;. Thus, s satisfies <p 1\ '1/; and s' sat­ isfies Filter[a] ( <p 1\ '1/; ). From Theorem 3.1 it follows that f= Filter[a](<p 1\ '1/;) {= Filter[a](<p) 1\ Filter[a]('!f;). 0

3.3 Limitations for Compact Representation

It may be argued that filtering may require only polynomial space, if we limit ourselves to initial belief states that are rep­ resented compactly and to actions whose effects and precon­ ditions are represented compactly. In Theorem 3.5 we show the contrary. That is, for every general-purpose representa­ tion of belief states there is a dynamic system, an initial be­ lief state, and a sequence of actions after which our belief state representation is exponential in the representation of the initial belief state.

P/poly is a nonstandard computational complexity class that includes problems that can be answered in polynomial time, if we are given a polynomial-length hint that depends only on the length of the input problem. It is considered likely that NP n co-NP ~ P/poly. Assume so, and let j(<T) (<1 ~ 2 5 ) encode belief states using n propositional symbols.

Theorem 3.5. There is dynamic system D with nfluents, be­ lief state <To, and action sequence a1 , . . . , an such that, for all i :::; n, <Ti = Filter[ai](<Ti-1) . and lf(<Tn)l > poly(if(<To)l · IDI · n). ~DI is the representation size of D.)

The proof of this theorem reduces the problem of repre­ senting the belief state after performing an action to that of representing a Craig Interpolant. It uses the following.

Theorem 3.6 ((Boppana and Sipser, 1990)). Assume that for every propositional implication A f= B there is a Craig interpolant C such that A f= C and C f= Band ICI < poly(IAI + lEI). Then NP n co-NP ~ Plpoly.

4 Efficient and Indefinitely Compact Filtering

In this section we present the main contribution of this paper, namely, a polynomial-time algorithm that computes logical filtering exactly for a significant class of transition systems. For some special cases we present simpler algorithms that are even more efficient. For systems that do not fall within this class our algorithm gives an approximation to the filter­ ing. Also, we show that we can keep the representation of the filtered belief state compact indefinitely for a class of dy­ namic systems. This class includes nondeterministic STRIPS systems and some systems whose actions are permuting.

The theorems that we consider most important are the fol­ lowing three. Let l<iJI be the number ofliterals in <p's represen­ tation, let #rules( a) be the number of effect rules defining a, and let Ga = G be the precondition of a as defined in (1). Assume that the effect rules that define a given action have identical sets of affected propositional symbols (how­ ever, different actions may have different such sets).

Theorem 4.1 (Efficiency). Given NNF formula <p, action a, and observation o, the filtering algorithm in Figure 1 returns the filtering of <p with a and o, if a is permuting. If a is not permuting, then the algorithm returns an logi­ cally weaker formula than the filtering. It does so in time O(l<fJI. 2#rules(a)+IL(Ga)l) .

Theorem 4.2 (Compact Filtering). Given k-CNF formula <p {fixed k), deterministic action a, and observation o in k-CNF. the filtering of <p with a and o is in k-CNF. if a is permut­ ing, Filter[a] (TRUE) is in k-CNF. and for every literal £ in <p, Filter[a](£) = Filter[a](TRUE) 1\ T, where Tis a conjunction of literals.

If a is not permuting, then the algorithm in Figure 1 still returns a formula in k-CNF.

The conditions on action a in the last theorem hold, e.g., for actions whose every defining rule has a precondition that is a single clause (e.g., a literal). It also holds for actions which are defined by at most two rules, and actions that affect all the literals that appear in their preconditions.

Finally, for nondeterministic STRIPS actions (actions that have no conditional effects) we get efficiency and compact representation. Let k-PI-CNF denote the class of k-CNF for­ mulae that include all their prime implicates (i.e., <p in k-PI­ CNF iff <pin k-CNF and for every clause C, if <p f= C, then there is a clause C' in <p such that C' subsumes C) . Every formula can be represented in k-PI-CNF for some k.

Theorem 4.3 (STRIPS Actions). Given k-PI-CNF formula <p {fixed k), STRIPS action a with effect in k-PI-CNF. and observation o in 2-CNF, the filtering of cp with a and o is computed in time O(lcpl· k + 21L(Ga) l). The result is ink-PI­ CNF, if after observing o we know if a succeeded or failed.

4.1 Closed-Form Solution and Factored Filtering

Our zeroth-order filtering algorithm uses consequence finding tools which do not scale to large domains. The following always holds and suggests a different reasoning procedure.

We can compute Filter [a] ( cp) by testing queries of the form cp f= Gi, V .. . V Giu (instead of applying consequence finding). On the other hand, it requires an exponential num­ ber in m of such tests (recall, m is the number of rules, in­ cluding the completion rules). Since m > 2n (there are two completion rules for each of the n domain features), this is worse computationally than the method of enumerating all the states.

In what follows we use the intuition that we need only few rules if cp includes only a small subset of P, the fluent sym­ bols of our domain. In general, cp may include many fluent symbols because we may know many things about many dif­ ferent parts of our domain. Nevertheless, if we can decom­ pose cp into small parts that can be filtered separately, then each of the parts includes only a small subset ofP, and filter­ ing each of the parts separately becomes easy.

Assume that we order the rules of a such that r 1 , ... , r t ( t :::; l) satisfy L(Fi) n L( Gi) = 0 (ri ="a causes Fi if G/', i :::; t), and rt+1 , ... , r1 satisfy L(Fi) n L(Gi) =f. 0. Furthermore, let r m+1 be the additional rule "a causes G if G" (recall, m is the number of rules of a, including completion rules). We define 13 to be

13 is a term that is always implied by Filter[a](TRUE), i.e., the progression of zero knowledge with the action a. The first set of conjuncts of 13 is the result of applying a rule "a causes Fi if Gi'' whose preconditions are not affected by ex­ ecuting a. Even when we know nothing before performing a, we will know that either the effect occurred or the precon­ dition did not hold and still does not hold. The second set of conjuncts applies a similar intuition for the case of effect rules that may affect the truth value of their original preconditions.

Define C ( L) to be the set of completion rules of a for flu­ ents in L, i.e., C(L) = { i > l I the effect ofri E Cis in L }.

We can now state the fundamental theorem of this Section. It holds for all domains expressed using our action language.

Theorem 4.4 (Closed-Form Representation). If cp is a be­ lief state formula and { r 1 , ... , r1} is the set of effect rules for action a, each of the form "a causes Fi if Gi ",then

The intuition for equation (4) is that progressing cp with an action a can be computed by looking at all the possible com­ bination of preconditions of effect rules and completion rules for L(cp). If we can prove that G1 V G2 holds from cp, then we can conclude that F1 V F2 holds in the result of executing a. The conclusions that are not accounted for with this intu­ ition are the effects that we infer from the completion rules in C(L(G1 , ... , G1)) together with the effect rules for a. Those conclusions are summarized in 13, which is independent of cp.

Our NNF filtering algorithm is presented in Figure I. It is much faster than our zeroth-order algorithm, and it relies on Theorems 4.4, 3.2, and 3.4. In the following, if 'ljJ is a logically weaker formula than our filtering, we say that it is a safe approximation for filtering. We denote effects by Fi and preconditions by Gi. For an action a, set t =I Ui::;! L(Gi)l.

Corollary 4.5 (NNF Filtering). Let cp be a formula in NNF with h literals, and let a be an action with l effect rules. Then, NNF-Filter safely approximates Filter [a]( cp) in time O(h · 2 1 H). If a is permuting, then this computation is exact.

Extended Example

As an example, consider our room-cleaning robot from above, and the action a = fetch(broom, closet), with the slightly more elaborate effect rule "a causes has(broom) 1\ -,in( broom, closet) if in( broom, closet) 1\ -,locked( closet)". Assume that our robot has its belief state represented by -,locked( closet) 1\ ( in(broom, closet) V in( broom, shed)).

NNF-Filter filters each of the literals separately with a and combines the results. For a given literal, filtering is mostly done is step I ofNNF-ProgressStep. We describe how this is done for each of the literals in our robot's belief state.

NNF-ProgressStep(a,-,locked(closet)) tests in step I all possible entailments of the form -,locked( closet) F viE/ Gi, where I includes elements from the effect rule of a, the frame rule for G (rule rm+1), and the completion rule for -,[ocked(closet). For brevity, denote the effect of a by F1, and the precondition for that rule by G1 . There is only one effect rule defining a, so in this case G = -,Q1 .

In that step, one of our tests finds that

-,[ocked(closet) f= G1 V G

(because G1 V G = G1 V ·G1 = TRUE). This makes us include F1 V G in the filtering. In the same step, another test finds that ·locked(closet) f= ·locked(closet) (trivially true). This makes us include ·locked(closet) in the filter­ ing. The conjunction of the two is logically equivalent to ·in( broom, closet) 1\ ·locked( closet). This is the result of filtering ·locked( closet) with a.

Similarly, for in( broom, closet), one of our tests in step I ofNNF-ProgressStep finds that

(because G1 V (G 1\ in(broom,closet)) G1 V in( broom, closet), and the latter follows trivially from in( broom, closet)) . As before, we also find that in( broom, closet) f= G1 V G. We find that the filter­ ing of in( broom, closet) with a is (in( broom, closet) V has( broom)) 1\ ( ·in( broom, closet) V locked( closet)) . Notice that this belief state implies has(broom) V locked(closet).

For the filtering of the last literal, in( broom, shed), we find its filtering to be equivalent to in( broom, shed) 1\ ( · in( broom, closet) V locked( closet)) . (Notice, that we do not know that the broom is not in the closet because initially we did not know that the broom cannot be in more than one place; we made this choice to simplify this example.)

Now, we recurse back in the algorithm and com­ bine the filtered formulae. We find that the filter­ ing of in(broom, closet) V in( broom, shed) is equivalent to (in(broom,shed) V in(broom,closet) V has(broom)) 1\ ( ·in(broom, closet) V locked( closet)). Notice that this belief state implies in( broom, shed) V has(broom) V locked( closet) .

Finally, for the original belief state, ·locked(closet) 1\ (in(broom,closet) V in(broom,shed)), we conjoin the last result with the filtering of ·locked( closet) and get

4.2 DNF and CNF Belief States

If <p is in DNF (a disjunction of conjunctions), then we can limit the size of the resulting formula. We write D I\ a f= 'If; to say that action a has effect rules in D that logically imply 'If; in a state in which a is executed (e.g., ,(j may be a tautology).

Corollary 4.6 (Iterating DNF Filtering). Let <p be in DNF with h literals and s disjuncts, and a an action with l effect rules with { Fi};::;L in DNFwith d disjuncts total, and { Gi}i :S: I in CNF, each with c conjuncts. Then, Filter[a](<p) in DNF is computed exactly in time O(h·2l+t) with at most max(2s, 1) · ( d~2) · c 1 disjuncts. If D 1\ a f= ·G, then it has at most

Thus, when a is a deterministic action (every rule's effect is a conjunction of literals) with a single effect rule that is always guaranteed to succeed, then the number of disjuncts in the formula does not grow as the filtering progresses.

For CNF formulae we can find a more significant class of actions that allow us to maintain compact representation. We show that under some conditions every k-CNF formula is fil­ tered into a k-CNF formula (fixed k). This implies that the belief state representation is no larger than (2n)k, which is manageable for small fixed k's.

The main observation that we use is that a clause of k liter­ als may give rise to a larger clause after filtering, only if one ofthe following holds: (a) the filtering ofT RUE includes a clause of more than k literals; or (b) the filtering of a literal includes a clause of2 or more literals that is not subsumed by Filter[a] (TRUE). The first case can occur when we do not know whether the action succeeded or not, and which rules applied if it did. In that case, we know that after the action one of the effects holds or no precondition holds (this yields a formula which may include many disjunctions). The second case can occur when the precondition of a rule includes a con­ junction ofliterals. When we filter a single literal we may get a disjunction in the result (of the form the effect holds, or the rest of the precondition does not). When we filter a clause, this may cause the filtering to include a larger clause.

The following theorem describes sufficient conditions for filtering a k-CNF formula into k-CNF, thus keeping the rep­ resentation compact (k is fixed).

Theorem 4.7 (Filtering a k-CNF Clause). Let C be a k­ CNF clause, and action a have l effect rules, all deterministic. Assume that B is in k-CNF, and that whenever f F v iE / Gi for literal f and I C { 1, ... , l, m + 1}, I I I ~ 2, then D 1\ a f= v iE/ Gi or f F G;Jor some i E I . Then, F i lter[a]( C) is in k-CNF and can be computed in time 0(2 1 +t ).

Note that B is in k-CNF for an action a when I ui<l L(Gi) UE.ff(a)l:::; k or I u i<l L(Gi ) \ Effia)l + l :::; k or l ~ 1 and IL(Gl)l- min(1, IL(Fl) \ L(GI)i) :::; k.

Consequently, filtering with actions that are permuting maintains a k-CNF ifF viE/ G; whenever f F viE/ Gi for some II I ~ 2. An example of such an action is .flipping a switch (if the light is on, it will get turned off, and vice versa). One of the preconditions always holds. Another example is moving a block (whichever it is) from the top of a stack. For literal f, iff f= top(A) V top(B) , then the disjunction is implied by D 1\ a or a single precondition follows from f.

Corollary 4.8 (Iterating CNF Filtering). If <p is in k-CNF. then the assumptions of Theorem 4. 7 imply that Filter [a] ( <p) is approximated safely in time O(I'PI · 2 1 H), with a result in k-CNF If a is permuting, then this computation is exact.

4.3 Prime-Implicate Belief States

It turns out that a form of distribution over conjunction holds for all actions if the belief state is represented as the conjunc­ tion of all of its prime implicates (formulae we call prime im­ plicate belief states (PI-CNF)). In this form we can distribute the computation to the conjuncts and conjoin the result of fil­ tering small subgroups of them separately. More precisely,

for z a number that depends on the representation of the pre­ conditions of a and on the number of rules defining a.

Theorem 4.9 (Filtering Prime Implicates). Let <p be in k­ PI-CNF (PI-CNF and k-CNF), and let action a have l effect rules with effects in k-CNF and preconditions in d-CNF, with each G; of at most c clauses. Then, equation ( 5) holds for z = c 1 · (de + 1), and PI-Filter (Figure 2) computes Filter[a](cp) exactlyintime0(2 1 ·1Pre(a)uEJJ(a)l.(sz+z)).IfDI\a I=-,(;, then z = c 1 , with 0(2 1 · (sz + z)) time.

Corollary 4.10 (Maintaining k-PI-CNF). Let cp be a k-Pl­ CNF formula, and let action a have l effect rules, all deter­ ministic. Assume that a; is a disjunction of literals, for all i ::; l. Also, assume that D 1\ a I= -,(;. Then, Filter[a] ( cp) = Pl-ProgressStep(a,cp), and the latter is in k-CNF. If k = 2, then Pl-Filter(a,cp) is in k-PI-CNF.

The conclusion for k = 2 uses the fact that every prime implicate of a formula in 2-CNF is a clause with at most two literals. Simple counter examples (omitted) show that k-PI­ CNF cannot be maintained without these conditions.

4.4 Nondeterministic STRIPS Domains

STRIPS domains present a special case of the results that we discussed above. In such domains every action has a single rule (no conditional effects) and actions can be executed only when their preconditions hold 1 . Unlike the original STRIPS, we allow nondeterministic effects, and allow belief states to be any CNF formulae in the ftuents of the domain.

More precisely, every action a has exactly two effect rules, r 1, r 2 . Their preconditions are such that a1 = .a2 . Also, F2 = FALSE. Thus, a can be executed only when a, holds. Consequently, when we filter with a we assert im­ plicitly that its preconditions held in the last world state.

The assumption that there is only one rule that determines a's effects and otherwise the action is not executed has a dramatic effect. For l1, ... ,lk literals we get that

1 With the alternate assumption that actions have no effect un­ less their preconditions hold, but observations (or their absence) are guaranteed to distinguish actions' success from failure, the same re­ sults hold, except that now the compactness of representation re­ mains only after filtering with observations.

Theorem 4.11 (Iterating STRIPS Filtering: CNF). Let cp be in k-CNF with s clauses and a a STRIPS action. If F1 is in k-CNF and IL(ai) \ L(F,)I ::; t, for some t ::; k, then Filter[ a]( cp) can be approximated safely in time 0( s · k + 2t), yielding a k-CNF formula. If a is permuting, then this computation is exact.

If our representation is PI-CNF, then we get an even stronger result, leading to the algorithm in Figure 3.

Theorem 4.12 (Factoring STRIPS filtering: PI-CNF). Let

1\;~8 C; be in Pl-CNF, and let a be a STRIPS action. Then,

For example, for a = fetch( broom, closet) that has ef­ fect F1 = has( broom) 1\ ·in( broom, closet), if we know (in( broom, closet)V·locked( closet) )A( in( broom, shed)V locked(closet)) before applying a, then after it we know F1 1\ (in(broom, shed) V locked( closet)).

Corollary 4.13 (Iterating STRIPS filtering: k-PI-CNF). Let cp be in k-PI-CNF, and let a be a STRIPS action with F, in k-PI-CNF, t = IL(a1 ) \ L(FI)I. and t ::; k. Then, STRIPS-Filter(a,cp) computes F i lter[a](cp) exactly in time O(lcpl · k + 2t), yielding a k-Pl-CNF formula.

This means that we can filter in practice any prime im­ plicate belief state in any nondeterministic STRIPS domain. This filtering stays compact, with the size depending only on the PI-CNF representation of F1 and the number of proposi­ tional symbols in a, but not F1 .

Finally, every STRIPS action can be filtered efficiently, even if we drop the assumption that either the action succeeds or we observe an error. This can be done by assuming that the action succeeds, finding the filtering of that action, and then disjoining the result with the initial belief state. Nonetheless, this scheme may cause representation space explosion as fil­ tering proceeds over multiple steps, unless some care is taken.

We tested our STRIPS-filter algorithm in partially observ­ able blocks-world domains. The implementation in LISP in­ cludes a random action-sequence and observation-sequence generator, and both the generator and filtering algorithm re­ ceive a description of the domain, actions and observations specified in PDDL (a plan-problem specification language).

We ran the algorithm with blocks-world domains of in­ creasing sizes (3 to 20 blocks), yielding domains that range from tens to over a thousand of propositional features. We collected the time taken per filtering step for each of the exe­ cutions and the space taken overall at every iteration, starting with zero knowledge. The results are shown in Figure 4.

4.5 Observation Model

An observation model is a theory 0 that includes observation constraints, axioms that describe the relationship between ob­ served facts and other fluents. We allow 0 to include any ax­ ioms. Our model assumes that observations o are collected after an action is executed. o is a sentence made up with flu­ ents, similar to the observation constraints. The conjunction, 01\ o is then used to filter the resulting belief state. Formally,

This allows all the results that we enumerated above to apply with this model as well. The following connects the results of Sections 3,4 to filtering with observations.

Corollary 4.14. If o 1\ 0 is in k-CNF and Filter[a] ( cp) is in k-CNF, then Filter[a,o](cp) is in k-CNF.

In particular, this means that our results for STRIPS do­ mains and for NNF, CNF and DNF formulae still hold here. Thus, the representation remains compact in the cases that we indicated already, and computation remains easy in the same cases as well. Finally, for k-PI-CNF, we get the following.

Corollary 4.15 (Obs. and k-PI-CNF). If o 1\ 0 is in 2-CNF, and cp is in k-PI-CNF, then Filter[o](cp) is in k-PI-CNF.

5 Conclusions

In this paper we presented the task of logical filtering and gave it a computational treatment. The results we obtained here have implications for monitoring and controlling dy­ namic systems. In many cases we present a closed-form com­ putation of the filtering and in others show how to approxi­ mate this computation. In some cases we can guarantee that the size of the representation of the filtered formula can be bounded and kept small. In those cases, logical filtering can be used to control processes that run over very long periods of time. Examples of such systems are abundant and include robot motion control, natural language processing, and agents that explore partially observed worlds.

We made use of several assumptions in this paper in differ­ ent contexts and with different consequences. We presented permutation domains and the certainty of existence of an ef­ fect ( D 1\ a I= -.G) as characteristics of the domain that make filtering easier. We showed that the commonly used assump­ tion that every action has a relatively small number of rules (at most polynomial inn), and that effects, preconditions and terms in the belief state typically use a small vocabulary, all have a drastic effect on the computational effort needed for filtering and on the size of the resulting belief state.

The need to track the state of the world is a basic one, and many works have appealed to it implicitly in the past. How­ ever, the computational treatment of such tracking has been avoided so far, partially due to the absence of a developed theory of nondeterministic domains, and partially due to neg­ ative results about the general cases of this task. Nonethe­ less, this problem and methods for its solution have received much attention in control theory. The results we obtained here promise to find their application in this domain and may be combined with stochastic filtering techniques.

Acknowledgments

This research was supported by ONR MURI Fund N000140l-l-0890, ONR MURI Fund N00014-00-l-0637, and NSF grant ECS-9873474. The first author thanks Xuanlong Nguyen for a stimulating discussion on Theorem 3.4.