Algebraic Program Analysis of Probabilistic Programs

The following summary was generated by AI from the slides.

This talk presents an algebraic framework for analyzing probabilistic programs using Markov algebras, which unify sequencing, probabilistic branching, and nondeterministic choice into a partially-ordered semiring structure. Newton’s method is lifted to Markov algebras via explicit syntactic differentiation rules for all operators — sequencing, probabilistic choice, and nondeterministic choice — yielding superlinearly convergent fixed-point computation over the resulting equation systems. Case studies on termination-probability and moment-of-reward analysis illustrate the framework’s reach over programs with probabilistic, demonic, and conditional branching.