Advertisement

Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs

  • Toru TakisakaEmail author
  • Yuichiro Oyabu
  • Natsuki Urabe
  • Ichiro Hasuo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account of various martingale-based methods for over- and underapproximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points—a classic topic in computer science—in the analysis of probabilistic programs. This leads us to two new martingale-based techniques, too. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales.

Notes

Acknowledgment

We thank Shin-ya Katsumata, Takamasa Okudono and the anonymous referees for useful comments. The authors are supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), the JSPS-INRIA Bilateral Joint Research Project “CRECOGI,” and JSPS KAKENHI Grant Numbers 15KT0012 & 15K11984. Natsuki Urabe is supported by JSPS KAKENHI Grant Number 16J08157.

References

  1. 1.
    Abate, A., Katoen, J., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 16(6), 624–641 (2010)MathSciNetCrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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_9CrossRefGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)Google Scholar
  5. 5.
    Bertsekas, D.P., Shreve, S.E.: Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific (2007)Google Scholar
  6. 6.
    Bodík, R., Majumdar, R. (eds.): Proceedings of POPL 2016. ACM (2016)Google Scholar
  7. 7.
    Chakarov, A., Sankaranarayanan, S.: Probabilistic Program Analysis with Martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511–526. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_34CrossRefGoogle Scholar
  8. 8.
    Chakarov, A., Voronin, Y.-L., Sankaranarayanan, S.: Deductive Proofs of Almost Sure Persistence and Recurrence Properties. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 260–279. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_15CrossRefGoogle Scholar
  9. 9.
    Chatterjee, K., Fu, H.: Termination of nondeterministic recursive probabilistic programs. CoRR abs/1701.02944 (2017). arXiv:1701.02944
  10. 10.
    Chatterjee, K., Fu, H., Goharshady, A.K.: Termination Analysis of Probabilistic Programs Through Positivstellensatz’s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3–22. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41528-4_1CrossRefGoogle Scholar
  11. 11.
    Chatterjee, K., Fu, H., Novotný, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Bodík and Majumdar [6], pp. 327–342Google Scholar
  12. 12.
    Chatterjee, K., Novotný, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of POPL 2017. pp. 145–160. ACM (2017)Google Scholar
  13. 13.
    Cousot, R., Cousot, P.: Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics 82(1), 43–57 (1979)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: Soundness, completeness, and compositionality. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015. pp. 489–501. ACM (2015).  https://doi.org/10.1145/2676726.2677001
  15. 15.
    The GNU linear programming kit, http://www.gnu.org/software/glpk
  16. 16.
    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. pp. 167–181. ACM (2014)Google Scholar
  17. 17.
    Hasuo, I., Shimizu, S., Cîrstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: Bodík and Majumdar [6], pp. 718–732CrossRefGoogle Scholar
  18. 18.
    Jurdziński, M.: Small Progress Measures for Solving Parity Games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-46541-3_24CrossRefGoogle Scholar
  19. 19.
    Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: Thiemann, P. (ed.) Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9632, pp. 364–389. Springer (2016)Google Scholar
  20. 20.
    Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-Invariant Generation for Probabilistic Programs: In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390–406. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_24CrossRefGoogle Scholar
  21. 21.
    McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). Springer Verlag (2004)Google Scholar
  22. 22.
    McIver, A., Morgan, C.: Developing and Reasoning About Probabilistic Programs in pGCL. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 123–155. Springer, Heidelberg (2006).  https://doi.org/10.1007/11889229_4CrossRefGoogle Scholar
  23. 23.
    Prajna, S., Jadbabaie, A., Pappas, G.J.: Stochastic safety verification using barrier certificates. In: 2004 43rd IEEE Conference on Decision and Control. IEEE, Piscataway. pp. 929–934 (2004)Google Scholar
  24. 24.
  25. 25.
  26. 26.
    Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. I. J. Robotics Res. 31(7), 901–923 (2012)CrossRefGoogle Scholar
  27. 27.
    Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for approximating reachability. CoRR abs/1805.10749 (2018), arXiv:1805.10749
  28. 28.
    Urabe, N., Hara, M., Hasuo, I.: Categorical liveness checking by corecursive algebras. In: Proc. of LICS 2017. pp. 1–12. IEEE Computer Society (2017)Google Scholar
  29. 29.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60915-6_6CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Toru Takisaka
    • 1
    Email author
  • Yuichiro Oyabu
    • 1
    • 2
  • Natsuki Urabe
    • 3
  • Ichiro Hasuo
    • 1
    • 2
  1. 1.National Institute of InformaticsTokyoJapan
  2. 2.The Graduate University for Advanced Studies (SOKENDAI)HayamaJapan
  3. 3.University of TokyoTokyoJapan

Personalised recommendations