Abstract
Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analog for probabilistic programs, namely termination with probability one (“almost-sure termination”), is an equally important property for randomized algorithms and probabilistic protocols. We suggest a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs: it calls such tools within a refinement loop and thereby iteratively constructs a “terminating pattern”, which is a set of terminating runs with probability one. We report on various case studies illustrating the effectiveness of our algorithm. As a further application, our algorithm can improve lower bounds on reachability probabilities.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arons, T., Pnueli, A., Zuck, L.D.: Parameterized Verification by Probabilistic Abstraction. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 87–102. Springer, Heidelberg (2003)
Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)
Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32, 824–840 (1985)
Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)
Esparza, J., Gaiser, A.: Probabilistic Abstractions with Arbitrary Domains. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 334–350. Springer, Heidelberg (2011)
Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. Technical report (2012), http://arxiv.org/abs/1204.2932
Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: Abstraction Refinement for Infinite Probabilistic Models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 353–357. Springer, Heidelberg (2010)
Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008)
Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003)
Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction Refinement for Probabilistic Software. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 182–197. Springer, Heidelberg (2009)
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)
McIver, A., Morgan, C., Hoang, T.S.: Probabilistic Termination in B. In: Bert, D., Bowen, J. P., King, S., Waldén, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 216–239. Springer, Heidelberg (2003)
Monniaux, D.: An Abstract Analysis of the Probabilistic Termination of Programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 111–126. Springer, Heidelberg (2001)
Nakata, T.: On the expected time for Herman’s probabilistic self-stabilizing algorithm. Theoretical Computer Science 349(3), 475–483 (2005)
Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: STOC, pp. 278–290. ACM (1983)
Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. Comput. 103, 1–29 (1993)
Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32–41. IEEE Computer Society (2004)
Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006)
Podelski, A., Rybalchenko, A.: Transition Invariants and Transition Predicate Abstraction for Program Termination. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 3–10. Springer, Heidelberg (2011)
Rybalchenko, A.: Temporal verification with transition invariants. PhD thesis (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Esparza, J., Gaiser, A., Kiefer, S. (2012). Proving Termination of Probabilistic Programs Using Patterns. In: Madhusudan, P., Seshia, S.A. (eds) Computer Aided Verification. CAV 2012. Lecture Notes in Computer Science, vol 7358. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31424-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-31424-7_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31423-0
Online ISBN: 978-3-642-31424-7
eBook Packages: Computer ScienceComputer Science (R0)