{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T14:08:00Z","timestamp":1767967680922,"version":"3.49.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031223365","type":"print"},{"value":"9783031223372","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_18","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"364-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8406-0443","authenticated-orcid":false,"given":"Miroslav","family":"Chodil","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6602-8028","authenticated-orcid":false,"given":"Anton\u00edn","family":"Ku\u010dera","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. In: FOCS, pp. 164\u2013169. IEEE Computer Society (1989)","DOI":"10.1109\/SFCS.1989.63473"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proceedings of IFIP, TCS 2004, pp. 493\u2013506. Kluwer (2004)","DOI":"10.1007\/1-4020-8141-3_38"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-51803-7_22","volume-title":"Temporal Logic in Specification","author":"B Banieqbal","year":"1989","unstructured":"Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62\u201374. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51803-7_22"},{"key":"18_CR4","unstructured":"Bertrand, N., Fearnley, J., Schewe, S.: Bounded satisfiability for PCTL. In: Proceedings of CSL 2012. Leibniz International Proceedings in Informatics, vol. 16, pp. 92\u2013106. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"18_CR5","volume-title":"Probability and Measure","author":"P Billingsley","year":"1995","unstructured":"Billingsley, P.: Probability and Measure. Wiley, Hoboken (1995)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Forejt, V., Ku\u010dera, A.: Stochastic games with branching-time winning objectives. In: Proceedings of LICS 2006, pp. 349\u2013358. IEEE Computer Society Press (2006)","DOI":"10.1109\/LICS.2006.48"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A.: The satisfiability problem for probabilistic CTL. In: Proceedings of LICS 2008, pp. 391\u2013402. IEEE Computer Society Press (2008)","DOI":"10.1109\/LICS.2008.21"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A.: The satisfiability problem for probabilistic CTL. Technical report FIMU-RS-2008-03. Faculty of Informatics, Masaryk University (2008)","DOI":"10.1109\/LICS.2008.21"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-70583-3_13","volume-title":"Automata, Languages and Programming","author":"T Br\u00e1zdil","year":"2008","unstructured":"Br\u00e1zdil, T., Forejt, V., Ku\u010dera, A.: Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 148\u2013159. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70583-3_13"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-31856-9_12","volume-title":"STACS 2005","author":"T Br\u00e1zdil","year":"2005","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: On the decidability of temporal properties of probabilistic pushdown automata. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 145\u2013157. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31856-9_12"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: Proceedings of STOC 1988, pp. 460\u2013467. ACM Press (1988)","DOI":"10.1145\/62212.62257"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Cern\u00fd, P., Henzinger, T.A.: From boolean to quantitative synthesis. In: EMSOFT, pp. 149\u2013154. ACM (2011)","DOI":"10.1145\/2038642.2038666"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11560548_7","volume-title":"Correct Hardware Design and Verification Methods","author":"A Chakrabarti","year":"2005","unstructured":"Chakrabarti, A., Chatterjee, K., Henzinger, T.A., Kupferman, O., Majumdar, R.: Verifying quantitative properties using bound functions. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 50\u201364. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560548_7"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Katoen, J.: On the satisfiability of some simple probabilistic logics. In: LICS, pp. 56\u201365. ACM (2016)","DOI":"10.1145\/2933575.2934526"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-87531-4_28","volume-title":"Computer Science Logic","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 385\u2013400. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87531-4_28"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Jurdzinski, M., Henzinger, T.A.: Quantitative stochastic parity games. In: SODA, pp. 121\u2013130. SIAM (2004)","DOI":"10.21236\/ADA603293"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-030-86593-1_10","volume-title":"Fundamentals of Computation Theory","author":"M Chodil","year":"2021","unstructured":"Chodil, M., Ku\u010dera, A.: The satisfiability problem for a quantitative fragment of PCTL. In: Bampis, E., Pagourtzis, A. (eds.) FCT 2021. LNCS, vol. 12867, pp. 149\u2013161. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86593-1_10"},{"issue":"4","key":"18_CR19","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. Assoc. Comput. Mach. 42(4), 857\u2013907 (1995)","journal-title":"J. Assoc. Comput. Mach."},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-662-49674-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Daca","year":"2016","unstructured":"Daca, P., Henzinger, T.A., K\u0159et\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 112\u2013129. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_7"},{"key":"18_CR21","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Linear distances between Markov chains. In: CONCUR. LIPIcs, vol. 59, pp. 20:1\u201320:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"issue":"3","key":"18_CR22","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Emerson, E.: Temporal and modal logic. In: Handbook of Theoretical Computer Science B, pp. 995\u20131072 (1991)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Emerson, E., Halpern, J.: Decision procedures and expressiveness in the temporal logic of branching time. In: Proceedings of STOC 1982, pp. 169\u2013180. ACM Press (1982)","DOI":"10.1145\/800070.802190"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku\u010dera, A., Mayr, R.: Model-checking probabilistic pushdown automata. Log. Methods Comput. Sci. 2(1:2), 1\u201331 (2006)","DOI":"10.2168\/LMCS-2(1:2)2006"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-31856-9_28","volume-title":"STACS 2005","author":"K Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of non-linear equations. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 340\u2013352. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31856-9_28"},{"key":"18_CR27","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M Fischer","year":"1979","unstructured":"Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"18_CR28","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, 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"2\u20133","key":"18_CR29","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0019-9958(86)80001-8","volume":"70","author":"S Hart","year":"1986","unstructured":"Hart, S., Sharir, M.: Probabilistic propositional temporal logics. Inf. Control 70(2\u20133), 97\u2013155 (1986)","journal-title":"Inf. Control"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Hart, S., Sharir, M.: Probabilistic temporal logics for finite and bounded models. In: STOC, pp. 1\u201313. ACM (1984)","DOI":"10.1145\/800057.808660"},{"issue":"2","key":"18_CR31","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.tcs.2005.11.015","volume":"354","author":"T Henzinger","year":"2006","unstructured":"Henzinger, T., Kupferman, O., Majumdar, R.: On the universal and existential fragments of the $$\\mu $$-calculus. Theoret. Comput. Sci. 354(2), 173\u2013186 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: From boolean to quantitative notions of correctness. In: POPL, pp. 157\u2013158. ACM (2010)","DOI":"10.1145\/1707801.1706319"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-33666-9_1","volume-title":"Model Driven Engineering Languages and Systems","author":"TA Henzinger","year":"2012","unstructured":"Henzinger, T.A.: Quantitative reactive models. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 1\u20132. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33666-9_1"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Sara\u00e7, N.E.: Quantitative and approximate monitoring. In: LICS, pp. 1\u201314. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470547"},{"key":"18_CR35","doi-asserted-by":"crossref","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proceedings of LICS 1997, pp. 111\u2013122. IEEE Computer Society Press (1997)","DOI":"10.1109\/LICS.1997.614940"},{"issue":"3","key":"18_CR36","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF00370554","volume":"47","author":"D Kozen","year":"1988","unstructured":"Kozen, D.: A finite-model theorem for the propositional $$\\mu $$-calculus. Stud. Logica 47(3), 233\u2013241 (1988)","journal-title":"Stud. Logica"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"Kraus, S., Lehmann, D.: Decision procedures for time and chance. In: Proceedings of FOCS 1983, pp. 202\u2013209. IEEE Computer Society Press (1983)","DOI":"10.1109\/SFCS.1983.12"},{"key":"18_CR38","unstructured":"K\u0159et\u00ednsk\u00fd, J., Rotar, A.: The satisfiability problem for unbounded fragments of probabilistic CTL. In: Proceedings of CONCUR 2018. Leibniz International Proceedings in Informatics, vol. 118, pp. 32:1\u201332:16. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2018)"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/11590156_44","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"A Ku\u010dera","year":"2005","unstructured":"Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: On the controller synthesis for finite-state Markov decision processes. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 541\u2013552. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11590156_44"},{"key":"18_CR40","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/345099.345104","volume":"22","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.: An automata-theoretic approach to modular model checking. ACM Trans. Program. Lang. Syst. 22, 87\u2013128 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR41","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D Lehmann","year":"1982","unstructured":"Lehmann, D., Shelah, S.: Reasoning with time and chance. Inf. Control 53, 165\u2013198 (1982)","journal-title":"Inf. Control"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:55:26Z","timestamp":1728615326000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}