Cheng, Tong

Title: Analyzing Probabilistic Programs with Dynamic Logic

Abstract: We present a unified framework for the analysis of probabilistic programs based on Dynamic Logic in which both iterative and recursive programs can be analyzed. We augment the traditional rules of probabilistic Dynamic Logic with rules for reasoning about assignments, as well as proof rules for recursive programs with call-by-value parameters. We show soundness of our system with respect to a standard Markov kernel semantics. We give an example of their use in the analysis of the Coupon Collector's Problem.

Publication: 2017 Logic and Computational Complexity Workshop (co-located with LICS)