A Language and Logic for Programming and Reasoning with Partial Observability
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 o...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2024
|
| Online Access: | https://hdl.handle.net/1721.1/153840 https://orcid.org/0000-0002-8396-1258 |
| _version_ | 1826194176035782656 |
|---|---|
| author | Atkinson, Eric Hamilton |
| author2 | Carbin, Michael |
| author_facet | Carbin, Michael Atkinson, Eric Hamilton |
| author_sort | Atkinson, Eric Hamilton |
| collection | MIT |
| description | 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 dissertation, I will present programming language tools that enable developers to deliver correct software in partially-observable environments. In particular, I will present belief programming, a new type of programming 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 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 naïve 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 and reasoning about efficient state estimators. |
| first_indexed | 2024-09-23T09:51:47Z |
| format | Thesis |
| id | mit-1721.1/153840 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T09:51:47Z |
| publishDate | 2024 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1538402024-03-22T03:57:27Z A Language and Logic for Programming and Reasoning with Partial Observability Atkinson, Eric Hamilton Carbin, Michael Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science 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 dissertation, I will present programming language tools that enable developers to deliver correct software in partially-observable environments. In particular, I will present belief programming, a new type of programming 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 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 naïve 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 and reasoning about efficient state estimators. Ph.D. 2024-03-21T19:09:32Z 2024-03-21T19:09:32Z 2024-02 2024-02-21T17:18:36.381Z Thesis https://hdl.handle.net/1721.1/153840 https://orcid.org/0000-0002-8396-1258 In Copyright - Educational Use Permitted Copyright retained by author(s) https://rightsstatements.org/page/InC-EDU/1.0/ application/pdf Massachusetts Institute of Technology |
| spellingShingle | Atkinson, Eric Hamilton A Language and Logic for Programming and Reasoning with Partial Observability |
| title | A Language and Logic for Programming and Reasoning with Partial Observability |
| title_full | A Language and Logic for Programming and Reasoning with Partial Observability |
| title_fullStr | A Language and Logic for Programming and Reasoning with Partial Observability |
| title_full_unstemmed | A Language and Logic for Programming and Reasoning with Partial Observability |
| title_short | A Language and Logic for Programming and Reasoning with Partial Observability |
| title_sort | language and logic for programming and reasoning with partial observability |
| url | https://hdl.handle.net/1721.1/153840 https://orcid.org/0000-0002-8396-1258 |
| work_keys_str_mv | AT atkinsonerichamilton alanguageandlogicforprogrammingandreasoningwithpartialobservability AT atkinsonerichamilton languageandlogicforprogrammingandreasoningwithpartialobservability |