Doctoral Thesis: A Language and Logic for Programming and Reasoning with Partial Observability
Eric H. Atkinson
Computer systems are increasingly deployed in partially-observable environments, in which the system cannot directly determine the environment’s state but receives partial information from observations. When such a computer system executes, it risks forming an incorrect belief about the true state of the environment. For example, the Mars Polar Lander (MPL) is a lost space probe that crashed because its control software believed it was on the Martian surface when it was actually 40m high, and as a result, it turned off its descent engine too early. Developers need better software development tools to prevent such accidents.
In this talk, I will present a new type of programming language and corresponding program logic that enable developers to deliver correct software in partially-observable environments. In particular, I will present belief programming, a language in which developers write a model of the partial observability in the environment. The language produces an executable state estimator, which is a function that maps environmental observations to estimates of the environment’s true state. I have implemented the prototype belief programming language BLIMP, and used BLIMP to implement several example programs including an engine controller for the MPL. I will also present in this talk Epistemic Hoare Logic (EHL), a program logic for belief programs that enables developers to reason about properties of the resulting state estimators. I have used EHL to prove that the BLIMP version of the MPL does not have the error that caused the original MPL to crash. Furthermore, I will present semi-symbolic inference, a technique that provides more efficient implementations of belief programming languages. Across a range of benchmarks, my performance experiments show that a semi-symbolic BLIMP implementation achieves speedups of 515x-58,919x over a naive BLIMP implementation. Together, the contributions of belief programming, EHL, and semi-symbolic inference enable developers to focus on modeling the partial observability in the environment, and provide programming language support for automatically generating efficient state estimators and reasoning about their properties.
Thesis Supervisor: Prof. Michael Carbin
- Date: Wednesday, September 27
- Time: 1:00 pm - 2:30 pm
- Category: Thesis Defense
- Location: 32-D463 (Star)