國立虎尾科技大學 |

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

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	A Language and Logic for Programming and Reasoning With Partial Observability./
Author:	Atkinson, Eric Hamilton.
Description:	1 online resource (133 pages)
Notes:	Source: Dissertations Abstracts International, Volume: 86-05, Section: A.
Contained By:	Dissertations Abstracts International86-05A.
Subject:	Syntax. -
Online resource:	click for full text (PQDT)
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. - 1 online resource (133 pages)

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

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

Includes bibliographical references

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.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2024

Mode of access: World Wide Web

ISBN: 9798346385530Subjects--Topical Terms:

671699
Syntax.
Index Terms--Genre/Form:

554714
Electronic books.

A Language and Logic for Programming and Reasoning With Partial Observability.
LDR:03395ntm a22003257 4500 001 1152797
005 20241213095603.5
006 m o d
007 cr mn ---uuuuu
008 250605s2024 xx obm 000 0 eng d
020 $a 9798346385530
035 $a (MiAaPQ)AAI31652307
035 $a (MiAaPQ)MIT1721_1_153840
035 $a AAI31652307
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Atkinson, Eric Hamilton. $3 1479884
245 1 2 $a A Language and Logic for Programming and Reasoning With Partial Observability.
264 0 $c 2024
300 $a 1 online resource (133 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
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.
504 $a Includes bibliographical references
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.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2024
538 $a Mode of access: World Wide Web
650 4 $a Syntax. $3 671699
650 4 $a Mars. $3 1479885
650 4 $a Linguistics. $3 557829
655 7 $a Electronic books. $2 local $3 554714
690 $a 0290
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a Massachusetts Institute of Technology. $b Department of Electrical Engineering and Computer Science. $3 1467552
773 0 $t Dissertations Abstracts International $g 86-05A.
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=31652307 $z click for full text (PQDT)