Computer programs are increasingly being deployed in partially-observable environments. A partially observable environment is an environment whose state is not completely visible to the program, but from which the program receives partial observations. Developers typically deal with partial observability by writing a state estimator that, given observations, attempts to deduce the hidden state of the environment. In safety-critical domains, to formally verify safety properties developers may write an environment model. The model captures the relationship between observations and hidden states and is used to prove the software correct.
In this paper, we present a new methodology for writing and verifying programs in partially observable environments. We present belief programming, a programming methodology where developers write an environment model that the program runtime automatically uses to perform state estimation. A belief program dynamically updates and queries a belief state that captures the possible states the environment could be in. To enable verification, we present Epistemic Hoare Logic that reasons about the possible belief states of a belief program the same way that classical Hoare logic reasons about the possible states of a program. We develop these concepts by defining a semantics and a program logic for a simple core language called BLIMP. In a case study, we show how belief programming could be used to write and verify a controller for the Mars Polar Lander in BLIMP. We present an implementation of BLIMP called CBLIMP and evaluate it to determine the feasibility of belief programming.
RWTH Aachen University（亚琛工业大学）；Saarland University（萨尔大学）；University College London（伦敦大学学院）
我们研究加权规划，指定数学模型的编程范式。更具体地说，我们研究的加权程序就像通常的命令式程序一样，具有两个额外的功能：（1）不确定性分支和（2）加权执行轨迹。权重可以是数字，也可以是其他对象，如字母表中的单词、多项式、形式幂级数或基数。我们认为，加权规划作为一种范式，可以用来指定数学模型超越概率分布（如概率规划）。我们开发了最弱的预条件和最弱的自由预条件风格的演算à la Dijkstra，用于推理加权程序指定的数学模型。我们提出了几个案例研究。例如，我们使用加权规划来模拟滑雪租赁问题-一个优化问题。我们不仅模型的优化问题本身，而且最好的确定性在线算法解决这个问题的加权程序。通过最弱前提式推理，可以在源代码级确定在线算法的竞争比。
