UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

On the hardness of analyzing probabilistic programs

Kaminski, BL; Katoen, J-P; Matheja, C; (2019) On the hardness of analyzing probabilistic programs. Acta Informatica , 56 (3) pp. 255-285. 10.1007/s00236-018-0321-1. Green open access

[thumbnail of main.pdf]
Preview
Text
main.pdf - Accepted Version

Download (491kB) | Preview

Abstract

We study the hardness of deciding probabilistic termination as well as the hardness of approximating expected values (e.g. of program variables) and (co)variances for probabilistic programs. Termination We distinguish two notions of probabilistic termination: Given a program P and an input σ ... 1. ...does P terminate with probability 1 on input σ ? (almost-sure termination) 2. ...is the expected time until P terminates on input σ finite? (positive almost-sure termination) For both of these notions, we also consider their universal variant, i.e. given a program P, does P terminate on all inputs? We show that deciding almost-sure termination as well as deciding its universal variant is Π02 -complete in the arithmetical hierarchy. Deciding positive almost-sure termination is shown to be Σ02 -complete, whereas its universal variant is Π03 -complete. Expected values Given a probabilistic program P and a random variable f mapping program states to rationals, we show that computing lower and upper bounds on the expected value of f after executing P is Σ01 - and Σ02 -complete, respectively. Deciding whether the expected value equals a given rational value is shown to be Π02 -complete. Covariances We show that computing upper and lower bounds on the covariance of two random variables is both Σ02 -complete. Deciding whether the covariance equals a given rational value is shown to be in Δ03 . In addition, this problem is shown to be Σ02 -hard as well as Π02 -hard and thus a “proper” Δ03 -problem. All hardness results on covariances apply to variances as well.

Type: Article
Title: On the hardness of analyzing probabilistic programs
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/s00236-018-0321-1
Publisher version: https://doi.org/10.1007/s00236-018-0321-1
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.
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/10089603
Downloads since deposit
72Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item