{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:23Z","timestamp":1780994483512,"version":"3.54.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030010898","type":"print"},{"value":"9783030010904","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-01090-4_28","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T11:23:23Z","timestamp":1538220203000},"page":"476-493","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs"],"prefix":"10.1007","author":[{"given":"Toru","family":"Takisaka","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuichiro","family":"Oyabu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natsuki","family":"Urabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"issue":"6","key":"28_CR1","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., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 16(6), 624\u2013641 (2010)","journal-title":"Eur. J. Control"},{"issue":"POPL","key":"28_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158122","volume":"2","author":"Sheshansh Agrawal","year":"2017","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. PACMPL 2(POPL), 34:1\u201334:32 (2018)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-90686-7_9","volume-title":"Functional and Logic Programming","author":"M Avanzini","year":"2018","unstructured":"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\u2013148. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-90686-7_9"},{"key":"28_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"key":"28_CR5","unstructured":"Bertsekas, D.P., Shreve, S.E.: Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific (2007)"},{"key":"28_CR6","unstructured":"Bod\u00edk, R., Majumdar, R. (eds.): Proceedings of POPL 2016. ACM (2016)"},{"key":"28_CR7","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-662-49674-9_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Chakarov","year":"2016","unstructured":"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\u2013279. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_15"},{"key":"28_CR9","unstructured":"Chatterjee, K., Fu, H.: Termination of nondeterministic recursive probabilistic programs. CoRR abs\/1701.02944 (2017). arXiv:1701.02944"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Bod\u00edk and Majumdar [6], pp. 327\u2013342","DOI":"10.1145\/2914770.2837639"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of POPL 2017. pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3009837.3009873"},{"issue":"1","key":"28_CR13","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"R Cousot","year":"1979","unstructured":"Cousot, R., Cousot, P.: Constructive versions of Tarski\u2019s fixed point theorems. Pacific Journal of Mathematics 82(1), 43\u201357 (1979)","journal-title":"Pacific Journal of Mathematics"},{"key":"28_CR14","doi-asserted-by":"publisher","unstructured":"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\u201317, 2015. pp. 489\u2013501. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"28_CR15","unstructured":"The GNU linear programming kit, http:\/\/www.gnu.org\/software\/glpk"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"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\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"issue":"1","key":"28_CR17","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1145\/2914770.2837673","volume":"51","author":"Ichiro Hasuo","year":"2016","unstructured":"Hasuo, I., Shimizu, S., C\u00eerstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: Bod\u00edk and Majumdar [6], pp. 718\u2013732","journal-title":"ACM SIGPLAN Notices"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small Progress Measures for Solving Parity Games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290\u2013301. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46541-3_24"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"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\u20138, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9632, pp. 364\u2013389. Springer (2016)","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"28_CR20","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). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24"},{"key":"28_CR21","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). Springer Verlag (2004)"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11889229_4","volume-title":"Refinement Techniques in Software Engineering","author":"A McIver","year":"2006","unstructured":"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\u2013155. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11889229_4"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013934 (2004)","DOI":"10.1109\/CDC.2004.1428804"},{"key":"28_CR24","unstructured":"SDPT3, http:\/\/www.math.nus.edu.sg\/~mattohkc\/sdpt3.html"},{"key":"28_CR25","unstructured":"SOSTOOLS, http:\/\/sysos.eng.ox.ac.uk\/sostools\/"},{"issue":"7","key":"28_CR26","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. I. J. Robotics Res. 31(7), 901\u2013923 (2012)","journal-title":"I. J. Robotics Res."},{"key":"28_CR27","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for approximating reachability. CoRR abs\/1805.10749 (2018), arXiv:1805.10749"},{"key":"28_CR28","doi-asserted-by":"crossref","unstructured":"Urabe, N., Hara, M., Hasuo, I.: Categorical liveness checking by corecursive algebras. In: Proc. of LICS 2017. pp. 1\u201312. IEEE Computer Society (2017)","DOI":"10.1109\/LICS.2017.8005151"},{"key":"28_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"MY Vardi","year":"1996","unstructured":"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\u2013266. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60915-6_6"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-01090-4_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,24]],"date-time":"2019-10-24T23:34:17Z","timestamp":1571960057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}