publication . Conference object . Preprint . 2017

A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations

Kaminski, Benjamin Lucien; Katoen, Joost-Pieter;
Open Access English
  • Published: 22 Mar 2017
  • Publisher: IEEE
  • Country: United Kingdom
Abstract
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-...
Subjects
free text keywords: Science & Technology, Technology, Computer Science, Theory & Methods, Logic, Computer Science, Science & Technology - Other Topics, PROGRAMS, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, D.2.4, D.3.1, F.1.2, F.3.1, F.3.2
Download fromView all 2 versions
UCL Discovery
Conference object . 2017
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue
publication . Conference object . Preprint . 2017

A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations

Kaminski, Benjamin Lucien; Katoen, Joost-Pieter;