Analyzing generalized planning under nondeterminism

摘要

In automated planning, there has been a recent interest in solving a class of problems, where a single solution applies for multiple, possibly infinitely many, instances. This necessitates a generalized notion of plans, such as plans with loops. However, the correctness of such plans is non-trivial to define, making it difficult to provide a clear specification of what we should be looking for. In an influential paper, Levesque proposed a formal specification for analyzing the correctness of such plans. He motivated a logical characterization within the situation calculus that included binary sensing actions. This characterization argued that from each state considered possible initially, the plan should terminate while satisfying the goal. Increasingly, classical plan structures are being applied to stochastic environments such as robotics applications. This raises the question as to what the specification for correctness should look like, since Levesque's account makes the assumption that actions are deterministic.