Skip to main content
SpringerLink
Log in

Termination of Nondeterministic Probabilistic Programs

  • Conference paper
  • First Online:
Book cover Verification, Model Checking, and Abstract Interpretation (VMCAI 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11388))

Abstract

We study the termination problem for nondeterministic probabilistic programs. We consider the bounded termination problem that asks whether the supremum of the expected termination time over all schedulers is bounded. First, we show that ranking supermartingales (RSMs) are both sound and complete for proving bounded termination over nondeterministic probabilistic programs. For nondeterministic probabilistic programs a previous result claimed that RSMs are not complete for bounded termination, whereas our result corrects the previous flaw and establishes completeness with a rigorous proof. Second, we present the first sound approach to establish lower bounds on expected termination time through RSMs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Agrawal, S., Chatterjee, K., Novotný, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. PACMPL 2(POPL), 34:1–34:32 (2018)

    Google Scholar 

  2. Avanzini, M., Dal Lago, U., Yamada, A.: On probabilistic term rewriting. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 132–148. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_9

    Chapter  Google Scholar 

  3. Avanzini, M., Lago, U.D., Yamada, A.: On probabilistic term rewriting. CoRR abs/1802.09774 (2018). http://arxiv.org/abs/1802.09774

  4. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  5. Barthe, G., Espitau, T., Grégoire, B., Hsu, J., Strub, P.: Proving expected sensitivity of probabilistic programs. PACMPL 2(POPL), 57:1–57:29 (2018)

    Google Scholar 

  6. Barthe, G., Grégoire, B., Hsu, J., Strub, P.: Coupling proofs are probabilistic product programs. In: Castagna and Gordon [11], pp. 161–174 (2017)

    Article  Google Scholar 

  7. Billingsley, P.: Probability and Measure, 3rd edn. Wiley, Hoboken (1995)

    MATH  Google Scholar 

  8. Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: RTA, pp. 323–337 (2005)

    Google Scholar 

  9. Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: CAV, pp. 491–504 (2005)

    Google Scholar 

  10. Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: ICALP, pp. 1349–1361 (2005)

    Google Scholar 

  11. Castagna, G., Gordon, A.D. (eds.): Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017. ACM (2017)

    Google Scholar 

  12. Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV, pp. 511–526 (2013)

    Chapter  Google Scholar 

  13. Chatterjee, K., Fu, H.: Termination of nondeterministic recursive probabilistic programs. CoRR abs/1701.02944 (2017). http://arxiv.org/abs/1701.02944

  14. Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz’s. In: CAV, pp. 3–22 (2016)

    Google Scholar 

  15. 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 (2016)

    Article  Google Scholar 

  16. Chatterjee, K., Novotný, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Castagna and Gordon [11], pp. 145–160 (2017)

    Article  Google Scholar 

  17. Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_39

    Chapter  Google Scholar 

  18. Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: TACAS, pp. 67–81 (2001)

    Google Scholar 

  19. Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS, pp. 47–61 (2013)

    Google Scholar 

  20. Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_1

    Chapter  MATH  Google Scholar 

  21. Cusumano-Towner, M., Bichsel, B., Gehr, T., Vechev, M.T., Mansinghka, V.K.: Incremental inference for probabilistic programs. In: Foster and Grossman [27], pp. 571–585 (2018)

    Article  Google Scholar 

  22. Durrett, R.: Probability: Theory and Examples, 2nd edn. Duxbury Press, Boston (1996)

    MATH  Google Scholar 

  23. Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: CAV, pp. 123–138 (2012)

    Google Scholar 

  24. Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL, pp. 489–501 (2015)

    Google Scholar 

  25. Floyd, R.W.: Assigning meanings to programs. Math. Asp. Comput. Sci. 19, 19–33 (1967)

    Article  MathSciNet  Google Scholar 

  26. Foster, F.G.: On the stochastic matrices associated with certain queuing processes. Ann. Math. Stat. 24(3), 355–360 (1953)

    Article  MathSciNet  Google Scholar 

  27. Foster, J.S., Grossman, D. (eds.): Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, 18–22 June 2018. ACM (2018)

    Google Scholar 

  28. Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic netKAT. In: Thiemann [56], pp. 282–309 (2016)

    Chapter  Google Scholar 

  29. Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 550–567. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_37

    Chapter  Google Scholar 

  30. Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Herbsleb, J.D., Dwyer, M.B. (eds.) Proceedings of the on Future of Software Engineering, FOSE 2014, Hyderabad, India, 31 May–7 June 2014, pp. 167–181. ACM (2014)

    Google Scholar 

  31. Hart, S., Sharir, M.: Concurrent probabilistic programs, or: How to schedule if you must. SIAM J. Comput. 14(4), 991–1012 (1985)

    Article  MathSciNet  Google Scholar 

  32. Hesselink, W.H.: Proof rules for recursive procedures. Formal Asp. Comput. 5(6), 554–570 (1993)

    Article  Google Scholar 

  33. Howard, H.: Dynamic Programming and Markov Processes. MIT Press, Cambridge (1960)

    MATH  Google Scholar 

  34. Jones, C.: Probabilistic non-determinism. Ph.D. thesis, The University of Edinburgh (1989)

    Google Scholar 

  35. Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1), 99–134 (1998)

    Article  MathSciNet  Google Scholar 

  36. Kaelbling, L.P., Littman, M.L., Moore, A.W.: Reinforcement learning: a survey. JAIR 4, 237–285 (1996)

    Article  Google Scholar 

  37. Kaminski, B.L., Katoen, J.-P.: On the hardness of almost–sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 307–318. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48057-1_24

    Chapter  Google Scholar 

  38. Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: Thiemann [56], pp. 364–389 (2016)

    Chapter  Google Scholar 

  39. Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. D. Van Nostrand Company, New York City (1966)

    MATH  Google Scholar 

  40. Kura, S., Urabe, N., Hasuo, I.: Tail probabilities for randomized program runtimes via martingales for higher moments. CoRR abs/1811.06779 (2018). http://arxiv.org/abs/1811.06779

  41. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  42. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81–92 (2001)

    Google Scholar 

  43. McIver, A., Morgan, C.: Developing and reasoning about probabilistic programs in pGCL. In: PSSE, pp. 123–155 (2004)

    Chapter  Google Scholar 

  44. McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005). https://doi.org/10.1007/b138392

    Book  MATH  Google Scholar 

  45. McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. PACMPL 2(POPL), 33:1–33:28 (2018)

    Google Scholar 

  46. Meyn, S., Tweedie, R.: Markov Chains and Stochastic Stability. Cambridge University Press, Cambridge (2009)

    Book  Google Scholar 

  47. Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Foster and Grossman [27], pp. 496–512 (2018)

    Article  Google Scholar 

  48. Olmedo, F., Kaminski, B.L., Katoen, J.P., Matheja, C.: Reasoning about recursive probabilistic programs. In: LICS, pp. 672–681 (2016)

    Google Scholar 

  49. Paz, A.: Introduction to Probabilistic Automata. Computer Science and Applied Mathematics. Academic Press, Cambridge (1971)

    MATH  Google Scholar 

  50. Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI, pp. 239–251 (2004)

    Google Scholar 

  51. Rabin, M.: Probabilistic automata. Inf. Control. 6, 230–245 (1963)

    Article  Google Scholar 

  52. Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI, pp. 447–458 (2013)

    Google Scholar 

  53. Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM J. Comput. 13(2), 292–314 (1984)

    Article  MathSciNet  Google Scholar 

  54. Sohn, K., Gelder, A.V.: Termination detection in logic programs using argument sizes. In: PODS, pp. 216–226 (1991)

    Google Scholar 

  55. Staton, S., Yang, H., Wood, F.D., Heunen, C., Kammar, O.: Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, 5–8 July 2016, pp. 525–534. ACM, New York (2016)

    Google Scholar 

  56. Thiemann, P. (ed.): ESOP 2016. LNCS, vol. 9632. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1

    Book  MATH  Google Scholar 

  57. Williams, D.: Probability with Martingales. Cambridge University Press, Cambridge (1991)

    Book  Google Scholar 

Download references

Acknowledgements

This work is partially funded by the National Natural Science Foundation of China (NSFC) Grant no. 61802254, Austrian Science Fund (FWF) grant S11407-N23 (RiSE/SHiNE) and Vienna Science and Technology Fund (WWTF) project ICT15-003.

Author information

Authors and Affiliations

  1. Shanghai Jiao Tong University, Shanghai, China

    Hongfei Fu

  2. IST Austria, Klosterneuburg, Austria

    Krishnendu Chatterjee

Authors
  1. Hongfei Fu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Krishnendu Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hongfei Fu .

Editor information

Editors and Affiliations

  1. IRIF, University Paris Diderot and CNRS, Paris, France

    Constantin Enea

  2. Yale University, New Haven, CT, USA

    Ruzica Piskac

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Fu, H., Chatterjee, K. (2019). Termination of Nondeterministic Probabilistic Programs. In: Enea, C., Piskac, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2019. Lecture Notes in Computer Science(), vol 11388. Springer, Cham. https://doi.org/10.1007/978-3-030-11245-5_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-11245-5_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-11244-8

  • Online ISBN: 978-3-030-11245-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation