Planning in Non-Deterministic Domains via Symbolic Model Checking

In the thesis is tackled the Artificial Intelligence (AI) problem of Automatic Planning using Symbolic Model Checking (SMC) techniques developed within the Formal Verification community for the verification of designs. The use of SMC techniques allowed for a formal definition and for an efficient handling of a large class of planning problems that classical planning systems developed within AI Planning are not able to deal with. In the thesis two restricting hypothesis of classical planning have been discarded. Planning domains are assumed to be non-deterministic and are modeled as non-deterministic finite state automata. Moreover, a planning domain can be partially observable at execution time. A formal characterization of solutions to different planning problem is provided, distinguishing among weak solutions (that may achieve the goal), strong solution (that guarantee goal achievement) and strong cyclic solutions (that capture a trial and error behavior guaranteeing goal achievement under `fair` executions); under different hypothesis of domain run-time observability (i.e., full, null and partial observability). A family of algorithms to synthesize solutions to the different planning problems characterized are provided and proved to be correct. The algorithms have been implemented in the Model Based Planner (MBP) using SMC techniques. An extensive experimental analysis is carried out to show the effectiveness of the proposed approach w.r.t. the other state of the art planners