{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:20:15Z","timestamp":1778498415119,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_15","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"260-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Deductive Proofs of Almost Sure Persistence and Recurrence Properties"],"prefix":"10.1007","author":[{"given":"Aleksandar","family":"Chakarov","sequence":"first","affiliation":[]},{"given":"Yuen-Lam","family":"Voronin","sequence":"additional","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A.: A contractivity approach for probabilistic bisimulations of diffusion processes. In: Proceedings of CDC, pp. 2230\u20132235 (2009)","DOI":"10.1109\/CDC.2009.5400334"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A.: Probabilistic bisimulations of switching and resetting diffusions. In: Proceedings of CDC, pp. 5918\u20135923 (2010)","DOI":"10.1109\/CDC.2010.5717751"},{"issue":"6","key":"15_CR3","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"16","author":"A Abate","year":"2010","unstructured":"Abate, A., Katoen, J.-P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 16(6), 624\u2013641 (2010)","journal-title":"Eur. J. Control"},{"key":"15_CR4","series-title":"International Series in Operations Research & Management Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-0769-0","volume-title":"Handbook on Semidefinite, Conic and Polynomial Optimization","author":"MF Anjos","year":"2012","unstructured":"Anjos, M.F., Lasserre, J.B.: Handbook on Semidefinite, Conic and Polynomial Optimization. International Series in Operations Research & Management Science, vol. 166. Springer, New York (2012)"},{"key":"15_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P., et al.: Principles of Model Checking, vol. 26202649. MIT press, Cambridge (2008)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Blekherman, G., Parrilo, P.A., Thomas, R.R.: Semidefinite optimization and convex algebraic geometry. In: MOS-SIAM Series on Optimization. Society for Industrial and Applied Mathematics (SIAM), vol. 13. Mathematical Optimization Society, Philadelphia, PA (2013)","DOI":"10.1137\/1.9781611972290"},{"issue":"8","key":"15_CR7","doi-asserted-by":"publisher","first-page":"1040","DOI":"10.1177\/0278364909340446","volume":"28","author":"K Byl","year":"2009","unstructured":"Byl, K., Tedrake, R.: Metastable walking machines. Int. J. Robot. Res. 28(8), 1040\u20131064 (2009)","journal-title":"Int. J. Robot. Res."},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-319-10936-7_6","volume-title":"Static Analysis","author":"A Chakarov","year":"2014","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 85\u2013100. Springer, Heidelberg (2014)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Hasheminezhad, R., Novotny, P.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POpPL , St. Petersburg, Florida, United States, 20\u201322 January 2016","DOI":"10.1145\/2837614.2837639"},{"issue":"4","key":"15_CR11","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM (JACM) 42(4), 857\u2013907 (1995)","journal-title":"J. ACM (JACM)"},{"key":"15_CR12","unstructured":"De Alfaro, L.: Formal verification of probabilistic systems. PhD thesis, Stanford University (1997)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"De Alfaro, L.: How to specify and verify the long-run average behaviour of probabilistic systems. In: Proceedings of LICS, pp. 454\u2013465. IEEE (1998)","DOI":"10.1109\/LICS.1998.705679"},{"key":"15_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511779398","volume-title":"Probability: theory and examples","author":"R Durrett","year":"2010","unstructured":"Durrett, R.: Probability: theory and examples. Cambridge University Press, Cambridge (2010)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hartmanns, A., Hermann, H.: Probabilistic termination: Soundness, completeness, and compositionality. In: Proceedings of POPL, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2775051.2677001"},{"issue":"3","key":"15_CR16","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1214\/aoms\/1177728976","volume":"24","author":"FG Foster","year":"1953","unstructured":"Foster, F.G.: On the stochastic matrices associated with certain queuing processes. Ann. Math. Stat. 24(3), 355\u2013360 (1953)","journal-title":"Ann. Math. Stat."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Proceedings of FOSE 2014, pp. 167\u2013181 (2014)","DOI":"10.1145\/2593882.2593900"},{"issue":"5","key":"15_CR18","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"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\u2013406. Springer, Heidelberg (2010)"},{"issue":"3","key":"15_CR20","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"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\u2013591. Springer, Heidelberg (2011)"},{"issue":"2","key":"15_CR22","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1177\/027836499000900206","volume":"9","author":"T McGeer","year":"1990","unstructured":"McGeer, T.: Passive dynamic walking. Int. J. Robot. Res. 9(2), 62\u201382 (1990)","journal-title":"Int. J. Robot. Res."},{"key":"15_CR23","volume-title":"Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science)","author":"A McIver","year":"2004","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). SpringerVerlag, New York (2004)"},{"key":"15_CR24","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626630","volume-title":"Markov Chains and Stochastic Stability","author":"SP Meyn","year":"2009","unstructured":"Meyn, S.P., Tweedie, R.L.: Markov Chains and Stochastic Stability. Cambridge University Press, Cambridge (2009)"},{"key":"15_CR25","unstructured":"Papachristodoulou, A., Anderson, J., Valmorbida, G., Prajna, S., Seiler, P., Parrilo, P.A.: SOSTOOLS: Sum of squares optimization toolbox for MATLAB (2013). http:\/\/arxiv.org\/abs\/1310.4716"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: Stochastic safety verification using barrier certificates. In: 43rd IEEE Conference on Decision and Control, CDC, vol. 1, pp. 929\u2013934. IEEE (2004)","DOI":"10.1109\/CDC.2004.1428804"},{"issue":"7","key":"15_CR27","doi-asserted-by":"publisher","first-page":"901","DOI":"10.1177\/0278364912444146","volume":"31","author":"J Steinhardt","year":"2012","unstructured":"Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901\u2013923 (2012)","journal-title":"Int. J. Robot. Res."},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Stability and attractivity of absorbing sets for discrete-time Markov processes. In: IEEE 51st Annual Conference on Decision and Control (CDC), pp. 7652\u20137657. IEEE (2012)","DOI":"10.1109\/CDC.2012.6426410"},{"key":"15_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.09.032","volume":"515","author":"I Tkachev","year":"2014","unstructured":"Tkachev, I., Abate, A.: Characterization and computation of infinite-horizon specifications over markov processes. Theoret. Comput. Sci. 515, 1\u201318 (2014)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR30","unstructured":"Tkachev, I., Mereacre, A., Katoen, J.-P., Abate, A.: Quantitative model-checking of controlled discrete-time Markov processes (2014). arXiv preprint arXiv:1407.5449"},{"key":"15_CR31","series-title":"nternational Series in Operations Research and Management Science","doi-asserted-by":"publisher","first-page":"715","DOI":"10.1007\/978-1-4614-0769-0_25","volume-title":"Handbook on Semidefinite, Conic and Polynomial Optimization","author":"T Kim-Chuan","year":"2012","unstructured":"Kim-Chuan, T., Todd, M.J., T\u00fct\u00fcnc\u00fc, R.H.: On the implementation and usage of SDPT3\u2013a matlab software package for semidefinite-quadratic-linear programming, version 4.0. In: Anjos, M.F., Lasserre, J.B. (eds.) Handbook on Semidefinite, Conic and Polynomial Optimization. nternational Series in Operations Research and Management Science, vol. 166, pp. 715\u2013754. Springer, New York (2012)"},{"key":"15_CR32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813658","volume-title":"Probability with Martingales","author":"D Williams","year":"1991","unstructured":"Williams, D.: Probability with Martingales. Cambridge University Press, Cambridge (1991)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:27:02Z","timestamp":1748852822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}