{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/153840"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/153840","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"A Language and Logic for Programming and Reasoning with Partial Observability","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Atkinson, Eric Hamilton"],"institution":"Massachusetts Institute of Technology","degree_name":"Doctoral","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Carbin, Michael"],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-02","date_published":"2024-02","updated_at":"2026-07-22T22:21:06Z","subjects":[],"languages":[],"rights":["In Copyright - Educational Use Permitted","Copyright retained by author(s)"],"rights_urls":["https://rightsstatements.org/page/InC-EDU/1.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/153840","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Carbin, Michael"]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"]},{"key":"dc:creator","label":"Author","values":["Atkinson, Eric Hamilton"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2024-03-21T19:09:32Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2024-03-21T19:09:32Z"]},{"key":"dc:date.issued","label":"Date","values":["2024-02"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctoral","Doctor of Philosophy"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright - Educational Use Permitted","Copyright retained by author(s)"]},{"key":"dc:rights.uri","label":"Rights URI","values":["https://rightsstatements.org/page/InC-EDU/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/153840"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Ph.D."]},{"key":"dc:title","label":"Title","values":["A Language and Logic for Programming and Reasoning with Partial Observability"]}]}],"canonical_facts":{"dc:contributor.advisor":["Carbin, Michael"],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"],"dc:creator":["Atkinson, Eric Hamilton"],"dc:date.accessioned":["2024-03-21T19:09:32Z"],"dc:date.available":["2024-03-21T19:09:32Z"],"dc:date.issued":["2024-02"],"dc:description.abstract":["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."],"dc:description.degree":["Ph.D."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/153840"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["In Copyright - Educational Use Permitted","Copyright retained by author(s)"],"dc:rights.uri":["https://rightsstatements.org/page/InC-EDU/1.0/"],"dc:title":["A Language and Logic for Programming and Reasoning with Partial Observability"],"dc:type":["Thesis"],"thesis:degree_name":["Doctoral","Doctor of Philosophy"]},"updated_at":"2026-07-22T22:21:06Z"}