Rune M. Jensen and Manuela M. Veloso
Model checking representation and search techniques were recently shown to be efficiently applicable to planning, in particular to non-deterministic planning. Ordered Binary Decision Diagrams ( obdd s) encode a planning domain as a non-deterministic finite automaton (NFA) and fast algorithms from model checking search for a solution plan. With proper encodings, obdd s can effectively scale and can provide universal plans for complex planning domains. We are particularly interested in addressing the complexities arising in non-deterministic, multi-agent domains. In this paper, we present umop, a new universal obdd -based planning framework applicable to non-deterministic and multi-agent domains. We introduce a new planning domain description language, NADL, to include the specification of such non-deterministic, multiagent domains. The language contributes the explicit definition of controllable agents and uncontrollable environment agents. We describe the syntax and semantics of NADL and show how to build an efficient obdd-based representation of an NADL description. The umop planning systems uses NADL and it includes the previously developed strong and strong cyclic planning algorithms (Cimatti et al., 1998a, 1998b). In addition, we introduce a new optimistic planning algorithm, which relaxes optimality guarantees and generates plausible universal plans in some domains where no strong or strong cyclic solution exists. We present empirical results in a previously tested non-deterministic domains. We also introduce three new multi-agent domains with complex environment actions. Umop is shown to be a rich and efficient planning system.