Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Acta Informatica
Erschienen in: Acta Informatica 3/2019

15.05.2018 | Original Article

On the hardness of analyzing probabilistic programs

verfasst von: Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Erschienen in: Acta Informatica | Ausgabe 3/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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 \(\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\)-complete in the arithmetical hierarchy. Deciding positive almost-sure termination is shown to be \(\varSigma _2^0\)-complete, whereas its universal variant is \(\varPi _3^0\)-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\)- and \(\varSigma _2^0\)-complete, respectively. Deciding whether the expected value equals a given rational value is shown to be \(\varPi ^0_2\)-complete.
Covariances We show that computing upper and lower bounds on the covariance of two random variables is both \(\varSigma _2^0\)-complete. Deciding whether the covariance equals a given rational value is shown to be in \(\varDelta _3^0\). In addition, this problem is shown to be \(\varSigma ^0_2\)-hard as well as \(\varPi ^0_2\)-hard and thus a “proper” \(\varDelta _3^0\)-problem. All hardness results on covariances apply to variances as well.
Vorheriger Artikel Associative composition of components with double-sided interfaces

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
The left branch is executed with probability \(\nicefrac {1}{3}\) and the right branch with probability \(\nicefrac {2}{3}\).
 
2
i.e. \({\textsf {diverge}}\) is syntactic sugar for \({\textsf {while}}\, \left( {\textsf {true}} \right) \, \left\{ {{\textsf {skip}}} \right\} \).
 
3
The notion of valid inputs is needed due to our restriction that program states have finite domains. If we drop this restriction, the set of all program states becomes uncountable. Moreover, note that it is clearly decidable whether a program state is valid for a given program.
 
4
Note that we allow the values of the quantified variables to be drawn from a computable domain other than \(\mathbb {N}\) that could be encoded in the natural numbers such as \(\mathbb {Q}\), the set of syntactically correct programs, etc.
 
5
The last quantifier is universal if n is even and existential if n is odd.
 
6
In this context, a set is cofinite iff its relative complement, i.e. its complement with respect to some appropriate universe, is finite.
 
7
i.e. iff \(\mathbb {S}_P \setminus \{\sigma \in \mathbb {S}_P ~|~ (P,\, \sigma ) \in \mathcal {H} \}\) is finite.
 
8
This is because we ask for an a-priori expected value with respect to an initial state.
 
9
I.e. the postexpectation that maps every program state to constantly 1.
 
10
The \(\varepsilon \) in the \( T _k(\ldots ,\, \varepsilon )\) comes from the fact that \( T _k\) is supposed to simulate k steps of an ordinary program. The \(\varepsilon \) thus stands for an empty sequence of resolutions of probabilistic choices.
 
11
The program P cheers as it was able to prove the termination of Q on input \(g_Q(i)\).
 
12
The runtime of a program corresponds to the number of execution steps in our operational semantics of pGCL (Definition 3). If more fine-grained runtime models are considered that take, for instance, the size of numbers into account, a single program step can be simulated in at most polynomial time on a Turing machine. To this end, we first translate pGCL programs to programs on a random access machine and translate the resulting program to Turing machines (cf. [37, Theorem 2.5]). In particular, our reduction remains valid for such more fine-grained runtime models.
 
13
Rounding up the value of i to a natural number, i.e. computing \(\max \{\lceil i \rceil ,\, 0\}\), is a technical necessity: We assume that variable valuations range over \(\mathbb {Q}\) but the domain of \(g_Q\) is \(\mathbb {N}\).
 
14
As opposed to a smoothed analysis of an algorithm.
 
Literatur
1.
Arons, T., Pnueli, A., Zuck, L.D.: Parameterized Verification by Probabilistic Abstraction. In: FoSSaCS, LNCS, vol. 2620, pp. 87–102. Springer (2003)
2.
Ash, R.B., Doleans-Dade, C.: Probability and Measure Theory. Academic Press, Cambridge (2000)MATH
3.
Barthe, G., Köpf, B., Olmedo, F., Béguelin, S.Z.: Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst. 35(3), 9 (2013)CrossRefMATH
4.
5.
Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Proceedings of 16th International Conference on Term Rewriting and Applications, RTA 2005, Nara, Japan, April 19–21, 2005,LNCS, vol. 3467, pp. 323–337. Springer (2005)
6.
Bournez, O., Hoyrup, M.: Rewriting logic and probabilities. In: RTA, LNCS, vol. 2706, pp. 61–75. Springer (2003)
7.
Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV, LNCS, vol. 8044, pp. 511–526. Springer (2013)
8.
Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz’s. In: CAV (1), LNCS, vol. 9779, pp. 3–22. Springer (2016)
9.
Chatterjee, K., Fu, H., Novotný, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: POPL, pp. 327–342. ACM (2016)
10.
Davis, M.D.: Computability and Unsolvability. McGraw-Hill Series in Information Processing and Computers. McGraw-Hill, New York (1958)
11.
Davis, M.D.: Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science. Academic Press, Cambridge (1994)
12.
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)MATH
13.
Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: CAV, LNCS, vol. 7358, pp. 123–138. Springer (2012)
14.
Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL 2015, pp. 489–501. ACM (2015)
15.
Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: ESOP, LNCS, vol. 9632, pp. 282–309. Springer (2016)
16.
17.
Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Future of Software Engineering (FOSE), pp. 167–181. ACM (2014)
18.
Gretz, F., Katoen, J.P., McIver, A.: Operational versus Weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110–132 (2014)CrossRef
19.
Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. TOPLAS 5(3), 356–380 (1983)CrossRefMATH
20.
Jansen, N., Kaminski, B.L., Katoen, J.P., Olmedo, F., Gretz, F., McIver, A.: Conditioning in probabilistic programming. ENTCS 319, 199–216 (2015)MathSciNetMATH
21.
Kaminski, B.L., Katoen, J.P.: On the hardness of almost–sure termination. In: Proceedings of MFCS 2015, Part I, LNCS, vol. 9234, pp. 307–318. Springer (2015)
22.
Kaminski, B.L., Katoen, J.P., Matheja, C.: Inferring covariances for probabilistic programs. In: QEST 2016, pp. 191–206 (2016)
23.
Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. (2016). arXiv:​1601.​01001
24.
Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP, LNCS, vol. 9632, pp. 364–389. Springer (2016)
25.
Katoen, J., McIver, A., Meinicke, L., Morgan, C.C.: Linear-invariant generation for probabilistic programs: automated support for proof-based methods. In: SAS, LNCS, vol. 6337, pp. 390–406. Springer (2010)
26.
27.
Klenke, A.: Probability Theory: A Comprehensive Course. Springer, Berlin (2013)MATH
28.
29.
30.
dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. In: ESOP, LNCS, vol. 10201, pp. 393–419. Springer (2017)
31.
McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Berlin (2004)MATH
32.
McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new proof rule for almost-sure termination. In: POPL [to appear] (2018)
33.
Morgan, C.: Proof rules for probabilistic loops. In: Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing, p. 7. Springer Verlag (1996)
34.
Murawski, A., Ouaknine, J.: On probabilistic program equivalence and refinement. In: CONCUR, LNCS, vol. 3653, pp. 156–170. Springer (2005)
35.
Odifreddi, P.: Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers. Elsevier, Amsterdam (1992)MATH
36.
Odifreddi, P.: Classical Recursion Theory, vol. II. Elsevier, Amsterdam (1999)MATH
37.
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Boston (1994)MATH
38.
39.
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (2005)MATH
40.
Rogers, H.: Theory of Recursive Functions and Effective Computability, vol. 5. McGraw-Hill, New York (1967)MATH
41.
42.
Sneyers, J., de Schreye, D.: Probabilistic termination of CHRiSM Programs. In: LOPSTR, LNCS, vol. 7225, pp. 221–236. Springer (2011)
43.
44.
Ying, M.: Floyd–Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19 (2011)CrossRef
Metadaten
Titel
On the hardness of analyzing probabilistic programs
verfasst von
Benjamin Lucien Kaminski
Joost-Pieter Katoen
Christoph Matheja
Publikationsdatum
15.05.2018
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 3/2019
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-018-0321-1

Premium Partner

    Bildnachweise