Planning under Uncertainty in Linear Time Logic

The planning as satisfiability approach for classical planning establishes a correspondence between planning problems and logical theories, and, consequently, between plans and models. This work proposes a similar framework for contingency planning: considering contingent planning problems where the sources of indeterminism are incomplete knowledge about the initial state, non-inertial fluents and nondeterministic actions, it shows how to encode such problems into Linear Time Logic. Exploiting the semantics of the logic, and the notion of conditioned model introduced in this work, a formal characterization is given of the notion of contingent plan (a plan together with the set of conditions that ensure its executability).