LAUSR

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 $$\sigma $$σ...1....does P terminate with probability 1 on input $$\sigma $$σ? (almost-sure termination)2....is the expected time until P terminates on input $$\sigma $$σ 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 $$\varPi ^0_2$$Π20-complete in the arithmetical hierarchy. Deciding positive almost-sure termination is shown to be $$\varSigma _2^0$$Σ20-complete, whereas its universal variant is $$\varPi _3^0$$Π30-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 $$\varSigma _1^0$$Σ10- and $$\varSigma _2^0$$Σ20-complete, respectively. Deciding whether the expected value equals a given rational value is shown to be $$\varPi ^0_2$$Π20-complete.Covariances We show that computing upper and lower bounds on the covariance of two random variables is both $$\varSigma _2^0$$Σ20-complete. Deciding whether the covariance equals a given rational value is shown to be in $$\varDelta _3^0$$Δ30. In addition, this problem is shown to be $$\varSigma ^0_2$$Σ20-hard as well as $$\varPi ^0_2$$Π20-hard and thus a “proper” $$\varDelta _3^0$$Δ30-problem. All hardness results on covariances apply to variances as well.