Decision-theoretic planning with generalized first-order decision diagrams

Many tasks in AI require representation and manipulation of complex functions. First-Order Decision Diagrams (FODD) are a compact knowledge representation expressing functions over relational structures. They represent numerical functions that, when constrained to the Boolean range, use only existential quantification. Previous work has developed a set of operations for composition and for removing redundancies in FODDs, thus keeping them compact, and showed how to successfully employ FODDs for solving large-scale stochastic planning problems through the formalism of relational Markov decision processes (RMDP). In this paper, we introduce several new ideas enhancing the applicability of FODDs. More specifically, we first introduce Generalized FODDs (GFODD) and composition operations for them, generalizing FODDs to arbitrary quantification. Second, we develop a novel approach for reducing (G)FODDs using model checking. This yields - for the first time - a reduction that maximally reduces the diagram for the FODD case and provides a sound reduction procedure for GFODDs. Finally we show how GFODDs can be used in principle to solve RMDPs with arbitrary quantification, and develop a complete solution for the case where the reward function is specified using an arbitrary number of existential quantifiers followed by an arbitrary number of universal quantifiers.