关于含循环与噪声的计划

在一篇有影响力的论文中，Levesque提出了一种形式化规范，用于分析类程序计划（如条件计划、迭代计划和基于知识的计划）的正确性。他动机于包含二元感知动作的情境演算中的逻辑刻画。尽管该刻画不能立即产生实用算法，此规范可作为通用骨架，以探索针对合理、可处理片段的类程序计划的综合。经典计划结构正日益应用于随机环境，如机器人应用。这就提出了正确性的规范应当如何的问题，因为Levesque的论述假设感知精确且动作确定。基于用于推理信念程度与噪声的情境演算理论，我们重访广义计划的执行语义。该规范随后被用于分析示例计划的正确性。