×

zbMATH — the first resource for mathematics

Time-bounded termination analysis for probabilistic programs with delays. (English) Zbl 07285773
Summary: This paper investigates the model of probabilistic program with delays (PPD) that consists of a few program blocks. Performing each block has an additional time-consumption – waiting to be executed – besides the running time. We interpret the operational semantics of PPD by Markov automata with a cost structure on transitions. Our goal is to measure those individual execution paths of a PPD that terminates within a given time bound, and to compute the minimum termination probability, i.e. the termination probability under a demonic scheduler that resolves the nondeterminism inherited from probabilistic programs. When running time plus waiting time is bounded, the demonic scheduler can be determined by comparison between a class of well-formed real numbers. The method is extended to parametric PPDs. When only the running time is bounded, the demonic scheduler can be determined by real root isolation over a class of well-formed real functions under Schanuel’s conjecture. Finally we give the complexity upper bounds of the proposed methods.
MSC:
68Q Theory of computing
Software:
AProVE; REDLOG
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P. A., Carrying probabilities to the infinite world, (Katoen, J.-P.; König, B., Proceedings of the 22nd International Conference on Concurrency Theory. Proceedings of the 22nd International Conference on Concurrency Theory, LNCS, vol. 6901 (2011), Springer), 1-16 · Zbl 1343.68149
[2] Achatz, M.; McCallum, S.; Weispfenning, V., Deciding polynomial-exponential problems, (Proceedings of the 33rd International Symposium on Symbolic and Algebraic Computation (2008), ACM), 215-222 · Zbl 1236.68301
[3] Agrawal, S.; Chatterjee, K.; Novotný, P., Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs, (Proceedings of the ACM on Programming Languages 2 (POPL) (2018)), Article 34 pp.
[4] Arons, T.; Pnueli, A.; Zuck, L. D., Parameterized verification by probabilistic abstraction, (Gordon, A. D., Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures. Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures, LNCS, vol. 2620 (2003), Springer), 87-102 · Zbl 1029.68104
[5] Ax, J., On Schanuel’s conjectures, Ann. Math., 93, 2, 252-268 (1971) · Zbl 0232.10026
[6] Aziz, A.; Sanwal, K.; Singhal, V.; Brayton, R., Verifying continuous time Markov chains, (Alur, R.; Henzinger, T. A., Proceedings of the 8th International Conference on Computer Aided Verification. Proceedings of the 8th International Conference on Computer Aided Verification, LNCS, vol. 1102 (1996), Springer), 269-276
[7] Baier, C.; Haverkort, B. R.; Hermanns, H.; Katoen, J.-P., Model checking continuous-time Markov chains by transient analysis, (Emerson, E. A.; Sistla, A. P., Proceedings of the 12th International Conference on Computer Aided Verification. Proceedings of the 12th International Conference on Computer Aided Verification, LNCS, vol. 1855 (2000), Springer), 358-372 · Zbl 0974.68017
[8] Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), MIT Press
[9] Baker, A., Transcendental Number Theory (1975), Cambridge University Press · Zbl 0297.10013
[10] Ben-Amram, A. M.; Genaim, S., Ranking functions for linear-constraint loops, J. ACM, 61, 4, Article 26 pp. (2014) · Zbl 1321.68296
[11] Bournez, O.; Garnier, F., Proving positive almost-sure termination, (Giesl, J., Proceedings of the 16th International Conference on Term Rewriting and Applications. Proceedings of the 16th International Conference on Term Rewriting and Applications, LNCS, vol. 3467 (2005), Springer), 323-337 · Zbl 1078.68057
[12] Bradley, A. R.; Manna, Z.; Sipma, H. B., The polyranking principle, (Caires, L.; Italiano, G. F.; Monteiro, L.; Palamidessi, C.; Yung, M., Proceedings of the 32nd International Colloquium on Automata, Languages and Programming. Proceedings of the 32nd International Colloquium on Automata, Languages and Programming, LNCS, vol. 3580 (2005), Springer), 1349-1361 · Zbl 1081.68568
[13] Cai, X.; Zhou, X., Asymmetric earliness and tardiness scheduling with exponential processing times on an unreliable machine, Ann. Oper. Res., 98, 1-4, 313-331 (2000) · Zbl 0990.90033
[14] Chakarov, A.; Sankaranarayanan, S., Probabilistic program analysis with martingales, (Sharygina, N.; Veith, H., Proceedings of the 25th International Conference on Computer Aided Verification. Proceedings of the 25th International Conference on Computer Aided Verification, LNCS, vol. 8044 (2013), Springer), 511-526
[15] Chatterjee, K.; Fu, H.; Goharshady, A. K., Termination analysis of probabilistic programs through positivstellensatz’s, (Chaudhuri, S.; Farzan, A., Proceedings of the 28th International Conference on Computer Aided Verification, Part I. Proceedings of the 28th International Conference on Computer Aided Verification, Part I, LNCS, vol. 9779 (2016), Springer), 3-22 · Zbl 1411.68025
[16] Chatterjee, K.; Fu, H.; Goharshady, A. K., Non-polynomial worst-case analysis of recursive programs, (Majumdar, R.; Kuncak, V., Proceedings of the 29th International Conference on Computer Aided Verification, Part II. Proceedings of the 29th International Conference on Computer Aided Verification, Part II, LNCS, vol. 10427 (2017), Springer), 41-63
[17] Chatterjee, K.; Fu, H.; Murhekar, A., Automated recurrence analysis for almost-linear expected-runtime bounds, (Majumdar, R.; Kuncak, V., Proceedings of the 29th International Conference on Computer Aided Verification, Part I. Proceedings of the 29th International Conference on Computer Aided Verification, Part I, LNCS, vol. 10426 (2017), Springer), 118-139
[18] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Brakhage, H., Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages. Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, LNCS, vol. 33 (1975), Springer), 134-183
[19] Colón, M. A.; Sipma, H. B., Synthesis of linear ranking functions, (Margaria, T.; Yi, W., Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 2031 (2001), Springer), 67-81 · Zbl 0978.68095
[20] Cook, B.; Podelski, A.; Rybalchenko, A., TERMINATOR: beyond safety, (Ball, T.; Jones, R. B., Proceedings of the 18th International Conference on Computer Aided Verification. Proceedings of the 18th International Conference on Computer Aided Verification, LNCS, vol. 4144 (2006), Springer), 415-418
[21] de Moura, L.; Passmore, G. O., Computation in real closed infinitesimal and transcendental extensions of the rationals, (Bonacina, M. P., Proceedings of the 24th International Conference on Automated Deduction. Proceedings of the 24th International Conference on Automated Deduction, LNCS, vol. 7898 (2013), Springer), 178-192 · Zbl 1381.68278
[22] Deng, Y.; Hennessy, M., On the semantics of Markov automata, Inf. Comput., 222, 139-168 (2013) · Zbl 1286.68362
[23] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall · Zbl 0368.68005
[24] Dolzmann, A.; Sturm, T., REDLOG: computer algebra meets computer logic, ACM SIGSAM Bull., 31, 2, 2-9 (1997)
[25] Eisentraut, C.; Hermanns, H.; Zhang, L., On probabilistic automata in continuous time, (Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science (2010), IEEE Computer Society), 342-351
[26] Esparza, J.; Gaiser, A.; Kiefer, S., Proving termination of probabilistic programs using patterns, (Proceedings of the 24th International Conference on Computer Aided Verification. Proceedings of the 24th International Conference on Computer Aided Verification, LNCS, vol. 7358 (2012), Springer), 123-138
[27] Fioriti, L. M.F.; Hermanns, H., Probabilistic termination: soundness, completeness, and compositionality, (Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015), ACM), 489-501 · Zbl 1345.68104
[28] Giesl, J.; Brockschmidt, M.; Emmes, F.; Frohn, F.; Fuhs, C.; Otto, C.; Plücker, M.; Schneider-Kamp, P.; Ströder, T.; Swiderski, S.; Thiemann, R., Proving termination of programs automatically with AProVE, (Demri, S.; Kapur, D.; Weidenbach, C., Proceedings of the 7th International Joint Conference on Automated Reasoning. Proceedings of the 7th International Joint Conference on Automated Reasoning, LNCS, vol. 8562 (2014), Springer), 184-191 · Zbl 1409.68256
[29] Goldstine, H. H.; von Neumann, J., Planning and coding problems for an electronic computing instrument, (von Neumann, J.; Traub, A. H., The Collected Works of John von Neumann, vol. 5 (1963), Pergamon Press), 80-235
[30] Gordon, A. D.; Henzinger, T. A.; Nori, A. V.; Rajamani, S. K., Probabilistic programming, (Proceedings on Future of Software Engineering (2014), ACM), 167-181
[31] Hajek, B. E., The proof of a folk theorem on queuing delay with applications to routing in networks, J. ACM, 30, 4, 834-851 (1983) · Zbl 0627.68035
[32] Han, T.; Katoen, J.-P.; Mereacre, A., Approximate parameter synthesis for probabilistic time-bounded reachability, (Proceedings of the 29th IEEE Real-Time Systems Symposium (2008), IEEE Computer Society), 173-182
[33] He, J.; Seidel, K.; McIver, A., Probabilistic models for the guarded command language, Sci. Comput. Program., 28, 2-3, 171-192 (1997) · Zbl 0877.68014
[34] Hoare, C. A.R., An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105
[35] Hyytiä, E.; Aalto, S., On round-robin routing with FCFS and LCFS scheduling, Perform. Eval., 97, 83-103 (2016)
[36] Jansen, N.; Dehnert, C.; Kaminski, B. L.; Katoen, J.-P.; Westhofen, L., Bounded model checking for probabilistic programs, (Artho, C.; Legay, A.; Peled, D., Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis. Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, LNCS, vol. 9938 (2016), Springer), 68-85 · Zbl 1398.68343
[37] Kaltofen, E., Polynomial-time reductions from multivariate to bi- and univariate integral polynomial factorization, SIAM J. Comput., 14, 2, 469-489 (1985) · Zbl 0605.12001
[38] Kaminski, B. L.; Katoen, J.-P., On the hardness of almost-sure termination, (Italiano, G. F.; Pighizzini, G.; Sannella, D., Proceedings of the 40th International Symposium on Mathematical Foundations of Computer Science, Part I. Proceedings of the 40th International Symposium on Mathematical Foundations of Computer Science, Part I, LNCS, vol. 9234 (2015), Springer), 307-318 · Zbl 06482744
[39] Kaminski, B. L.; Katoen, J.-P.; Matheja, C.; Olmedo, F., Weakest precondition reasoning for expected run-times of probabilistic programs, (Thiemann, P., Proceedings of the 25th European Symposium on Programming. Proceedings of the 25th European Symposium on Programming, LNCS, vol. 9632 (2016), Springer), 364-389 · Zbl 1335.68058
[40] Katoen, J.-P.; Gretz, F.; Jansen, N.; Kaminski, B. L.; Olmedo, F., Understanding probabilistic programs, (Meyer, R.; Platzer, A.; Wehrheim, H., Correct System Design. Correct System Design, LNCS, vol. 9360 (2015), Springer), 15-32 · Zbl 1444.68045
[41] Kozen, D., Semantics of probabilistic programs, (Proceedings of the 20th Annual Symposium on Foundations of Computer Science (1979), IEEE Computer Society), 101-114
[42] Kozen, D., A probabilistic PDL, (Proceedings of the 15th Annual ACM Symposium on Theory of Computing (1983), ACM), 291-297
[43] Manna, Z., Mathematical Theory of Computation (1974), McGraw-Hill · Zbl 0353.68066
[44] McIver, A.; Morgan, C., Abstraction, Refinement and Proof for Probabilistic Systems (2006), Springer
[45] McIver, A.; Morgan, C.; Kaminski, B. L.; Katoen, J., A new proof rule for almost-sure termination, (Proceedings of the ACM on Programming Languages 2 (POPL) (2018)), Article 33 pp.
[46] Monniaux, D., An abstract analysis of the probabilistic termination of programs, (Cousot, P., Proceedings of the 8th International Symposium on Static Analysis. Proceedings of the 8th International Symposium on Static Analysis, LNCS, vol. 2126 (2001), Springer), 111-126 · Zbl 0997.68515
[47] Olmedo, F.; Kaminski, B. L.; Katoen, J.-P.; Matheja, C., Reasoning about recursive probabilistic programs, (Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (2016), ACM), 672-681 · Zbl 1401.68048
[48] Pinedo, M., Scheduling: Theory, Algorithms, and Systems (1995), Prentice-Hall · Zbl 1145.90393
[49] Podelski, A.; Rybalchenko, A., A complete method for the synthesis of linear ranking functions, (Steffen, B.; Levi, G., Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation. Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation, LNCS, vol. 2937 (2004), Springer), 239-251 · Zbl 1202.68109
[50] Ross, S., Introduction to Stochastic Dynamic Programming (1983), Academic Press · Zbl 0567.90065
[51] Sharir, M.; Pnueli, A.; Hart, S., Verification of probabilistic programs, SIAM J. Comput., 13, 2, 292-314 (1984) · Zbl 0533.68012
[52] Stewart, W. J., Introduction to the Numerical Solution of Markov Chains (1994), Princeton University Press · Zbl 0821.65099
[53] Tanenbaum, A. S., Modern Operating Systems (2007), Pearson · Zbl 0856.68041
[54] Wang, P.; Fu, H.; Chatterjee, K.; Deng, Y.; Xu, M., Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination, (Proceedings of the ACM on Programming Languages 4 (POPL) (2020)), Article 25 pp.
[55] Weiss, G.; Pinedo, M., Scheduling tasks with exponential service times on nonidentical processors to minimize makespan or flow time, J. Appl. Probab., 17, 1, 187-202 (1980) · Zbl 0427.90051
[56] Xu, M.; Chen, L.; Zeng, Z.; Li, Z.-B., Reachability analysis of rational eigenvalue linear systems, Int. J. Syst. Sci., 41, 12, 1411-1419 (2010) · Zbl 1206.93013
[57] Xu, M.; Zhang, L.; Jansen, D. N.; Zhu, H.; Yang, Z., Multiphase until formulas over Markov reward models: an algebraic approach, Theor. Comput. Sci., 611, 116-135 (2016) · Zbl 1332.68143
[58] Zhang, L.; Jansen, D. N.; Nielson, F.; Hermanns, H., Efficient CSL model checking using stratification, Log. Methods Comput. Sci., 8, 2, Article 17 pp. (2012) · Zbl 1348.68152
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.