A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations

Preprint English OPEN
Kaminski, Benjamin Lucien; Katoen, Joost-Pieter;
(2017)
  • Subject: Computer Science - Programming Languages | D.2.4 | D.3.1 | Computer Science - Logic in Computer Science | F.3.2 | F.3.1 | F.1.2
    acm: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
    arxiv: Computer Science::Logic in Computer Science

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 iterativ... View more
  • References (20)
    20 references, page 1 of 2

    [1] A. D. Gordon, T. A. Henzinger, A. V. Nori, and S. K. Rajamani, “Probabilistic Programming,” in Future of Software Engineering (FOSE). ACM, 2014, pp. 167-181.

    [2] E. W. Dijkstra, A Discipline of Programming. Prentice Hall, 1976.

    [3] A. McIver and C. Morgan, Abstraction, Refinement and Proof for Probabilistic Systems. Springer, 2004.

    [4] D. Kozen, “A probabilistic PDL,” J. Comput. Syst. Sci., vol. 30, no. 2, pp. 162-178, 1985.

    [5] C. Jones, “Probabilistic non-determinism,” Ph.D. dissertation, University of Edinburgh. College of Science and Engineering. School of Informatics., 1990.

    [6] E. C. R. Hehner, “A Probability Perspective,” Formal Aspects of Computing, vol. 23, no. 4, pp. 391-419, 2011.

    [7] B. L. Kaminski, J. Katoen, C. Matheja, and F. Olmedo, “Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs,” in ESOP, ser. LNCS, vol. 9632. Springer, 2016, pp. 364-389.

    [8] F. Olmedo, B. L. Kaminski, J. Katoen, and C. Matheja, “Reasoning about Recursive Probabilistic Programs,” in LICS. ACM/IEEE, 2016, pp. 672-681.

    [9] A. McIver and C. Morgan, “Partial Correctness for Probabilistic Demonic Programs,” Theor. Comput. Sci., vol. 266, no. 1-2, pp. 513-541, 2001.

    [10] J. Hurd, “A Formal Approach to Probabilistic Termination,” in Theorem Proving in Higher Order Logics (TPHOL), ser. LNCS. Springer Berlin Heidelberg, 2002, vol. 2410, pp. 230-245.

  • Similar Research Results (1)
  • Related Organizations (2)
  • Metrics
Share - Bookmark