反例引导的规划

对抗性和不确定环境中的规划可以建模为在随机完美信息博弈中制定策略的问题。这些博弈是马尔可夫决策过程（MDP）的推广：有两个（对抗性）玩家和一个随机源。在这种博弈中计算获胜策略的主要实际障碍是状态空间的大小。因此，在实践中，人们通常使用模型的抽象。困难在于提出一个既不会太粗糙以至于移除所有获胜策略（计划），也不会太精细以至于难以处理的抽象。在验证中，反例引导的抽象细化范式已成功用于自动构建有用但简洁的抽象。我们将这一范式扩展到概率模型（即完美信息博弈，以及作为特例的MDP）。这使我们能够将反例引导的抽象范式应用于AI规划问题。作为特例，我们得到了自动构建系统抽象的MDP和确定性系统的规划算法。