Programming and reasoning with partial observability
© 2020 Owner/Author. 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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2021
|
| Online Access: | https://hdl.handle.net/1721.1/134213 |
| _version_ | 1826191780549230592 |
|---|---|
| author | Atkinson, Eric Carbin, Michael |
| author_facet | Atkinson, Eric Carbin, Michael |
| author_sort | Atkinson, Eric |
| collection | MIT |
| description | © 2020 Owner/Author. 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. |
| first_indexed | 2024-09-23T09:01:10Z |
| format | Article |
| id | mit-1721.1/134213 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T09:01:10Z |
| publishDate | 2021 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1342132021-10-28T04:49:36Z Programming and reasoning with partial observability Atkinson, Eric Carbin, Michael © 2020 Owner/Author. 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. 2021-10-27T20:04:01Z 2021-10-27T20:04:01Z 2020 2021-09-27T14:38:11Z Article http://purl.org/eprint/type/ConferencePaper https://hdl.handle.net/1721.1/134213 en 10.1145/3428268 Proceedings of the ACM on Programming Languages Creative Commons Attribution NonCommercial License 4.0 https://creativecommons.org/licenses/by-nc/4.0/ application/pdf Association for Computing Machinery (ACM) ACM |
| spellingShingle | Atkinson, Eric Carbin, Michael Programming and reasoning with partial observability |
| title | Programming and reasoning with partial observability |
| title_full | Programming and reasoning with partial observability |
| title_fullStr | Programming and reasoning with partial observability |
| title_full_unstemmed | Programming and reasoning with partial observability |
| title_short | Programming and reasoning with partial observability |
| title_sort | programming and reasoning with partial observability |
| url | https://hdl.handle.net/1721.1/134213 |
| work_keys_str_mv | AT atkinsoneric programmingandreasoningwithpartialobservability AT carbinmichael programmingandreasoningwithpartialobservability |