Verifying probabilistic programs requires reasoning about various probabilistic behaviors, e.g., random sampling, nondeterminism, and conditioning, against multiple quantitative properties, e.g., assertion-violation probabilities, moments, and expected running times. It is desirable and theoretically significant to have a unified framework which can deal with quantitative analysis of programs with different probabilistic behaviors and properties. In this paper, we present a unified framework for the quantitative analysis of probabilistic programs, which incorporates and extends existing results on the analysis of termination, temporal properties, and expected cost. We show that these quantitative properties of a general probabilistic program can be characterized as solutions to equation systems of the corresponding Markov chain counterpart with a possibly uncountable state space. Based on such characterization, we propose sufficient conditions to establish upper and lower bounds on these quantitative properties. Moreover, we demonstrate how our approach can be adapted to address inference problems in Bayesian programming.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Unified Framework for Quantitative Analysis of Probabilistic Programs

  • Shenghua Feng,
  • Tengshun Yang,
  • Mingshuai Chen,
  • Naijun Zhan

摘要

Verifying probabilistic programs requires reasoning about various probabilistic behaviors, e.g., random sampling, nondeterminism, and conditioning, against multiple quantitative properties, e.g., assertion-violation probabilities, moments, and expected running times. It is desirable and theoretically significant to have a unified framework which can deal with quantitative analysis of programs with different probabilistic behaviors and properties. In this paper, we present a unified framework for the quantitative analysis of probabilistic programs, which incorporates and extends existing results on the analysis of termination, temporal properties, and expected cost. We show that these quantitative properties of a general probabilistic program can be characterized as solutions to equation systems of the corresponding Markov chain counterpart with a possibly uncountable state space. Based on such characterization, we propose sufficient conditions to establish upper and lower bounds on these quantitative properties. Moreover, we demonstrate how our approach can be adapted to address inference problems in Bayesian programming.