{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T05:54:43Z","timestamp":1783490083776,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"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_16","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"280-296","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Probabilistic CTL $$^{*}$$ : The Deductive Way"],"prefix":"10.1007","author":[{"given":"Rayna","family":"Dimitrova","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luis Mar\u00eda","family":"Ferrer Fioriti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-36576-1_6","volume-title":"Foundations of Software Science and Computational Structures","author":"T Arons","year":"2003","unstructured":"Arons, T., Pnueli, A., Zuck, L.D.: Parameterized verification by probabilistic abstraction. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 87\u2013102. Springer, Heidelberg (2003)"},{"key":"16_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"DP Bertsekas","year":"1991","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Math. Oper. Res. 16(3), 580\u2013595 (1991)","journal-title":"Math. Oper. Res."},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS. LNCS, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-32033-3_24","volume-title":"Term Rewriting and Applications","author":"O Bournez","year":"2005","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 323\u2013337. Springer, Heidelberg (2005)"},{"key":"16_CR6","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)"},{"issue":"4","key":"16_CR7","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 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"16_CR8","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. PhD thesis, Standford (1997)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, p. 395. Springer, Heidelberg (2000)"},{"key":"16_CR10","unstructured":"Dimitrova, R., Ferrer Fioriti, L.M., Hermanns, H., Majumdar, R.: PCTL\n                      \n                        \n                      \n                      $$^*$$\n                    : the deductive way (extended version). Reports of SFB\/TR 14 AVACS 114, (2016). \n                      http:\/\/www.avacs.org"},{"key":"16_CR11","series-title":"Series in Statistical and Probabilistic Mathematics","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. Series in Statistical and Probabilistic Mathematics, 4th edn. Cambridge University Press, New York (2010)","edition":"4"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31424-7_14","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2012","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 123\u2013138. Springer, Heidelberg (2012)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL, pp. 489\u2013501 (2015)","DOI":"10.1145\/2775051.2677001"},{"key":"16_CR14","volume-title":"Competitive Markov Decision Processes","author":"J Filar","year":"1997","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997)"},{"key":"16_CR15","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"N Francez","year":"1986","unstructured":"Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Heidelberg (1986)"},{"issue":"3","key":"16_CR16","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S Hart","year":"1983","unstructured":"Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst. 5(3), 356\u2013380 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR17","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. PhD thesis, University of Cambridge (2001)"},{"key":"16_CR18","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":"2\u20133","key":"16_CR19","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.tcs.2004.09.023","volume":"331","author":"Y Kesten","year":"2005","unstructured":"Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theor. Comput. Sci. 331(2\u20133), 397\u2013428 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"16_CR20","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1530873.1530882","volume":"36","author":"MZ Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic model checking for performance and reliability analysis. SIGMETRICS Perform. Eval. Rev. 36(4), 40\u201345 (2009)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"key":"16_CR21","series-title":"Monographs in Computer Science","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005)"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 278\u2013290 (1983)","DOI":"10.1145\/800061.808757"},{"issue":"1","key":"16_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. Comput. 103(1), 1\u201329 (1993)","journal-title":"Inf. Comput."},{"key":"16_CR24","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF00288965","volume":"17","author":"MO Rabin","year":"1982","unstructured":"Rabin, M.O.: The choice coordination problem. Acta Informatica 17, 121\u2013134 (1982)","journal-title":"Acta Informatica"},{"issue":"4\u20135","key":"16_CR25","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s00165-008-0075-6","volume":"20","author":"M Slanina","year":"2008","unstructured":"Slanina, M., Sipma, H.B., Manna, Z.: Deductive verification of alternating systems. Form. Asp. Comput. 20(4\u20135), 507\u2013560 (2008)","journal-title":"Form. Asp. Comput."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"}],"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_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:13:20Z","timestamp":1585012400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_16","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"}]}}