State estimation is the task of estimating the state of a partially observable dynamical system given a sequence of executed actions and observations. In logical settings, state estimation can be realized via logical filtering. Unfortunately such filtering, though exact, can be intractable. To this end, we propose logical smoothing, a form of backwards reasoning that works in concert with logical filtering to refine past beliefs in light of new observations. We characterize the notion of logical smoothing together with an algorithm for backwards-forwards state estimation. We prove properties of our algorithms, and experimentally demonstrate their behaviour. Smoothing together with backwards-forwards reasoning are important techniques for reasoning about partially observable dynamical systems, introducing the logical analogue of effective techniques from control theory and dynamic programming.
Many applications of artificial intelligence from automated planning and diagnosis to activity recognition require reasoning about dynamical systems that are only partially observable. A necessary component of such systems is state estimation – the task of estimating the state of the systems given a sequence of executed actions and observations. State estimation is well-studied in control systems where transition systems are stochastic and the belief state is typically represented as a probability distribution. State estimation is commonly realized via filtering, of which Kalman filtering [Kalman, 1960] is a well-known example.
In logical settings, an analogous form of logical filtering
was proposed by Amir and Russell [2003] in which an agent’s
belief state – the set of possible world states – can be
compactly represented as a formula, and filtering is a form of
belief update. While logical filtering is intractable in the general
case [Eiter and Gottlob, 1992], there are tractable subclasses
often involving restricted transition systems or compact
encodings of the belief state
Our concern is with logical state estimation in service of tasks such as planning, execution monitoring, diagnosis, and activity recognition. We are particularly concerned with systems that include a rich characterization of how the actions of an agent indirectly affect their environment. These are typically captured by causal or ramification constraints (e.g., a causal constraint might say that if the battery and radio are ok and the radio is on then sound is emitted.). We assume that such constraints are compiled into the transition system as additional effects of actions following, e.g., [Pinto, 1999; Strass and Thielscher, 2013; Baier et al., 2014]. In planning such constraints tend to create problems with large conformant width [Palacios and Geffner, 2009].
We exploit the observation that for planning, only a subset
of the state is necessary to track. Planning systems need to
know (1) when actions are applicable, and (2) when the goal
is reached [Bonet and Geffner, 2014]. Execution monitoring
systems need only track the conditions under which a plan
remains valid
These observations motivate the development of state
estimation techniques tailored to the task of tracking the truth
of (conjunctions of) fluent literals. In Section 2 we
formalize state estimation as semantic logical filtering and propose
a sound under-approximation that is computationally
appealing. Motivated by the technique of smoothing for stochastic
systems
State estimation is a core task in reasoning about dynamical systems with partial observability. Consider the simplified action-observation sequence in support of diagnosing a car. You turn the key in the ignition, turn ignition, resulting in ignition turned. If ignition turned, battery ok and gas ok hold, then so will car started. You observe that the car did not start (car started = F alse), and so, under the assumption that the characterization of the vehicle functioning is complete, you can you infer :battery ok _ :gas ok. You turn on the radio, turn on radio, causing radio on as well as sound if battery ok ^ radio ok. You observe sound (sound = T rue). Under completeness and frame assumptions, you are now able to infer radio ok, battery ok and :gas ok. So following the action-observation sequence (turn ignition,:car started,turn on radio,sound), your estimated belief state comprises just one state here represented by the set of fluents fignition turned, radio on, :car started, battery ok, radio ok, :gas ok, soundg.
Informally, the state estimation task we address is: Given a dynamical system, a belief state, and a sequence of executed actions and observations, infer the resulting belief state of the system. For logical theories, state estimation is captured by logical filtering [Amir and Russell, 2003].
To relate our work to planning, execution monitoring
and diagnosis, we appeal to standard finite domain
planning language syntax. A dynamical system is a tuple =
hF ; S; A; R; Ii, where F is a finite set of propositional fluent
symbols such that if p 2 F , then p and :p are fluent literals,
S = P ow(F ) is the set of possible world states, A is a set of
actions including sensing actions, R S A S is the
transition relation (equivalently we use the notation (s; a; s0) 2 R
or s0 = R(s; a)), and I is a set of clauses over F that defines
a set of possible initial states, collectively – the initial
belief state. As noted in the introduction, we assume that causal
constraints are compiled into our transition system as extra
effects of actions
Throughout this paper we take the viewpoint that the state of represents the belief state of the agent. The semantics of logical filtering is defined by considering the belief state to be a set of possible world states S. For our purposes , we will often represent the belief state (henceforth also the state of the system) as a state formula . Later we will be restricting to a conjunction of fluent literals, sometimes denoted as a set of fluent literals and referred to as a conjunctive state formula. Following Amir and Russell (2003):
Given belief state S of dynamical system , the filtering of a sequence of actions and observations ha1; o1; : : : ; at; oti with respect to is defined as: 1. Filter[hi]( ) = 2. Filter[a]( ) = fs0 j s0 = R(s; a); s 2 g 3. Filter[o]( ) = fs j s 2
and o is true in sg 4. Filter[hai; oi; : : : ; at; oti]( ) =
Filter[hai+1; oi+1; : : : ; at; oti](Filter[oi](Filter[ai]( ))) We call step 2 progression with a and step 3 filtering with o.
When action a is filtered, every state s 2 is updated with
respect to the transition system R(s; a). When an
observation o is filtered, every state inconsistent with the observation
is eliminated. Logical filtering results in an interleaving of
action progression and observation filtering
While logical filtering realizes state estimation, the
resulting belief state representation can cause fundamental
inference operations to be intractable, such as inferring beliefs
about individual fluents [Shahaf and Amir, 2007]. A core
component of automated planning is determining the
applicability of actions during the search for a plan, as well as
determining whether the goal condition has been achieved.
Similarly dynamical diagnosis requires determination of the
refutation or confirmation of candidate diagnoses as the result
of (treatment) actions and sensing
Given belief-state formula of dynamical system , the approximate filtering of a sequence of actions and observations ha1; o1; : : : ; at; oti with respect to is defined as: 1. Filtera[hi]( ) = ; 2. Filtera[a]( ) = VfL j (C ! L) 2 ef f (a) ^
VfL j j= L ^ 8(C ! :L) 2 ef f (a); j= Cg j= :Cg; 3. Filtera[o]( ) =
^ o; 4. Filtera[hai; oi; : : : ; at; oti]( ) =
Filtera[hai+1; oi+1; : : : ; at; oti](Filtera[oi](Filtera[ai]( ))) Approximate logical filtering describes the belief state only in terms of a subset of the fluent literals entailed by the belief state. One can see from line 2 that progressing a state through an action a produces a state consisting of what was known to be caused (directly or indirectly) by a and what was known to persist through a.
Returning to our car example, we can see how this is a weak approximation. After the observations car started = F alse and sound = T rue, no further inferences could be made, yielding the belief state fignition turned, radio on, :car started, soundg
namical system, , belief-state formula representing possible belief state S, and action-observation sequence ha1; o1; : : : ; at; oti, Filter[ha1; o1; : : : ; at; oti]( ) j= Filtera[ha1; o1; : : : ; at; oti]( ).
This follows from Definitions 1 and 2. Approximate Logical Filtering is not complete with respect to the logical filtering semantics.
Given dynamical system, , conjunctive state formula , and action-observation sequence ha1; o1; : : : ; at; oti, where each oi is a conjunctive formula, Filtera[ha1; o1; : : : ; at; oti]( ) is a conjunctive formula.
The above proposition follows naturally from lines 2 and 3 of Definition 2 and is key to our complexity results and tractable approximate representations.
Theorem 2 (Complexity) Given dynamical system, , conjunctive state formula , and action-observation sequence ha1; o1; : : : ; at; oti, where each oi is a conjunctive formula, Filtera[ha1; o1; : : : ; at; oti]( ) is computable in time O(t c jF j) where c is the maximum number of conditional effects over actions in the sequence.
This follows from fluent entailment of a conjunctive formula and the limit of jF j fluents per consistent conditional effect. For automated planning and similar problems where the general assumption is that observations are conjunctive formulae, approximate logical filtering enables state estimation to reduce to set operations. While computationally appealing, the approximation is weak and thus of limited use on its own for AI planning, dynamical diagnosis, and similar tasks. In the next section, we show how to combine approximate logical filtering with a new approach for reasoning over the past – logical smoothing. 3
Filtering with a stochastic transition system involves
estimating the marginal posterior probability distribution of the
system conditioned on some data that was received prior
to the current system state. There is an analogous concept
for estimating not the current state but instead a previous
state. This is called smoothing – refining a previous state
estimation
We begin our treatment of logical smoothing by defining the semantics of logical smoothing with respect to a belief state. Given a representation of the sequence of actions, observations, and intermediate state estimates, logical smoothing recursively refines previous state estimates through a backwards update procedure. To this end, we store previous state estimates, coupled with the actions executed to construct successor states in a so-called history. Note that while we use a set of possible worlds to represent a belief state, histories can be defined with any sort of state representation (logical formulae, sets of fluents understood as a logical conjunction, etc.), which we exploit later in this section.
tem, , a belief state history over is a sequence of tuples ( 0; a0);( 1; a1);: : : ( n; an) such that each i is a belief state, a set of possible world states i S and each ai is an action of .
The intent of a history is to capture the evolution of the system starting from some designated initial belief state 0. The observations are not modeled as separate entities. Rather, they reside in the intermediate belief states, presumably as part of an original filtering process.
Given belief state S of dynamical system , the smoothing of a belief state history ( 0; a0);( 1; a1);: : : ( n; an) with respect to the is defined as: 1. Smooth[hi]( ) = 2. Smooth[o]( ) = Filter[o]( )
= fs j s 2 and o is true in sg 3. Smooth[( 0; a0)]( ) =
0 \ fs j s 2 PreImage(s0; a0); s0 2 g 4. Smooth[h( 0; a0); ( 1; a1); : : : ( n; an)i]( ) =
Smooth[h( 0; a0); : : : ( n 1; an 1)i]
(Smooth[( n; an)]( )) where PreImage(s0; a) = fs j s0 = R(s; a)g
Logical smoothing works by propagating acquired information (typically an observation or the resultant filtered stateaction pair) back through a given history and updating its constituent state estimates. Note that this is more akin to belief updating than to belief revision. Each smoothing step refines previous state estimates in that the smoothed state’s set of possible world states are always a (non-strict) subset of the state’s original set of possible world states.
With the semantic account of logical smoothing in hand, we now define the notion of logical smoothing with respect to a more compact representation of the set of belief state in terms of a belief state formula.
Definition 5 (History) Given dynamical system, , a history H over is a sequence of tuples ( 0; a0); ( 1; a1); : : : ( n; an) such that each i is a belief-state formula over F and each ai is an action of .
Definition 6 provides a formal characterization of logical smoothing with respect to a belief-state formula representation of the history. It utilizes regression rewriting [Reiter, 2001] to propagate updates back through the history. Regression, denoted as R[ ; a], takes a logical formula and action a and rewrites the formula in terms of the weakest conditions necessary for to hold following the execution of a. We appeal to Reiter’s definition of regression in the situation calculus [Reiter, 2001] with syntactic notation suitably modified.
When the history comprises a single state-action pair, formula is simply conjoined to the state. Otherwise, the formula is regressed step by step through the history, and any new information garnered from the regression, NEW , is conjoined to the associated state. P I( ) refers to the prime implicates of formula .
, history H = ( 0; a0); : : : ( n; an) and formula , the logical smoothing of H with respect to is defined as: 1. Smooth[( ; a)]( ) = ( ^ ; a) 2. Smooth[( 0; a0); : : : ; ( n; an)]( ) =
Smooth[( 0; a0); : : : ; ( n 1; an 1)]( NEW), Smooth[( n; an)]( ) where NEW = Vf' 2 P I(R[ ; an 1]) j n 1 2 'g
The soundness and completeness of Logical Smoothing (Definition 6) relative to the semantic account in Definition 4 follow straightforwardly from the correspondence between PreImage and regression.
Returning to our car example, consider logical smoothing with respect to the observation car started = F alse. For ease of presentation, assume approximate logical filtering is used for action progression. Progressing the initial state, 0, through the action turn ignition results in state 1, which is equivalent to 0 since the effect of turn ignition is predicated on fluents whose truth value is unknown. When the observation action obs(car started) is subsequently performed and car started = F alse observed, the smoothed history is given by Smooth[h0; h1](:car started) where h0 = ( 0; turn ignition) h1 = ( 1; obs(car started)). Following point 2 of Definition 6, this is equivalent to Smooth[(h0)]( NEW); Smooth[(h1))](:car started). Rule 1 of the logical smoothing semantics smooths 1 of h1 as 1 ^ :car started. The action obs(car started) has no effects and therefore the observation car started = F alse must hold in the prior state. Returning to NEW , this formula hinges on R[:car started; turn ignition]. By the regression re-writing and frame axioms, this gives = :car started ^ (:battery ok _ :gas ok). As 0 j= :car started, we are left with NEW = :battery ok _ :gas okay after restricting to prime implicates, giving the intuitive refinement of the initial state given the observation. Algorithm 1: LSmooth(H; ; i) Perform logical smoothing on history H given that holds at i in H. Returns updated H and the index of termination. 1 i = i ^ 2 if i > 0 then 3 = R[ ; ai 1] 4 NEW = Vf' 2 P I( ) j i 1 2 'g 5 if NEW is empty then 6 return 7
LSmooth(H; NEW ; i 1)
Algorithm 1 realizes Logical Smoothing together with an optimization to support early termination of the regression. Included in its input is a state index parameter, identifying the location within history H where is to be integrated. Logical smoothing can thus acquire information about a past state and smooth the preceding state estimates in light of it, as well as smoothing from the most recent state. The heart of the smoothing procedure lies within R[ ; ai 1] (line 3) as explained above. Line 4 identifies those aspects of that are new to state i 1 by identifying prime implicates of not entailed by i 1. This is an optimization as it allows for early termination (line 5) when further smoothing would be unnecessary and it minimizes the subsequent formula to be regressed in the next iteration. The process then repeats on the newly computed NEW formula at index i 1. Finally, LSmooth returns a tuple of the refined history and the index of termination term-idx . The purpose of returning term-idx will become apparent in Section 4 when we leverage logical smoothing in a state estimation algorithm.
dynamical system and a history H over with at least n state-action tuples and a formula over F , the updated history returned by LSmooth(H; ; n) is the updated history returned by LSmooth(H; ; n) with the early termination condition of line 5 removed.
It follows straightforwardly from the close correspondence between Definition 6 and Algorithm 1, and Proposition 2 that the history computed in Algorithm 1 is equivalent to the specification in Definition 6.
We say that H0 = ( 00; a00); : : : ; n0; a0n) is a sound and complete refinement of H = ( 0; a0); : : : ; ( n; an) with respect to formula that holds at index i of H if for all 0 j n, (1) a0j = aj ; (2) j0 j= j ; and (2) if j < i, Filter[haj0; j0+1; :::; ai0; i0i]( j0) j= . In other words, a sound and complete refinement captures all of what must be known based on the existing history and necessary conditions for . With this definition in hand we have,
namical system , history H over , and formula over F that must be true at i of H, LSmooth(H; ; i) produces a sound and complete refinement of H.
Logical smoothing provides a sound, complete, and principled approach to smoothing previous state estimations in a logical system in light of additional observations or information which must hold in the associated state. As this is merely the general algorithmic structure of logical smoothing, further optimizations are possible but omitted for clarity of exposition of the core concepts.
Unfortunately, like logical filtering, the querying of belief states resulting from logical smoothing may not be tractable. To make matters worse, while a single regression step results in a linear increase in formula size with respect to the input, recursive applications of regression result in an exponential blow up [Fritz, 2009]. To remedy these issues, we define, as we did with logical filtering, an analogous procedure of approximate logical smoothing. We do so by one minor adjustment to the logical smoothing outlined in Algorithm 1: Line 4: NEW = ^ff j ^ i 1 j= f and i 1 2 f g (1) Where f is restricted to fluent literals. This approximation limits the updating of the history to fluent literals entailed by these regressed additions. Again we consider only the entailments not already captured by a state in the history. We denote the resulting algorithm obtained by modifying LSmooth as per (1) as LSmootha. It should be stressed that this is but one way to deal with the formula size increase due to repeated applications of regression. Alternatives which do not sacrifice completeness include adding new fluents in place of certain sub-formulae of the regressed formula [van Ditmarsch et al., 2007] or representing the formula as a circuit [Rintanen, 2008].
Following Definition 6, logical smoothing produced the correct refinement of the initial state with :battery ok _ :gas ok. However, with approximate logical smoothing
NEW is limited to fluent literals, resulting in an empty formula and therefore no refinement. Some information is lost but other inferences can still be made. Continuing with the sequence of actions in our example, after obs(car started) the actions turn on radio and obs(sound) are executed, obtaining sound = T rue. By smoothing with respect to this observation the regression R[sound; turn on radio] gives = sound_(battery ok^radio ok). Following the approximation rule (1) we get NEW = battery ok ^ radio ok due to the previous state in the history entailing :sound. Even with the approximation, we refine the estimate of the prior state with the knowledge battery ok ^ radio ok. Continuing this example, approximate logical smoothing would smooth each state in the history, including the initial state, to include battery ok ^ radio ok.
H be a history over of n state-action tuples, and be a formula over the language of F that must be true at the state at index i of H. If LSmooth(H; ; i) = (H0; j) and LSmootha(H; ; i) = (H00; k) then for all 0 i n, if i0 is the i-th state of H0 and i00 is the i-th state of H00 then i0 j= i00.
By Proposition 3, LSmootha is an under-approximation of LSmooth. It amounts to a version that smooths only with respect to conjunctive formulae. Moreover, analogously to approximate logical filtering (Proposition 1), approximate logical smoothing is conjunctive state formula preserving.
We also sidestep the exponential size formula blowup from repeated regression operations by always regressing conjunctive formulae except for, potentially, in the first step. Theorem 4 (Complexity) Given a history H over a dynamical system of n state-action tuples such that all states are conjunctive formulae, a conjunctive formula over the language of F , and an index i of H, LSmootha(H; ; i) can be computed in time O(n 2jFj) with propositional entailment or O(n jF j2) with unit propagation entailment.
While the worst case complexity is exponential, in practice this is not the case. Actions typically trigger few indirect system effects (ramifications) in comparison to the size of the propositional domain. This results in a compact regressed formula where all unit entailments are computable through unit propagation in most cases. Note that since we place no restrictions on the syntactic form of regressed formulae, such as restricting to Horn clauses, unit propagation may not produce all entailments, resulting in a sound under-approximation.
Logical smoothing refines the previous state estimates by reasoning backwards (regressing) over the history of actions and states with respect to some acquired information. In many cases, this process removes some uncertainty about the past, particularly in dynamical systems where actions have causal ramifications. This information about the past can then be propagated forwards (progressed) through the state-action history to potentially produce further refinements.
As we last left the car example from Section 3.1, each state in the history, including the initial state, was smoothed with battery ok ^ radio ok after observing sound = T rue. While it is obvious that this should be propagated forward to the current state, as it stands it is not so obvious how and why, in general, this should be done. Consider the case where the action turn ignition actually had an additional effect battery charging if battery ok. Propagating battery ok forward from the initial state given the actions and intermediate states in the history further refines the postturn ignition state estimates (including the current state) with battery charging.
We can realize the forward phase outlined above via filtering. Note that when operating on a history, simulating the forwards reasoning phase by filtering works on the corresponding sequence of actions with observation formulae being the state formula. For notational convenience, we define subseq(H; i) of a history H = ( 0; a0); ( 1; a1); : : : ; ( n; an) and index 0 i n as the sub-sequence hai; i+1; ai+1; :::; n; ani. Algorithm 2 outlines our backwards-forwards state estimation algorithm. Algorithm 2: BF(H; ; i) Perform backwards-forwards state estimation on history H given that formula holds at i in H. 1 (H0; term-idx ) = LSmootha(H; ; i) 2 return Filtera[(subseq(H0; term-idx )]( term-idx )
The BF algorithm uses approximate logical smoothing and approximate logical filtering. BF maintains conjunctive state formulae while computing sound state estimates. Logical smoothing allows us to encode complex information about any state of the system into the history, keeping each individual state estimate in a compact and computationally manageable form that is maintained through a simple logical filtering procedure. Towards this goal of tractability, BF leverages approximate logical smoothing with unit propagation entailment. When combined, the result is an intuitive reasoning mechanism for dynamical states with partial observability.
Although it may appear excessive to filter with respect to state formulae, the states are always conjunctive formulae and approximate filtering operates by conjoining the observation formula with the state formula resulting from progressing the previous action. Since all refinements are sound, this reduces to simple set operations over the fluents.
namical system of n state-action tuples such that all states are conjunctive formulae, a conjunctive formula over the language of F , and an index i of H, BF(H; ; i) can be computed in time O(n c 2jFj) with propositional entailment or O(n c jF j2) with unit propagation entailment, where c is the maximum number of conditional effects over actions of .
This follows from the previous complexity results.
Here we outline two optimizations to alleviate the space requirements of logical smoothing.
State Relevance Minimization. The smoothing process only relies on a subset of the state. Given a history H with tuple ( ; a), it is sufficient for to only include the fluents f that are involved in the conditional effects of a. This is due to the regression formula being purely over these fluents plus fluents of which have no positive or negative effects with respect to a. Such an optimization of the state fluents would greatly reduce the memory overhead as actions typically involve and effect a small fraction of the domain. The downside is that the
NEW may contain old inferences and thus the early termination becomes less robust.
Sliding Window History. A second optimization is to smooth over a fixed window size called fixed-lag smoothing [Einicke, 2012] in stochastic systems. This greatly improves the memory footprint, at the potential expense of quality of the estimation.
We investigate three key questions: (1) how effective is our approach in capturing the necessary fluent literals to determine action preconditions and the goal; (2) how does our state relevance minimization impact the system; and (3) how does our approach perform in light of different manifestations of a domain’s dynamics. Ideally, we would compare our approach empirically with logical filtering. However, the original authors confirmed in private correspondence that the code is unavailable. Instead, we look to the field of automated planning that deals with partial observability and sensing. We use a set of standard benchmark problems and two newly created domains.
We ran the BF algorithm on valid plans, and here we present statistics on the proportion of action traces (plan branches) for which all action preconditions and goal condition are known to hold. For comparison, these are also reported for Approximate Logical Filtering (ALF). Average history state sizes over the action traces are reported for the BF algorithm and with the state relevance minimization (BF+SRM) as outlined in Section 4.1. Problem statistics and running times are also reported.
The plans were produced by the planner POPRP [Muise
et al., 2014], which leverages a compilation of partially
observable planning problems that exhibit particular
properties making them easier to solve
Table 1 shows the results of evaluating the BF algorithm on plans for each of the benchmarks. First, consider the Precondition / Goal Coverage section. Even with a judicious underapproximation, the BF algorithm is capable of tracking every relevant fluent for every action trace of all plans for the above problems. This is due in part to the fact that these problems belong to the class of width-1 simple contingent problems, which has the property that once a fluent becomes known it stays known [Bonet and Geffner, 2011]. For problems like the Colored Balls, ALF is capable of solving a significant portion of the action traces. This is to be expected; the domain has very little dynamics. In the case of four colors with one ball, the only unsolvable traces result from the situations when the ball must be in the last location not observed and the plan is able to infer this without directly observing it. Other domains, like Wumpus and CTP, require heavy reasoning, causing ALF to fail in most, if not all, cases.
Table 1 also reports the average history state size as a percentage of the total number of fluents in the problem. The large reduction in state size from SRM is due to the fact that only sensing actions have relevant information: no action affects observable fluents. This is a byproduct of the problem structures that the planning community has chosen to focus on and highlights the orthogonality of this work to what is currently being researched.
Lastly, Table 1 reports how much time it takes to solve every action trace of the plan for the associated problem. There are two main take-aways here. First, the SRM optimization creates a space vs time trade off. It significantly reduces the memory footprint of the history but has an impact on computation time. Second, as one would expect, the time to solve a given instance correlates with the number of branches (action traces) in the plan as well as their average length in terms of the number of actions. This is why large problems like Wumpus05 can be solved much quicker than a smaller problem like Balls4-2.
To further expand the evaluation, we introduce two new domains in the class of width-n non-simple contingent problems that specifically involve system dynamics and hidden state information that must be inferred.
Password. n switches may be flipped by the agent. Each has an unobservable correct position. There are n + 1 lights such that the i-th light signifies that exactly i switches are in the wrong position. The goal is for the 0-th light to be on and for the agent to know the correct position of each switch. Lights. n lights are connected in series and each may potentially be broken. A light may be off if it is broken or a light downstream is broken. The agent must fix lights that are known to be broken and reach a state where all lights are no longer broken. This domain has cascading effects as fixing a single light may change the “lit” status of all lights upstream.
Note that the contingent width
These problems represent two orthogonal classes of dynamic domains with their differences best summarized by Figure 1. First, consider the Password domain. As the problem size grows, the average number of conditional effects grows dramatically. Any time a switch is flipped, all possible cases for the n + 1 lights changing must be covered. With the Lights domain, the actions of fixing a single light have more repercussions as lights are added but the chain is max-BR
avg-BR
20 30 Problem Size (# of lights/switches) 40 10
20 30 Problem Size (# of lights/switches) 40 50 only increased by one per new light. If we look at how the average number of conditions (fluents) of the conditional effects grow with respect to problem size we see the reverse the Lights domain grows much faster than Password. By the parametrization of the Password domain, each conditional effect of flipping a switch depends only on the correctness of the switch and the light that is currently on. For the Lights domain, as more lights are added fixing any single light has a longer chain of potential ramifications given the status of the lights both upstream and downstream. Therefore, these problems allow us to compare how BF scales with respect to these two important domain characteristics.
We evaluate via a simulation that creates a randomized true state and produces a sequence of actions that should result in a state where the goal holds. Figure 2 shows how the BF algorithm performs as the problem size increase, averaged over 100 random action traces. As with the standard benchmarks, the BF algorithm correctly deduced all action preconditions and goal states over all generated action traces. The main point of comparison here is not pure performance but instead performance of problem type as per the preceding discussion of Figure 1. The Password domain scales slightly better partially due to the general domain growth with respect to problem size being lower than the Lights domain as per Figure 3. As Figures 1 and 3 show, an increase in a simple notion of problem size can have a large impact on multiple facets of the problem representation. Regardless of how the dynamics of the system manifest when compiled into conditional effects of actions, Figure 2 shows that the BF algorithm scales equivalently. 6
In this paper we propose an approach to logical state estimation for dynamical systems that is tailored to address the tracking of individual fluents in a computationally efficient manner. Similar to Amir and Russell’s original work on logical filtering, we elected not to perform our analysis in the situation calculus, but rather to use a dynamical system model that is employed by those who develop efficient algorithms for AI automated planning and diagnosis. Nevertheless, there is a large body of work in the knowledge representation literature, much of it in the situation calculus, that is related to logical filtering; particularly work on belief update and on progression. Among these, Lin and Reiter (1997) provided a broad study of progression spawning a number of other advances and culminating in Vassos and Levesque’s (2013) treatment of first-order progression, which appears to subsume Shirazi and Amir’s (2011) work on first-order logical filtering. Also relevant to approximate filtering, and in small degree smoothing, is the work by Liu and Levesque (2005) that studies progression in dynamical systems with respect to so-called Proper Knowledge Bases. This work shares some motivation with our conjunctive formulae restriction in attempting to avoid disjunction in favor of tractability. Further, 3000 2500
20 30 Problem Size (# of lights/switches) 40 the authors discuss a limited integration of sensing via regression to determine the context of actions to be performed, building on a similar idea for projection by De Giacomo and Levesque (1999). Finally, Ewin et al. (2014) study the problem of query projection for long-living agents by combining regression and progression in a manner that is similar in spirit to the work presented here.
Our work is inspired by work on smoothing and
backwards-forwards reasoning in stochastic systems,
building on previous work on logical filtering [Amir and Russell,
2003], the adaptation of the classical filtering to a logical
setting. Various works on (database) progression
One of the first works on the approximation of logical belief states in dynamical systems was the 0-approximation semantics proposed by Baral and Son (1997). Like our approximation techniques, they represent beliefs in terms of conjunctions of fluents, but do not exploit a notion of backwardsforwards reasoning to do state estimation.
The field of automated planning has spawned numerous
systems which necessarily have a sub-component to perform
state estimation. For example, the systems CN Fct, DN Fct,
and P Ict
The SDR Planner [Brafman and Shani, 2012] maintains a history of actions similar to our history of state-action pairs but for a slightly different purpose. The planner samples a possible complete initial state then assumes it is correct and plans appropriately. When information is gained through sensing actions that disprove the correctness of the initial state sample, re-planning is performed and a new state is sampled. To ensure action preconditions are correctly followed, precondition fluents are regressed through the history to the initial state to ensure satisfiability. This portion of the algorithm is similar, at a high level, to the fundamental ideas of logical smoothing - that an understanding of the evolution of the past can produce new information about the present. More recently Brafman and Shani (2014) also exploit regression for effective state estimation. A key difference, however, is that we use newly discovered information about past states to reduce the uncertainty of more recent states. In contrast, they only perform a backwards pass on the history of actions and observations, using full regression, while we approximate for efficiency.
Most recently Bonet and Geffner (2014) developed algorithms for belief tracking for so-called simple planning problems, as noted previously. We were unable to perform an experimental comparison with their work because their implementation is domain-specific. Nevertheless, it is interesting to consider when one approach works well and the other does not. As width-n problems, both the Password and Lights domains would cause an exponential blowup for their technique. Conversely, there are width-1 problems where our approximation does not capture simple entailments, such as conformant-like conditions where case-based reasoning plays a role. The complementary nature of the two approaches makes their combination an obvious step for future research.
Logical smoothing and backwards-forwards reasoning are important techniques in service of reasoning about partially observable dynamical systems. They characterize the logical analogue of commonly used techniques in control theory and other dynamic programming settings. This paper provides the formal foundations for a number of interesting theoretical and algorithmic tools that are of practical significance for automated planning, execution monitoring, diagnosis and beyond. We demonstrated the effectiveness of our approach, which has flawless recall on state estimation for the preconditions and goal conditions in the plans for existing partially observable planning problems. Further, we witnessed a dramatic reduction in the number of fluent literals that must be monitored. In future work we plan to integrate our algorithms with a contingent planning system.While our work was presented in the context of deterministic actions, the account and algorithms extend trivially to non-deterministic actions, and can be extended to exogenous actions. We plan to elaborate on such cases and to further explore variants of logical smoothing and our BF algorithm as they relate to non-deterministic and probabilistic transition systems. Finally we wish to further explore the theoretical relastionship between our work and progression over Proper KBs, and relationship to the various approximations defined by Palacios and Geffner in [Palacios and Geffner, 2009] and by Bonet and Geffner in [Bonet and Geffner, 2014].
Acknowledgements: The authors gratefully acknowledge funding from the Natural Sciences and Engineering Research Council of Canada (NSERC).