Generalized First Order Decision Diagrams for First Order Markov Decision Processes

1 Introduction

Recently, Boutilier et al. [2001] have shown how ideas about relational MDPs (RMDP) can be used to solve stochastic planning problems. Several authors have developed different representation schemes and algorithms implementing this idea [Kersting et al., 2004; H¨olldobler et al., 2006; Sanner and Boutilier, 2009; Wang et al., 2008]. In particular, [Wang et al., 2008; Joshi and Khardon, 2008] introduced the FODD representation, showed how RMDPs can be solved using FODDs and provided a prototype implementation that performs well on problems from the International Roni Khardon Tufts University Medford, MA, USA

∗Supported by the Fraunhofer ATTRACT fellowship STREAM.

roni@cs.tufts.edu

Planning Competition. The use of FODDs to date has two main limitations. The first is representation power, where FODDs (roughly speaking) represent existential statements but do not allow universal quantification. This excludes some basic planning tasks. For example, a company that has to plan a recall of faulty products requires quantifier prefix ∃∀ for the goal: there exists a depot such that all products are in the depot. The second is that manipulation algorithms for FODDs require special reductions to ensure their size is small. Such reductions have been introduced but they are not complete.

The paper makes three contributions. We introduce Generalized FODDs that allow for arbitrary quantification. We show how they can be used to solve RMDPs with arbitrary quantification. We provide a new approach to reduction based on model checking. This provides a complete reduction for FODDs and a sound reduction to some quantifier settings of GFODDs. This is a significant extension of the scope of the FODD approach to solving stochastic planning problems, and a significant improvement of our understanding of their reductions. Due to space constraints all proofs and some details are omitted from the paper; they are available in the long version of this paper.

Relational MDPs

A Markov decision process (MDP) is a mathematical model of the interaction between an agent and its environment [Puterman, 1994]. Formally a MDP is a 4-tuple <S,A, T,R> defining a set of states S, set of actions A, a transition function T defining the probability P(s′ | s, a) of getting to state s′ from state s on taking action a, and an immediate reward function R(s). The objective of solving a MDP is to generate a policy that maximizes the agent's expected total discounted reward. Intuitively, the expected utility or value of a state is equal to the reward obtained in the state plus the discounted value of the state reached by the best action.

This is captured by the Bellman equation as V (s) = Maxa[R(s) + γΣs′P(s′ |s, a)V (s′ )]. The value iteration algorithm is a dynamic programming algorithm that treats the Bellman equation as an update rule and iteratively updates the value of every state until convergence. Once the optimal value function is known, a policy can be generated by assigning to each state the action that maximizes expected value. Hoey et al. [1999] showed that if R(s), P(s′ | s, a) and V (s) can be represented using algebraic decision diagrams (ADDs) [Bahar et al., 1993], then value iteration can be performed entirely using the ADD representation thereby avoiding the need to enumerate the state space. This provides a solution for propositionally factored MDPs but does not handle relational structure. Later Boutilier et al. [2001] developed the Symbolic Dynamic Programming (SDP) algorithm in the context of situation calculus. This algorithm provided a framework for dynamic programming solutions of RMDPs that was later employed in several formalisms and systems [Kersting et al., 2004; H¨olldobler et al., 2006; Sanner and Boutilier, 2009; Wang et al., 2008; Joshi and Khardon, 2008]. As in the propositional case, each portion of the Bellman equation is captured abstractly so that computation is shared by identical portions. Further details about the algorithm are given in Section 5. Importantly, in this scheme, we need an efficiently manipulable representation assigning values to abstract states.

First Order Decision Diagrams

This section briefly reviews FODDs [Wang et al., 2008] using standard terminology from first order logic (e.g. [Lloyd, 1987]). A first order decision diagram is a labeled directed acyclic graph, where each non-leaf node has exactly 2 outgoing edges labeled true and false and is labeled by an atom generated from a predetermined signature of predicates, constants and an enumerable set of variables. Leaf nodes have non-negative numeric values. The signature also defines a total order on atoms, and the FODD is ordered with every parent smaller than the child according to that order. Three examples of FODDs are given in Figure 1; in these and all diagrams in the paper left going edges represent the true branches and right edges are the false branches. Thus, a FODD is similar to a formula in first order logic. Its meaning is similarly defined relative to interpretations of the symbols. An interpretation defines a domain of objects, identifies each constant with an object, and specifies a truth value of each predicate over these objects. In the context of RMDPs, an interpretation represents a state of the world with the objects and relations among them. The semantics of FODDs is defined as follows [Groote and Tveretina, 2003; Wang et al., 2008]. Given a FODD and an interpretation, a valuation assigns each variable in the FODD to an object in the interpretation. If B is a FODD and I is an interpretation, a valuation ζ fixes the truth value of every node atom in B under I. The FODD B can then be traversed in order to reach a leaf. The value of the leaf is denotedMapB(I, ζ). MapB(I) is then defined as maxζMapB(I, ζ), i.e. an aggregation of MapB(I, ζ) over all valuations ζ. For example, consider the FODD in Figure 1(b) and the interpretation I with objects a, b, c and where the only true atoms are p(a), q(b). The valuations {x/a}, {x/b}, and {x/c} will produce the values 1, 1 and 0, respectively. By the max aggregation semantics, MapB(I) = max{1, 1, 0} = 1. Thus, this FODD is equivalent to the formula ∃x, p(x)∨q(x). In general, max aggregation yields existential quantification when leaves are binary. When using numerical values we can similarly capture value functions for RMDPs.

Akin to ADDs, FODDs can be combined under arithmetic operations, and reduced in order to remove redundancies. Previous work has introduced several reduction operators. Intuitively, redundancies in FODDs arise in two different ways. The first observes that some edges may never be traversed by any valuation. Reduction operators for such redundancies are called strong reduction operators and they preserve MapB(I, ζ) for every valuation ζ (thereby preserving MapB(I)). On the other hand, weak reduction operators preserve MapB(I) but not necessarily MapB(I, ζ) for every ζ. Weak reductions allow us to prune the diagrams further. All weak reductions previously introduced rely on notions of implication of reachability between different paths in the diagram, combined with a notion of value domination between the same parts [Wang et al., 2008; Joshi and Khardon, 2008].

Weak reductions offer some subtle difficulties discussed in previous work. One of the issues is illustrated by the example in Figure 1(c). This simple FODD contains only 2 paths leading to non-zero leaves. Notice that whenever there is a valuation traversing one of the paths, there is another valuation traversing the other and reaching the same leaf. Thus either path can be safely removed from the diagram, but at least one must be kept. This suggests that we impose an ordering among paths that will indicate which one is to be preferred in such cases.

Definition 1 A descending path ordering (DPO) is an ordered list of all paths from the root to a leaf in a FODD, sorted in descending order by the value of the leaf reached by the path. The relative order of paths reaching the same value can be set arbitrarily.

2 Model Checking Reduction for FODDs

In this section we introduce a new reduction operator R12 (numbered to agree with previous work). The basic intuition behind R12 is to use the semantics directly. The map of a diagram is generated by aggregation of values obtained by running all possible valuations through the FODD. Therefore, if we document the behavior of every possible valuation under every possible interpretation, that is, which path it traverses under which interpretation, we can identify parts of the diagram that are never instrumental in determining the map. Such parts can then be eliminated to reduce the diagram. Crucially, with some bookkeeping, it is possible to obtain this information without enumerating all possible interpretations. For a given valuation ζ, any interpretation can be classified into one of a set of equivalence classes based on the path p that it forces ζ through. All such interpretations are consistent with PF(p)(ζ), where PF(p) denotes the path formula of path p which is the conjunction of literals on the path. Therefore the most general interpretation that forces ζ

through p can be viewed as a key or identifier for its equivalence class. If we collect the abstract interpretation PF(p)(ζ) for every path p that a valuation ζ could possibly take (i.e. every path where PF(p)(ζ) is consistent), along with the corresponding path and leaf reached, we will have all information we need to describe the behavior of ζ under all possible interpretations. The procedure getValue does exactly that by simulating the run of a valuation through a FODD. The input to getValue is the FODD B to be reduced and a valuation ζ. The output of the procedure is a set of <leaf, p, I> triplets, where leaf is the leaf reached by ζ by traversing path p and I = PF(p)(ζ). The output must contain one triplet corresponding to every path in B such that PF(p)(ζ) is consistent. This can be done by traversing the diagram and, when we reach a node whose truth value has not yet been defined, recursively collecting the paths and values for both possible truth values.

Figure 2 shows an example of the R12 reduction. The reduction is applied to the FODD on the left to reduce it to the FODD on the right. The table illustrates the result of running the getValue procedure on all possible valuations over the set of domain objects {a, b} and the variables x and y appearing in the left FODD. For example, the traversal of valuation {x/a, y/b} through the FODD has 3 possible eventualities. Either it reaches a 10 leaf by traversing path {1t} (which is short for path consisting of the true edge of node 1), under abstract interpretation {p(a)}, or it reaches a 10 leaf by traversing path {1f2t} under abstract interpretation {¬p(a), p(b)} or otherwise it reaches the 0 leaf via path {1f2f}.

The next step is to generate all possible ways in which an aggregate value can be derived. Once again we avoid enumerating all interpretations. The table gives sufficient information to list all possible ways to aggregate over the set of all valuations. Just consider all combinations of behaviors over the set of valuations. Every combination (as long as it is consistent) can produce an aggregate value or the map. The aggregation, however, has to be done so as to expose the valuations (and paths) that prove to be instrumental in determining the map. Intuitively, paths that remain unexposed in spite of listing all possible ways to aggregate over the set of all valuations are not instrumental and can be removed. To this end, we introduce variants of the max aggregation function.

Generalized Aggregation Functions: max2 and max3 max2 is defined relative to a fixed DPO, PL. The input is a set of 3-tuples of the form <vi, pathi, Ii> each corresponding to a valuation ζi so that ζi traverses path pi in the FODD under interpretation Ii to reach leaf vi. The output is a 3tuple <vo, patho, Io> where vo = maxi[vi], Io = ⋃i=1 Ii, and patho is the path of least index, under the order imposed by PL, with leaf value vo.

The example in Figure 2 shows the DPO and aggregation results derived from the table. Each of the 3 resultant tuples is derived by collecting one tuple from every row and applying max2 to the collection. E.g., aggregating over <10, {1t}, {p(a)}>, <10, {1t}, {p(a)}>, <10, {1t}, {p(b)}>, and <10, {1t}, {p(b)}>, using max2 gives <10, {1t}, {p(a), p(b)}> indicating that there is a possible aggregation where the path consisting of the edge {1t} is instrumental in determining the map.

max3 just runs max2 on every possible combination of triplets over the list of valuations and returns the results of those where Io is consistent and vo > 0. The example in Figure 2 shows the result of applying max3 to the elements in the table. Only 3 of the 2 × 3 × 3 × 2 = 36 possible combinations result in a consistent combined interpretation and positive value. Aggregations resulting in 0 value are ignored because 0 is uninteresting under the max aggregation.

To summarize, R12 is defined as follows: we fix a DPO PL, invent as many new objects as the number of variables in B and generate U, the set of all possible valuations of the variables in B over these objects. Then we run getValue on each valuation to generate a table as in Figure 2 and run max3 on it to generate S, the set of resultant triplets. At the end we partition the set of edges in B into 2 sets: E′ , the set of edges appearing in any path in any triplet in S, and E, the set of edges in B that are not in E′ . Intuitively, the edges in E do not belong to any path that determines the map and they can be removed. We say that a path is instrumental if it is the least index path for the DPO reachable for some interpretation. The reduction satisfies the following properties:

Lemma 1 If there exists an instrumental path pi under DPO PL that crosses edge e in B and reaches a non-zero leaf, then ∃ Io such that {leaf(pi), pi, Io} ∈ S and therefore e ∈ E′ .

Theorem 1 (soundness) If FODD B′ is the output of R12(B) for any FODD B, then ∀ interpretations I, MapB(I) = MapB′ (I).

Theorem 2 (completeness) If no path crossing edge e and reaching a non-zero leaf in B is instrumental under DPO PL, then R12 removes e.

While this does not provide a normal form for FODDs, i.e. two semantically equivalent diagrams can be reduced but have different syntax, it provides much stronger reduction power compared to previous work. E.g., R12 reduces the FODD in Figure 1(a) to Figure 1(b). Whenever a valuation reaches the 0.5 leaf there is another valuation traversing one of the two paths reaching the 1 leaf. However, neither of the path (or edge) formulas are individually implied by the formula for the path reaching the 0.5 leaf. Since all previous reductions are based on some notion of single path implication they are inapplicable. R12, on the other hand, is very flexible since it tracks reachability by way of model checking.

3 Generalized FODDs syntax and semantics

A significant extension to expressive power of FODDs can be obtained by changing the aggregation function. E.g., min aggregation leads to universal quantification. Other possible aggregation functions include ∑, mean, etc. We define Generalized FODDs as follows:

Definition 2 A Generalized First Order Decision Diagram (GFODD) is a 2-tuple <V,D>, where, V , the aggregation function, is an ordered list of distinct variables each associated with its own aggregation operator. D is a FODD except that the leaves can be labeled by a special character d (for discard).

GFODD semantics

The semantics follow the approach of FODDs except that the aggregation operation is now defined by V = [(op1v1 ) · · · (opnvn )]. Here every vi is a variable of the GFODD (ordered v1 to vn) and the corresponding opi is the aggregation operator associated with it. Consider the set of all possible valuations defined over the domain of interpretation I. Each valuation ζ is associated with a value MapB(I, ζ). We can now divide up these valuations into blocks. All valuations in a block have the same assignment of values to variables v1 · · · vn-1 but they differ in the value of the variable vn. We then collapse each block to a single valuation over variables v1 · · · vn-1 by eliminating the variable vn and replacing the set of associated values (MapB(I, ζ)) by their aggregate value produced by applying opn to the set. Any discard values in the block are removed before applying opn . If we do this for every block we are left with the set of all possible valuations defined over the variables v1 · · · vn-1 each associated with a value. We repeat the procedure for variables vn-1 to v1 to produce a final aggregate value, MapB(I), obtained by nesting aggregation operators with opn being the innermost.

where [v1 · · · vn] is the corresponding valuation. We illustrate this using the example in Figure 3 where GFODD B captures the following statement from the logistics domain: ∃c∀b, box b is in city c. The output of B is 10 if all boxes are in one city and 0 otherwise. Aggregation is done from right to left, one variable at a time. In the example, therefore, first aggregate the values MapB(I, ζ) over all assignments of the variable b, using the min operation, producing exactly one value per binding of variable c, and then aggregating all of the produced values over all bindings of variable c using the max operation. In this example, to keep the GFODD diagram simple, we assume the variables are typed and use only valuations that conform to the types of the variables. Had we used all possible valuations over the set of objects {b1, b2, c1, c2}, the diagram would have been more complicated as it would have had to represent ∃c, ∀b, box(b) → city(c) ∧ bin(b, c).

Combining GFODDs

Our Value Iteration algorithm requires operations max, + and × over functions defined by GFODDs. We perform these by GFODD combination.

Definition 3 GFODD B is a combination of GFODDs B1 and B2 under combination operator opc iff ∀ interpretations I, MapB(I) = MapB1 (I) opc MapB2 (I).

Definition 4 Combination operator opc and aggregation operator opa are a safe pair iff for any non-negative values x1, · · · , xk and non-negative constant b, opa (x1, · · · , xk) opc b = opa (x1 opc b, · · · , xk opc b).

E.g., aggregation operator max and combination operator + are a safe pair because for any set S = {c1 · · · cm} and constant b, max{c1 · · · cm} + b = max{c1 + b, · · · cm + b}. Aggregation operator mean and combination operator max are not a safe pair.

FODDs can be combined with the apply operation [Wang et al., 2008]. Apply produces a combination of 2 FODDs under combination operator opc by choosing the smaller root (according to the FODD predicate order) to be the root of the resultant FODD and then recursing on the subdiagrams. When the computation reaches the leaves, the result is opc applied to the leaf values. for GFODDs, if either leaf value is d, so is the result. The following Theorem shows that GFODDs can be combined leaving some freedom in the order of aggregation. We call the resulting procedure Ex-apply.

Theorem 3 Given GFODDs B1 = <V1,D1> and B2 = <V2,D2>, V1 ∩ V2 = φ, and combination operator opc, if all operators in V1 ∪ V2, form a safe pair with opc, D = apply(D1,D2, opc) and V is obtained by combining V1 and V2 in a way that preserves the order of variables within V1 and within V2, then B = <V,D> is a combination of B1 and B2.

4 R12 for Max*Min* Aggregation

The R12 reduction can be extended to GFODDs with min aggregation by defining generalized aggregation function min3 . min3 is just a dual of max3 except that no special treatment is given to paths reaching the 0 leaf and in the reduction procedure, targets of edges in E are replaced by d instead of 0. Since these edges are not instrumental in determining the map and d values are just discarded during aggregation, correctness is preserved.

We next extend R12 to GFODDs with max∗min∗ aggregation. In this case the aggregation function V consists of a series of zero or more max operators followed by a series of zero or more min operators. The corresponding case in first order logic has the quantifier prefix ∃∗∀∗ and is decidable. V can be written as V lV r , where V l and V r contain all max and min aggregated variables respectively. The set U of all possible valuations of the variables in diagram B can be split into U l and U r , the sets of all valuations over the variables in V l and V r . Thus, for all ζ ∈ U, ζ = ζ l ζ r where ζ l ∈ U l and ζ r ∈ U r . By the definition of GFODD semantics, for any interpretation I,

Consider evaluating B on some interpretation I. U can be viewed as divided into blocks, each corresponding to one valuation ζ l . During aggregation each block is collapsed under the min aggregation and the aggregate values of all blocks are collapsed under the max aggregation. Intuitively, as long as R12 preserves all paths reaching the smallest leaf (under a DPO) in every block under every interpretation, the map will also be preserved. Other paths can be removed. This does not reduce all edges possible, but it is easy to track. R12 for max∗min∗ aggregation is identical to the R12 procedure for min aggregation with the following exceptions.

1. The set U of all possible valuations is generated as follows. Ol and Or are disjoint sets of respectively |V l | and |V r | newly invented objects. U l and U r are the sets of all possible valuations of variables in V l and V r over Ol and Ol ∪ Or respectively. U = {ζ l ζ r | ζ l ∈ U l and ζ r ∈ U r }.

(2) The generalized aggregation function maxmin3 returns all the triplets generated by applying min3 to each block.

Figure 4 shows an example of this reduction. Here V l = Max(x) and V r = Min(y) making |V l | = |V r | = |Ol | = |Or | = 1. Therefore we invent Ol = {a} and Or = {b}. Notice that the table built by the procedure consists of a single block (since only one variable is associated with the max and so there is only one ζ l ) but in general this is repeated for every block. The targets of all edges other than the ones present in the paths of the resultant triplets (shown below the table) can be replaced by the value d. This reduction satisfies the following properties.

Lemma 2 If there exists a path pi reaching the smallest leaf (under the DPO PL) in some block under some interpretation and pi crosses e in B then ∃ Io such that {leaf(pi), pi, Io} ∈ S and thus e ∈ E′ .

Theorem 4 (soundness) For GFODD B with the max∗min∗ aggregation, if B′ = R12(B), then ∀ interpretations I, MapB(I) = MapB′ (I).

A closer examination of the discussion above shows that we can make more precise constraints on the values of edges participating in the evaluation of diagram B on interpretation I. In particular, the winning path must be preserved, the value of edges participating in the same block (using the same ζl) can go down but they must not be smaller than the final value, and edges in other blocks can be reduced to zero. Thus tighter bookkeeping may allow us to prune the diagram much more than the version of R12 given above. We leave this to be investigated in future work.

5 Value Iteration with GFODDs

Value Iteration with GFODDs is an instance of the SDP algorithm [Boutilier et al., 2001]. We restrict attention to cases where the reward function is represented by a GFODD with max∗min∗ aggregation function. The following discussion shows why our algorithm VI-GFODD produces the correct result for each of the following 4 steps of SDP.

Regression: The n - 1 step-to-go value function V n-1 is regressed over every deterministic variant aji of every action ai to produce RegV j i by replacing each node in V n-1 by its corresponding Truth Value Diagram (TVD) without changing the aggregation function. A TVD for a predicate under deterministic action aji describes conditions under which the predicate becomes true after aji is executed. Wang et al. [2008] impose the constraint that TVDs cannot include free variables and therefore regression is correct regardless of the aggregation function.

Add Action Variants: The Q-function QRega i = ΣjP r(aji )RegV j i for each action ai is generated by combining regressed diagrams using Ex-apply. Since all argument GFODDs to Ex-apply have max∗min∗ aggregation, by Theorem 3 all max operators can be pushed to the head of the aggregation function, and the result also has max∗min∗ aggregation. Correctness is guaranteed because both max and min form a safe pair with all combination operators required for Value Iteration (+, ×, and max).

Object Maximization: This involves converting action parameters in QRega i to max aggregated variables and appending these to the head of the aggregation function to produce Qai . Aggregation in Qai chooses a single binding for the new variables that provides the best value in QRega i over all action variants, thereby ensuring correctness. Again max∗min∗ aggregation is preserved in Qai .

Maximize over Actions: The n step-to-go value function V n = Maxi[R(S) + γQai ], is generated by combining diagrams using Ex-apply. As above, by Theorem 3 the result can be written using max∗min∗ aggregation.

Figure 5 shows an example of the algorithm using GFODDs for a simple domain with one deterministic action A(x∗ , y∗ ). Notice that the 2nd and 4th steps in the algorithm are not required in this case. The reward is 1 if ∃x, ∀y, p(x, y) and 0 otherwise. The action A(x∗ , y∗ ), is defined such that p(x, y) is true after the action if either p(x, y) was true before or q(x, y) was true and A(x, y) was performed. Since the action can make at most one p(x, y) true at a time, intuitively, the regressed diagram should capture the following conditions for returning a value of 1. Either ∃x, ∀y, p(x, y) or ∃x, such that for all but one y, p(x, y) is true and for that y, q(x, y) is true. It is easily verified that the resultant diagram captures these cases. The next theorem shows that the result is correct; using R12 we can also keep the diagrams compact.

Theorem 5 For any First Order MDP with a reward function of the form <max∗min∗ ,D>, algorithm VI-GFODD produces the correct value function at every iteration.

6 Conclusions and FutureWork

This paper significantly extends the representation power of first order decision diagrams and our algorithmic understanding of their reduction. Generalized FODDs allow for arbitrary aggregation functions and basic operations on them can be done just as in the existential case. In particular we can naturally capture and manipulate logical formulas with existential and universal quantifiers using max and min aggregation. In addition we show that first order Value Iteration can be supported in the more expressive setting. Previous implementations of first order Value Iteration [Sanner and Boutilier, 2009; Joshi and Khardon, 2008] have resorted to heuristic treatment of universal goals. Using the new formulation, this can be captured and handled naturally. The other main contribution in the paper is the idea and analysis of model checking reductions. The completeness result for the FODD case falls short of being a normal form, but is much stronger than previous reductions. Examples by Wang et al. [2008] using a simple decidable fragment show that for normal form we may need some syntactic manipulation of diagrams so going beyond completeness may be hard or expensive to compute.

This work suggests several questions for future. The model checking reduction can probably be improved by further analysis, as discussed in Section 4. The model checking reductions currently require enumeration of substitutions. A promising idea is to use a sample of interpretations, judicially chosen, and reduce the diagrams relative to these interpretations.