Programming and Reasoning with Partial Observability
summary
Presents belief programming plus Epistemic Hoare Logic and a new language BLIMP that treat program state as a set of environments and use box/diamond modalities to write proofs about belief states. Provides semantics and a soundness proof, an implementation using hash set belief states, and two case studies: a drone example that meets its feasibility threshold and a Mars Polar Lander model that requires coarser discretization to run but can be verified to avoid the reported crash under the nondeterministic model.
AI-written summary · about
chapters (6)
- 0:00Start
- 3:01Belief Programming
- 4:29Develop an Environment Model
- 4:43Loop Invariant
- 8:26The Choose Statement
- 9:35State Estimator
related talks
01h 02mprogrammingLanguage as Language;
27mScheme Pearl: Quantum Continuations
26mRapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
32mWhy Current AI Cannot Truly See the World
30mSymbolic Execution of Hadamard-Toffoli Quantum Circuits
50mThe Wonders of Abstraction
25mExponential separations using guarded extension variables
42mWhen Magic Executes Code