Kaminski, BL;
Katoen, J-P;
(2017)
A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations.
In:
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
IEEE: Reykjavik, Iceland.
Preview |
Text
main.pdf - Accepted Version Download (451kB) | Preview |
Abstract
We present a weakest–precondition–style calculus for reasoning about the expected values (pre–expectations) of 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.
| Type: | Proceedings paper |
|---|---|
| Title: | A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations |
| Event: | 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
| Location: | Reykjavik, IRELAND |
| Dates: | 20 June 2017 - 23 June 2017 |
| Open access status: | An open access version is available from UCL Discovery |
| Publisher version: | https://dl.acm.org/doi/10.5555/3329995.3330088 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Science & Technology, Technology, Computer Science, Theory & Methods, Logic, Computer Science, Science & Technology - Other Topics, PROGRAMS |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10089601 |
Archive Staff Only
 |
View Item |
