Automatic OBDD-based generation of universal plans in non-deterministic domains

Most real world environments are non-deterministic. Automatic plan formation in non-deterministic do-mmns is, however, still an open problem. In this pa-per we present a practical algorithm for the automatic generation of solutions to planning problems in non-deterministic domains. Our approach has the following main features. First, the planner generates Universal Plans. Second, it generates plans which are guaranteed to achieve the goal in spite of non-determinism, if such plans exist. Otherwise, the planner generates plans which encode iterative trial-and-error strategies (e.g. try to pick up a block until succeed), which are guar-anteed to achieve the goal under the assumption that if there is a non-deterministic possibility for the iteration to terminate, this will not be ignored forever. Third, the implementation of the planner is based on symbolic model checking techniques which have been designed to explore efficiently large state spaces. The implementa-tion exploits the compactness of ORDDS (Ordered Bi-nary Decision Diagrams) to express in a practical way universal plans of extremely large size.