東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

A Language and Logic for Programming...

Atkinson, Eric Hamilton.

Linked to FindBook

Google Book

Amazon

博客來

A Language and Logic for Programming and Reasoning With Partial Observability.

Record Type:	Electronic resources : Monograph/item
Title/Author:	A Language and Logic for Programming and Reasoning With Partial Observability./
Author:	Atkinson, Eric Hamilton.
Published:	Ann Arbor : ProQuest Dissertations & Theses, : 2024,
Description:	133 p.
Notes:	Source: Dissertations Abstracts International, Volume: 86-05, Section: A.
Contained By:	Dissertations Abstracts International86-05A.
Subject:	Syntax. -
Online resource:	https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31652307
ISBN:	9798346385530

A Language and Logic for Programming and Reasoning With Partial Observability.
Atkinson, Eric Hamilton.

A Language and Logic for Programming and Reasoning With Partial Observability. - Ann Arbor : ProQuest Dissertations & Theses, 2024 - 133 p.

Source: Dissertations Abstracts International, Volume: 86-05, Section: A.

Thesis (Ph.D.)--Massachusetts Institute of Technology, 2024.

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 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 and reasoning about efficient state estimators.

ISBN: 9798346385530Subjects--Topical Terms:

897045
Syntax.

A Language and Logic for Programming and Reasoning With Partial Observability.
LDR:03171nmm a2200313 4500 001 2404543
005 20241213095603.5
006 m o d
007 cr#unu||||||||
008 251215s2024 ||||||||||||||||| ||eng d
020 $a 9798346385530
035 $a (MiAaPQ)AAI31652307
035 $a (MiAaPQ)MIT1721_1_153840
035 $a AAI31652307
040 $a MiAaPQ $c MiAaPQ
100 1 $a Atkinson, Eric Hamilton. $3 3774858
245 1 2 $a A Language and Logic for Programming and Reasoning With Partial Observability.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2024
300 $a 133 p.
500 $a Source: Dissertations Abstracts International, Volume: 86-05, Section: A.
500 $a Advisor: Carbin, Michael.
502 $a Thesis (Ph.D.)--Massachusetts Institute of Technology, 2024.
520 $a 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 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 and reasoning about efficient state estimators.
590 $a School code: 0753.
650 4 $a Syntax. $3 897045
650 4 $a Mars. $3 3687764
650 4 $a Linguistics. $3 524476
690 $a 0290
710 2 $a Massachusetts Institute of Technology. $b Department of Electrical Engineering and Computer Science. $3 3764399
773 0 $t Dissertations Abstracts International $g 86-05A.
790 $a 0753
791 $a Ph.D.
792 $a 2024
793 $a English
856 4 0 $u https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31652307