A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations
2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS)(2017)
摘要
We present a weakest-precondition-style calculus for reasoning about the expected values (pre-expectations) of \emph{mixed-sign unbounded} random variables after execution of a probabilistic program. The semantics of a while-loop is well-defined as the limit of iteratively applying a functional to a zero-element just as in the traditional weakest pre-expectation calculus, even though a standard least fixed point argument is not applicable in this context. A striking feature of our semantics is that it is always well-defined, even if the expected values do not exist. We show that the calculus is sound, allows for compositional reasoning, and present an invariant-based approach for reasoning about pre-expectations of loops.
更多查看译文
关键词
weakest-precondition-style calculus,expected values,mixed-sign unbounded random variables,probabilistic program,while-loop semantics,zero-element,compositional reasoning,invariant-based approach
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络